2023.10.02
https://www.youtube.com/watch?v=TIcesHBdz1s
いいね
https://www.youtube.com/watch?v=GhfXIiq2vxE
この
メモ
今仮定している算術では$ T \vdash A \to B ~\text{iff}~ (T \vdash A \implies T \vdash B)を仮定しているが，これって成り立つんだっけ？
$ \lbrack T \vdash A \implies T \vdash B \rbrack \implies T \vdash A \to B
$ \lbrack T \vdash A \implies T \vdash B \rbrack \impliedby T \vdash A \to B
冷静に考えると全然違うじゃん なんだこの形式化 ミスった…
もう一度考え直す
$ T \vdash \sigma \to \pi ~\&~ T \vdash \sigma \implies T \vdash \pi
読んだ
不動点を直接求めに行くのは面倒くさいという点までは確認した
知った
https://www.youtube.com/watch?v=fRQtDjiRtI8