View source for Gödel interpretation

''of intuitionistic arithmetic''

A translation of formulas of intuitionistic arithmetic into formulas of the type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g0445401.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g0445402.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g0445403.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g0445404.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g0445405.png" />, has an infinite list of variables of each type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g0445406.png" />: 1) a type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g0445407.png" /> (the type of natural numbers); and 2) if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g0445408.png" /> are types, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g0445409.png" /> is a type (the type of functions which take <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454010.png" /> arguments of types <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454011.png" />, respectively, into a value of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454012.png" />). The language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454013.png" /> contains terms of various types: a variable <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454014.png" /> of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454015.png" /> is a term of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454016.png" />, 0 is a term of type 0, and the symbol <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454017.png" /> which denotes the function of adding one to a natural number is a term of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454018.png" />. The remaining terms are formed by generation laws: [[Church lambda-abstraction|Church <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454019.png" />-abstraction]] and primitive recursion for functions of arbitrary type. The atomic formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454020.png" /> are equalities <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454021.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454022.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454023.png" /> are terms of type zero. The formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454024.png" /> are obtained from atomic formulas with the aid of the logical connectives of propositional calculus: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454025.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454026.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454027.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454028.png" />. The postulates of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454029.png" /> are the axioms and derivation rules of intuitionistic propositional calculus, equality axioms, the [[Peano axioms|Peano axioms]] for 0 and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454030.png" />, equations of primitive recursion, the axiom of application of a function defined by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454031.png" />-abstraction, and, finally, the principle of mathematical induction, formulated as a derivation rule without the use of quantifiers. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454032.png" /> will denote the theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454033.png" /> completed by quantifiers in variables of arbitrary type and corresponding logical axioms and derivation rules for quantifiers.

Gödel's interpretation translates any formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454034.png" /> from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454035.png" /> (i.e. any formula of intuitionistic arithmetic as well) into a formula of the type

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454036.png" /></td> </tr></table>

where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454037.png" /> is a quantifier-free formula, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454038.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454039.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454040.png" /> are variables of different types, and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454041.png" /> is the set of all free variables of the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454042.png" />.

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454043.png" /> be a formula of intuitionistic arithmetic, and let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454044.png" /> be its Gödel interpretation. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454045.png" /> is deducible in formal intuitionistic arithmetic, it is possible to construct a term <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454046.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454047.png" /> such that the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454048.png" /> is deducible in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454049.png" />. Thus, the consistency of arithmetic is reduced to demonstrating the consistency of the quantifier-free theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454050.png" />.

The intuitionistic semantics based on Gödel's interpretation is defined as follows: A formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454051.png" /> is considered to be true if it is possible to find a computable term <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454052.png" /> such that the quantifier-free formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454053.png" /> is true for any computable <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g044/g044540/g04454054.png" />.

====References====
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  K. Gödel,   "Ueber eine bisher noch nicht benützte Erweiterung des finiten Standpunktes"  ''Dialectica'' , '''12'''  (1958)  pp. 280–287</TD></TR></table>



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

====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  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</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  A.S. Troelstra (ed.) , ''Metamathematical investigations'' , ''Lect. notes in math.'' , '''344''' , Springer  (1973)  pp. 230ff</TD></TR></table>