弁証法解釈

数量詞を含まない式${\displaystyle A_{D}(x;y)}$は、論理構造に基づいて帰納的に定義される。${\displaystyle A}$以下のように、${\displaystyle P}$原子式は

${\displaystyle {\begin{array}{lcl}(P)_{D}&\equiv &P\\(A\wedge B)_{D}(x,v;y,w)&\equiv &A_{D}(x;y)\wedge B_{D}(v;w)\\(A\vee B)_{D}(x,v,z;y,w)&\equiv &(z=0\rightarrow A_{D}(x;y))\wedge (z\neq 0\to B_{D}(v;w))\\(A\rightarrow B)_{D}(f,g;x,w)&\equiv &A_{D}(x;fxw)\rightarrow B_{D}(gx;w)\\(\exists zA)_{D}(x,z;y)&\equiv &A_{D}(x;y)\\(\forall zA)_{D}(f;y,z)&\equiv &A_{D}(fz;y)\end{array}}}$

式の解釈は、${\displaystyle A}$ハイティング算術で証明可能であれば、閉項列が存在する。${\displaystyle t}$そのため${\displaystyle A_{D}(t;y)}$システム T において証明可能である。項の列${\displaystyle t}$そしてその証明${\displaystyle A_{D}(t;y)}$与えられた証明から構築される${\displaystyle A}$ハイティング算術において。${\displaystyle t}$縮約公理を除けば、非常に単純明快である。${\displaystyle A\rightarrow A\wedge A}$これは、量化子を含まない論理式が決定可能であるという仮定を必要とする。

また、ハイティング算術は以下の原理によって拡張されることも示されている。

• 選択の公理
• マルコフの原理
• 普遍的な公式の前提の独立性

これは、弁証法解釈によって解釈可能なHAの式を特徴づけるために必要かつ十分である。 ここでの選択公理は、前提にある任意の2項述語と、結論にある関数型の変数を含む存在主張に対して定式化される。

直観主義論理の基本的な弁証法解釈は、より強力な様々な体系へと拡張されてきた。直観的に言えば、追加原理の弁証法解釈が体系T（または体系Tの拡張）の項によって証明できる限り、弁証法解釈はより強力な体系にも適用できる。