直観主義論理への招待
p9
定義2.7
直観主義論理ILでの証明
有限または無限の文の集合$ T，有限部分集合$ \Gamma\subseteq Tについて
$ \Gamma\implies\varphiの証明図が存在するなら$ \varphiは$ Tから直観主義的に導出できる
$ T \vdash_{IL} \varphiと書く
特に$ T=\emptyなら$ \vdash_{IL}\varphiであって，直観主義的に証明できると言う
p11
節2.4
以下，$ \vdash_{IL}を$ \vdash
$ \varphi \vdash \psiかつ$ \psi \vdash \varphiを$ \varphi \sim \phiと書く（つまり$ \varphi \dashv\vdash \psi）
$ Tを項全体の集合，$ Fを論理式全体の集合，$ \vdashを$ F上の二項関係とみなす すなわち
反射律:$ \varphi\vdash\varphi 推移律:$ \varphi\vdash\psi, \psi\vdash\xi \implies \varphi\vdash\xi $ \varphi\land\psi,\varphi\lor\psiがそれぞれ$ \{\varphi,\psi\}の下限，上限
すなわち
$ \xi\vdash\varphiかつ$ \xi\vdash\varphi
$ \iff$ \xi\vdash\varphi\land\psi（下限）
$ \varphi\vdash\xiかつ$ \varphi\vdash\xi
$ \iff$ \varphi\lor\psi\vdash\xi（上限）
$ \forall x.\varphi(x),\exists x.\varphi(x)はそれぞれ$ \{\varphi(t):t\in T\}の下限，上限
すなわち
$ \forall t \in Tについて$ \xi\vdash\varphi(t)
$ \iff$ \xi \vdash \forall x.\varphi(x)
$ \forall t \in Tについて$ \varphi(t)\vdash\xi
$ \iff$ \exists x.\varphi(x)\vdash\xi
つまり
$ \xi\land\varphi\vdash\psi
$ \iff$ \xi \vdash\varphi\to\psi
$ \xi\land(\varphi\lor\psi)\dashv\vdash(\xi\land\varphi)\lor(\xi\land\psi)
$ \xi\land\exists x.\varphi(x) \dashv\vdash \exists x.(\xi\land\varphi(x))
p13.
全称の場合の分配則，つまり
$ \xi\land\exists x.\varphi(x) \dashv\vdash \forall x.(\xi\land\varphi(x))
$ (\varphi\to\psi) \lor (\psi\to\varphi)
$ \exist x.(\varphi(x) \to \forall y.\varphi(y))
SnO2WMaN.iconなにこれ？どういうことが起きてるんだ