The completeness of provable realizability (Q916636): Difference between revisions

The paper gives a complete axiomatization for intuitionistic logic without disjunction but with so called strong conjunction \& which is determined by the stipulation: \(x\) realizes \(A\&B\) iff \(x\) realizes both \(A\) and \(B\). It is shown also that the provability of a formula \(A\) in this calculus coincides with the classical provability of the first order formula ``the \(\lambda\)-term \(t\) realizes the formula \(A\)''. Realizing terms here are required to be untyped and the derivation of realizability is classical.