古典論理で成り立つが直観主義論理では成り立たないものの証明
用語
前提$ \Gammaから結論$ Aの推論について，
$ \Gammaは論理式の集合（$ \emptysetでもよい）
$ Aは論理式とする．
フレーム妥当性
あるKripkeフレーム$ \mathcal{F} = \lang W,\leq\rangにおいて， 直観主義論理の付値関数$ f: W \times \mathbf{Form} \to \mathbb{B}とは次を満たすものである． ある$ w \in Wについて
$ f(w,A) = 1$ \implies$ w \leq w'の任意の$ w'について$ f(w',A) = 1
次の付値関数$ fが存在するとき，前提$ \Gammaから結論$ Aへの推論はフレーム$ \mathcal{F}において妥当でないと言い，$ \Gamma \not\models^\mathcal{F} Aと表す．
ある$ w \in Wについて，
前提の中の任意の論理式$ B \in \Gammaについて$ f(w,B) = 1だが，
$ Bは世界$ wにおいて真
結論$ Aについては$ f(w,A) = 0
$ Aは世界$ wにおいて偽
そのような$ fが構成できないなら，前提$ \Gammaから結論$ Aへの推論はフレーム$ \mathcal{F}において妥当であり，$ \Gamma \models^\mathcal{F} Aと表す．
反例モデル
$ \Gamma \not\models^\mathcal{F} Aであったときの付値関数$ vをまとめたKripkeモデル$ \lang \mathcal{F}, v \rangすなわち$ \lang W,\leq, v\rangは， 「前提$ \Gammaから結論$ Aへの推論の反例モデル」と呼ばれる． 直観主義論理における妥当性
任意のKripkeフレーム$ \mathcal{F}について$ \Gamma \models^\mathcal{F} Aなら，前提$ \Gammaから結論$ Aへの推論は直観観主義論理として妥当であって$ \Gamma \models_\mathrm{IL} Aと書く． すなわち，前提$ \Gammaから結論$ Aへの推論の反例モデルが構成できないとき，直観主義論理として妥当である． 反例モデルが存在するなら，$ \Gamma \not\models_\mathrm{IL} Aと書く．
排中律: $ \not\models_\mathrm{IL} \varphi \lor \lnot\varphi 次のような反例モデル$ \mathcal{M} = \lang W,\leq, f\rang が提出される．
$ W = \{x,y\}
$ x \leq y
$ f(x,\varphi) = 0, f(y,\varphi)=1
1. $ f(y,\varphi)=1と$ x \leq yより，$ f(x,\lnot \varphi)=1である．
2. $ f(x,\varphi)=0かつ$ f(x,\lnot \varphi) = 0なので，$ f(x,\varphi\lor\lnot\varphi)=0である．
3. $ f(x,\varphi\lor\lnot\varphi)=0より，これは結論$ \varphi \lor \lnot\varphiの推論への反例モデルである．
二重否定除去: $ \lnot\lnot \varphi \not\models_\mathrm{IL} \varphi 次のような反例モデル$ \mathcal{M} = \lang W,\leq, f\rangが提出される．
$ W = \{x,y,z\}
$ x \leq y \leq z
$ f(x,\varphi) = 0, f(y,\varphi)=0, f(z,\varphi)=1とする．
1. $ f(z,\varphi) = 1と$ y \leq zより，$ f(y,\lnot\varphi) = 0である
2. $ f(y,\lnot\varphi)=0と$ x \leq yより，$ f(x,\lnot\lnot \varphi) = 1である．
3. $ f(x,\lnot\lnot \varphi) = 1と$ f(x,\varphi) = 0より，これは前提$ \lnot\lnot\varphiから結論$ \varphiの推論への反例モデルである．
対偶の除去: $ \lnot \psi \to \lnot \varphi \not\models_\mathrm{IL} \varphi \to \psi 古典論理では対偶の除去と思われている上の推論は
実際には古典論理では
1. $ \lnot \psi \to \lnot \varphi \models_\mathrm{CL} \lnot\lnot\varphi \to \lnot\lnot\psi
2. $ \lnot\lnot\varphi \models_\mathrm{CL} \varphi
の2段階を行っている．2が直観主義論理では妥当ではないことは上で二重否定除去として証明した． 1が直観主義論理で妥当かは後で検討する．