Namespaces
Variants
Actions

Difference between revisions of "Gödel interpretation"

From Encyclopedia of Mathematics
Jump to: navigation, search
m (moved Goedel interpretation to Gödel interpretation over redirect: accented title)
(TeX)
 
Line 1: Line 1:
 +
{{TEX|done}}
 
''of intuitionistic arithmetic''
 
''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.
+
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 <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.
+
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|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|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 <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
+
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
  
<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>
+
$$\exists x\forall yA(x,y,z),$$
  
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" />.
+
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 <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" />.
+
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 <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" />.
+
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====
 
====References====

Latest revision as of 15:15, 30 August 2014

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
How to Cite This Entry:
Gödel interpretation. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=G%C3%B6del_interpretation&oldid=23316
This article was adapted from an original article by A.G. Dragalin (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article