直観主義命題論理のHarrop選言特性
参考文献
remark
$ \lnot \varphiは$ \varphiが何であれHarrop論理式である:$ \lnot \varphi \equiv \varphi \to \botだから $ \Gamma \vdash A \lor Bならば$ \Gamma \vdash Aまたは$ \Gamma \vdash B
この結果は強められる↓.
proof
モーダスポネンスの場合
$ T \vdash \varphi \to \psi \lor \xiと$ T \vdash \varphiによって$ T \vdash \psi \lor \xiだったとする
帰納法の仮定