直観主義論理での否定の扱われ方

直観主義論理における否定は次の定義である

$ v(x,\lnot A) = 1$ \iff$ x\leq yとなる全ての$ yについて$ v(y,A)=0

まず，直観主義論理のモデルにおいて次は成り立たない

$ v(x,\lnot p) =1 \iff v(x,p)= 0

例えば次

https://gyazo.com/2013675207f665fd331d8d9a14da5425

$ v(x,p)=0で$ v(x,\lnot p)=0

$ x \leq yのある$ yで$ p(y,A)=1

以下ミスの可能性がある

$ v(x,\lnot p) = 0

$ \iff$ x\leq yとなるある$ yについて$ v(y,p)=1

二重否定導入は妥当である

$ A \models \lnot\lnot A

ある直観主義論理のモデル$ \lang W,\leq,v \rangのある$ xについて

$ Aが真で$ \lnot\lnot Aが偽

つまり

$ v(x,A)=1

$ v(x,\lnot\lnot A) = 0

$ v(\lnot\lnot A)=0

$ \iff$ x\leq yのある$ yで$ v(y,\lnot A) = 1

$ v(\lnot A) = 1

$ \iff$ y\leq zの全ての$ zで$ v(z,A)=0

反射律より$ z = y = xとしてよく，$ v(x,A)=0

これが$ v(x,A)=1と矛盾する

したがってそんな反例モデルは作れない

二重否定除去は妥当でない

$ \lnot\lnot A \not\models A

反例モデルは次のよう

$ v(x,\lnot\lnot A) = 1

$ v(x,A)=0

https://gyazo.com/2f9a92455f023f596faf6b23c8037dde

反例モデルを作ることはできる

ある直観主義論理のモデル$ \lang W,\leq,v \rangのある$ xについて

$ \lnot\lnot Aが真で$ Aが偽

つまり

$ v(x,\lnot\lnot A) = 1

$ v(x,A)=0

$ v(x,\lnot\lnot A) = 1

$ \iff$ x \leq yの全$ yで$ v(y,\lnot A) = 0

$ v(y, \lnot A) = 0

$ \iff$ y \leq zのある$ zで$ v(z,A)=1

三重否定除去は妥当

$ \lnot\lnot\lnot A \models \lnot A

ある直観主義論理のモデル$ \lang W,\leq,v \rangのある$ xについて

$ \lnot\lnot\lnot Aが真で$ \lnot Aが偽

つまり

$ v(x,\lnot\lnot\lnot A) = 1

$ v(x,\lnot A) = 0

$ v(\lnot\lnot\lnot A) = 1

$ \iff$ x\leq yの全ての$ yで$ v(y,\lnot\lnot A) = 0

$ v(\lnot\lnot A) = 0

$ \iff$ y \leq zのある$ zで$ v(z,\lnot A) = 1

反射律から$ x = y = zとしてよく，$ v(x,\lnot A) = 1

これが$ v(x,\lnot A) = 0と矛盾する

したがってそんな反例モデルは作れない

$ \lnot\lnot\lnot A \models \lnot A

三重否定導入は妥当

$ \lnot A \models \lnot\lnot\lnot A

除去の証明をひっくり返せばOK