Gödel interpretation

of intuitionistic arithmetic

A translation of formulas of intuitionistic arithmetic into formulas of the type $\exists x\forall yA(x,y,z)$, where $x$, $y$ and $z$ are variables of various finite types. Provable formulas of arithmetic are translated into provable formulas of a quantifier-free theory of finite types. Thus, this translation reduces the consistency of intuitionistic arithmetic (and hence of classical arithmetic) to that of such a theory of finite types, as was Gödel's original aim.

This type theory, call it $T$, has an infinite list of variables of each type $t$: 1) a type $0$ (the type of natural numbers); and 2) if $t_0,\dots,t_k$ are types, then $(t_0,\dots,t_k)$ is a type (the type of functions which take $k$ arguments of types $t_1,\dots,t_k$, respectively, into a value of type $t_0$). The language $T$ contains terms of various types: a variable $x^t$ of type $t$ is a term of type $t$, 0 is a term of type 0, and the symbol $s$ which denotes the function of adding one to a natural number is a term of type $(0,0)$. The remaining terms are formed by generation laws: Church $\lambda$-abstraction and primitive recursion for functions of arbitrary type. The atomic formulas of $T$ are equalities $(t=r)$, where $t$, $r$ are terms of type zero. The formulas of $T$ are obtained from atomic formulas with the aid of the logical connectives of propositional calculus: $\land$, $\lor$, $\supset$, $\neg$. The postulates of $T$ are the axioms and derivation rules of intuitionistic propositional calculus, equality axioms, the Peano axioms for 0 and $s$, equations of primitive recursion, the axiom of application of a function defined by $\lambda$-abstraction, and, finally, the principle of mathematical induction, formulated as a derivation rule without the use of quantifiers. $T^+$ will denote the theory $T$ completed by quantifiers in variables of arbitrary type and corresponding logical axioms and derivation rules for quantifiers.

Gödel's interpretation translates any formula $F$ from $T^+$ (i.e. any formula of intuitionistic arithmetic as well) into a formula of the type

$$\exists x\forall yA(x,y,z),$$

where $A(x,y,z)$ is a quantifier-free formula, $x$, $y$, $z$ are variables of different types, and $z$ is the set of all free variables of the formula $F$.

Let $F$ be a formula of intuitionistic arithmetic, and let $\exists x\forall yA(x,y,z)$ be its Gödel interpretation. If $F$ is deducible in formal intuitionistic arithmetic, it is possible to construct a term $t(z)$ of $T$ such that the formula $A(t(z),y,z)$ is deducible in $T$. Thus, the consistency of arithmetic is reduced to demonstrating the consistency of the quantifier-free theory $T$.

The intuitionistic semantics based on Gödel's interpretation is defined as follows: A formula $F$ is considered to be true if it is possible to find a computable term $t(z)$ such that the quantifier-free formula $A(t(z),y,z)$ is true for any computable $z$.

References

[1]	K. Gödel, "Ueber eine bisher noch nicht benützte Erweiterung des finiten Standpunktes" Dialectica , 12 (1958) pp. 280–287

Comments

In the West this interpretation is commonly called the Dialectica interpretation.

References

[a1]	E. Bishop, "Mathematics as a numerical language" A. Kino (ed.) J. Myhill (ed.) R.E. Vesley (ed.) , Intuitionism and Proof Theory , North-Holland (1970) pp. 53–71
[a2]	A.S. Troelstra (ed.) , Metamathematical investigations , Lect. notes in math. , 344 , Springer (1973) pp. 230ff