2021年度後期哲学演習I 直観主義論理のメモ
古典論理には非構成的なトリックが存在する
背理法はどうなんだ？
例.存在しないを仮定し，これを否定して存在するを主張する
二重否定除去を否定する
前順序を\leqで表す
様相論理S4のフレームと同じである
直観主義論理のフレーム\lang W,\leq \rang
Wの各要素，各命題変項の対に対しての関数vが次の性質を満たす
v(x,p) = 1かつx \leq yならば，v(y,p) = 1
直観主義論理の\to,\lnotは少し意味が違う
直観主義の含意は厳密含意に似ている
v(x,A\to B)=1の意味
Aの証明さえあればBの証明を構成できる方法がありますよ
v(x,\lnot A) = 1の意味
時点（世界）xにおいて[* Aは証明不可能である]という証明がある
ここから，v(x,\lnot A) = 1からv(x,\lnot A) = 0は成り立たないことが示される
遺伝性(直観主義論理)は拡張される
命題変項pだけでなく，任意の論理式Aについても遺伝性へと拡張される
v(x,A) = 1かつx \leq yならv(y,A)=1
性質\phiについて
1. 最も単純な論理式である命題変項pで\phi成り立つこと
2. 論理式A,Bが\phiを満たすと仮定し
A \lor B,A\land B,A\to B,\lnot Aでも\phiが満たされること
1,2を満たすなら，任意の論理式で性質\phiが成り立つことが証明出来る
証明，論理式の構成に関する帰納法を用いる
1については自明
2
A\land Bの場合
主張
v(x,A\land B) = 1かつx \leq yならv(y,A\land B)=1
v(x,A \land B)=1,x\leq yとする
演算子の定義より，v(x,A)=1,v(x,B)=1である
仮定より，v(y,A)=1,v(y,B)=1である
演算子の定義より，v(y,A\land B) = 1である，証明終了
A\lor Bの場合
A\land Bの場合と同様なので省略
\lnot Aの場合
主張
v(x,\lnot A) = 1かつx \leq yならv(y,\lnot A)=1
v(y,\lnot A)=1\iffx\leq yなる全てのyについてv(y,A)=0
v(x,\lnot A)=1,x\leq yとする
演算子の定義より
x\leq zとなる全てのzでv(z,A) = 0である
このときy,zは同じものであると考えられる…？
A \to Bの場合
\lnot Aの場合とまあ近いことにはなると思う
直観主義論理のモデルM = \lang W,\leq,v \rang
あるx \in Wについて
B \in Xでv(x,B)=1
v(x,A)=0
が成り立つなら，Mを前提Xから結論Aへの推論への反例モデルと呼ぶ
フレームの妥当性
フレームF=\lang W,\leq \rangで前提Xから結論Aへの推論の反例モデルが作れないなら
直観主義論理のフレームにおいて妥当である
X \models^F Aと書く
全てのフレームFでX \models^F Aならその推論は
直観主義論理において妥当である
X \models_{Int} Aあるいは単にX \models Aと書く
\not\models A \lor \lnot A
x\leq y
v(x,p)=0, v(y,p)=1を考えると，
v(x, \lnot p) = 0である
ここから，v(x,p\lor \lnot p) = 0が成り立つ
以下，直観主義論理で妥当だったり非妥当だったりする推論
A \models \lnot\lnot A二重否定導入
\lnot\lnot A \not\models A二重否定除去
A\lor B,\lnot B \models A選言三段論法
(A\land B) \to C \not\models (A \to C)\lor(B \to C)
A \to B \models \lnot B \to \lnot A対偶の導入
\lnot B \to \lnot A \models A \to B対偶の除去
\not\models_{Int} A \lor \lnot A
AかAでないかのどちらかとは限らない
どういうことなのか？
直観主義論理
「Aが真」とは「Aの証明が存在すること」
「Aが偽」なら「\lnot Aが真/の証明が存在すること」
「肯定か否定が，いつか証明される可能性がある，しかしまだ証明されていない」という状態がある
「まだ真とも偽とも言えない」命題がある
直観主義論理は「原理的には可能」に位置する
補題：直観主義論理の選言特性
\models_{Int} A \lor Bならば，\models_{Int}Aまたは\models_{Int}Bのどちらかが成り立つ
証明
\not\models Aかつ\not\models Bのそれぞれの反例モデルを合体させると\not\models A \lor Bの反例モデルが作れる
対偶を取って証明
以上の議論をn値論理なら命題変項をn+1個の命題変項を用意する
任意の論理式Aについて，
\models_{CL} A \iff \models_{Int} A
\models_{CL}を古典論理で妥当
\models_{Int}を直観主義論理で妥当
フレームがいずれも前順序であることを利用
\tau(A \to B) = \Box (\tau(A) \to \tau (B)) = \tau(A) \Rightarrow \tau(B)
証明
\not\models_{S4} \tau(A) \implies \not\models_{Int} A
遺伝性(直観主義論理)のズレを補正
\not\models_{Int} A\implies \not\models_{S4} \tau(A)
\tau(A)と\Box\tau(A)が同値
直観主義論理にから持ってきた命題は真ならば必然的に真であるになる
数学的命題とか
