Namespaces
Variants
Actions

Difference between revisions of "Recursive realizability"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
m (tex encoded by computer)
 
Line 1: Line 1:
A more precise definition of the intuitionistic semantics of arithmetical formulas, based on the concept of a [[Partial recursive function|partial recursive function]] as proposed by S.C. Kleene (see [[#References|[1]]], [[#References|[2]]]). For every closed arithmetical formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r0803101.png" />, a relation  "the natural number e realizes the formula F"  is defined; it is denoted by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r0803102.png" />. The relation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r0803103.png" /> is defined inductively according to the structure of the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r0803104.png" />.
+
<!--
 +
r0803101.png
 +
$#A+1 = 64 n = 0
 +
$#C+1 = 64 : ~/encyclopedia/old_files/data/R080/R.0800310 Recursive realizability
 +
Automatically converted into TeX, above some diagnostics.
 +
Please remove this comment and the {{TEX|auto}} line below,
 +
if TeX found to be correct.
 +
-->
  
1) If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r0803105.png" /> is an atomic formula without free variables, i.e. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r0803106.png" /> is of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r0803107.png" /> where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r0803108.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r0803109.png" /> are constant terms, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031010.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031011.png" /> and the values of the terms <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031012.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031013.png" /> coincide.
+
{{TEX|auto}}
 +
{{TEX|done}}
  
Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031014.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031015.png" /> be formulas without free variables.
+
A more precise definition of the intuitionistic semantics of arithmetical formulas, based on the concept of a [[Partial recursive function|partial recursive function]] as proposed by S.C. Kleene (see [[#References|[1]]], [[#References|[2]]]). For every closed arithmetical formula  $  F $,
 +
a relation  "the natural number e realizes the formula F" is defined; it is denoted by  $  erF $.  
 +
The relation  $  erF $
 +
is defined inductively according to the structure of the formula  $  F $.
  
2) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031016.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031017.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031018.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031019.png" />.
+
1) If  $  F $
 +
is an atomic formula without free variables, i.e. $  F $
 +
is of the form  $  s= t $
 +
where  $  s $
 +
and  $  t $
 +
are constant terms, then  $  erF $
 +
if and only if $  e= 0 $
 +
and the values of the terms  $  s $
 +
and  $  t $
 +
coincide.
  
3) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031020.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031021.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031022.png" />, or <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031023.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031024.png" />.
+
Let  $  A $
 +
and $  B $
 +
be formulas without free variables.
  
4) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031025.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031026.png" /> is the Gödel number of a unary partial recursive function <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031027.png" /> such that for any natural number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031028.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031029.png" /> implies that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031030.png" /> is defined at <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031031.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031032.png" />.
+
2) $  er( A \& B) $
 +
if and only if $  e = 2  ^ {a} \cdot 3  ^ {b} $,
 +
where  $  arA $,  
 +
$  brB $.
  
5) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031033.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031034.png" />.
+
3) $  er( A \lor B) $
 +
if and only if $  e = 2  ^ {0} \cdot 3  ^ {a} $
 +
and  $  arA $,
 +
or  $  e = 2  ^ {1} \cdot 3  ^ {b} $
 +
and  $  brB $.
  
Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031035.png" /> be a formula without free variables other than <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031036.png" />; if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031037.png" /> is a natural number, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031038.png" /> is a term which denotes the number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031039.png" /> in formal arithmetic.
+
4)  $  er( A \supset B) $
 +
if and only if $  e $
 +
is the Gödel number of a unary partial recursive function  $  \phi $
 +
such that for any natural number $  a $,  
 +
$  arA $
 +
implies that  $  \phi $
 +
is defined at  $  a $
 +
and  $  \phi ( a) rB $.
  
6) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031040.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031041.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031042.png" />.
+
5) $  er( \neg A) $
 +
if and only if $  er( A \supset 1= 0) $.
  
7) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031043.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031044.png" /> is the Gödel number of a [[Recursive function|recursive function]] <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031045.png" /> such that for any natural number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031046.png" /> the number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031047.png" /> realizes <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031048.png" />.
+
Let  $  A( x) $
 +
be a formula without free variables other than  $  x $;
 +
if $  n $
 +
is a natural number, then  $  \overline{n}\; $
 +
is a term which denotes the number $  n $
 +
in formal arithmetic.
  
A closed formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031049.png" /> is called realizable if there is a number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031050.png" /> which realizes <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031051.png" />. A formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031052.png" /> containing the free variables <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031053.png" /> can be regarded as a predicate in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031054.png" /> ( "the formula Ay1…ym is realizable" ). If a formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031055.png" /> is derivable from realizable formulas in [[Intuitionistic arithmetic|intuitionistic arithmetic]], then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031056.png" /> is realizable (see [[#References|[3]]]). In particular, every formula which can be proved in intuitionistic arithmetic is realizable. A formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031057.png" /> can be given for which the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031058.png" /> is not realizable. Accordingly, in this case the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031059.png" /> is realizable although it is classically false.
+
6)  $  er( \exists xA( x)) $
 +
if and only if $  e = 2  ^ {n} \cdot 3  ^ {a} $
 +
and  $  arA( \overline{n}\; ) $.
  
Every predicate formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031060.png" /> which is provable in intuitionistic predicate calculus has the property that each arithmetical formula obtained from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031061.png" /> by substitution is realizable. Predicate formulas possessing this property are called realizable. It has been shown [[#References|[4]]] that the propositional formula:
+
7)  $  er( \forall xA( x)) $
 +
if and only if  $  e $
 +
is the Gödel number of a [[Recursive function|recursive function]] $  f $
 +
such that for any natural number  $  n $
 +
the number  $  f( n) $
 +
realizes  $  A( \overline{n}\; ) $.
  
<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/r/r080/r080310/r08031062.png" /></td> </tr></table>
+
A closed formula  $  F $
 +
is called realizable if there is a number  $  e $
 +
which realizes  $  F $.
 +
A formula  $  A( y _ {1} \dots y _ {m} ) $
 +
containing the free variables  $  y _ {1} \dots y _ {m} $
 +
can be regarded as a predicate in  $  y _ {1} \dots y _ {m} $(
 +
"the formula Ay1…ym is realizable" ). If a formula  $  F $
 +
is derivable from realizable formulas in [[Intuitionistic arithmetic|intuitionistic arithmetic]], then  $  F $
 +
is realizable (see [[#References|[3]]]). In particular, every formula which can be proved in intuitionistic arithmetic is realizable. A formula  $  A( x) $
 +
can be given for which the formula  $  \forall x ( A( x) \lor \neg A( x)) $
 +
is not realizable. Accordingly, in this case the formula  $  \neg \forall x( A( x) \lor \neg A( x)) $
 +
is realizable although it is classically false.
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031063.png" /> denotes the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080310/r08031064.png" />, is realizable but cannot be derived in [[Intuitionistic propositional calculus|intuitionistic propositional calculus]].
+
Every predicate formula  $  \mathfrak U $
 +
which is provable in intuitionistic predicate calculus has the property that each arithmetical formula obtained from  $  \mathfrak U $
 +
by substitution is realizable. Predicate formulas possessing this property are called realizable. It has been shown [[#References|[4]]] that the propositional formula:
 +
 
 +
$$
 +
(( \neg \neg D \supset D)  \supset  ( \neg \neg D \lor \neg D))  \supset  ( \neg \neg D \lor
 +
\neg D),
 +
$$
 +
 
 +
where  $  D $
 +
denotes the formula $  \neg p \lor \neg q $,  
 +
is realizable but cannot be derived in [[Intuitionistic propositional calculus|intuitionistic propositional calculus]].
  
 
====References====
 
====References====
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  S.C. Kleene,  "On the interpretation of intuitionistic number theory"  ''J. Symbolic Logic'' , '''10'''  (1945)  pp. 109–124</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  S.C. Kleene,  "Introduction to metamathematics" , North-Holland  (1951)</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  D. Nelson,  "Recursive functions and intuitionistic number theory"  ''Trans. Amer. Math. Soc.'' , '''61'''  (1947)  pp. 307–368</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  G.F. Rose,  "Propositional calculus and realizability"  ''Trans. Amer. Math. Soc.'' , '''75'''  (1953)  pp. 1–19</TD></TR><TR><TD valign="top">[5]</TD> <TD valign="top">  P.S. Novikov,  "Constructive mathematical logic from a classical point of view" , Moscow  (1977)  (In Russian)</TD></TR></table>
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  S.C. Kleene,  "On the interpretation of intuitionistic number theory"  ''J. Symbolic Logic'' , '''10'''  (1945)  pp. 109–124</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  S.C. Kleene,  "Introduction to metamathematics" , North-Holland  (1951)</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  D. Nelson,  "Recursive functions and intuitionistic number theory"  ''Trans. Amer. Math. Soc.'' , '''61'''  (1947)  pp. 307–368</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  G.F. Rose,  "Propositional calculus and realizability"  ''Trans. Amer. Math. Soc.'' , '''75'''  (1953)  pp. 1–19</TD></TR><TR><TD valign="top">[5]</TD> <TD valign="top">  P.S. Novikov,  "Constructive mathematical logic from a classical point of view" , Moscow  (1977)  (In Russian)</TD></TR></table>
 
 
  
 
====Comments====
 
====Comments====
 
  
 
====References====
 
====References====
 
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  M.J. Beeson,  "Foundations of constructive mathematics" , Springer  (1985)</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  D. Mumford,  "Abelian varieties" , Oxford Univ. Press  (1974)</TD></TR></table>
 
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  M.J. Beeson,  "Foundations of constructive mathematics" , Springer  (1985)</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  D. Mumford,  "Abelian varieties" , Oxford Univ. Press  (1974)</TD></TR></table>

Latest revision as of 08:10, 6 June 2020


A more precise definition of the intuitionistic semantics of arithmetical formulas, based on the concept of a partial recursive function as proposed by S.C. Kleene (see [1], [2]). For every closed arithmetical formula $ F $, a relation "the natural number e realizes the formula F" is defined; it is denoted by $ erF $. The relation $ erF $ is defined inductively according to the structure of the formula $ F $.

1) If $ F $ is an atomic formula without free variables, i.e. $ F $ is of the form $ s= t $ where $ s $ and $ t $ are constant terms, then $ erF $ if and only if $ e= 0 $ and the values of the terms $ s $ and $ t $ coincide.

Let $ A $ and $ B $ be formulas without free variables.

2) $ er( A \& B) $ if and only if $ e = 2 ^ {a} \cdot 3 ^ {b} $, where $ arA $, $ brB $.

3) $ er( A \lor B) $ if and only if $ e = 2 ^ {0} \cdot 3 ^ {a} $ and $ arA $, or $ e = 2 ^ {1} \cdot 3 ^ {b} $ and $ brB $.

4) $ er( A \supset B) $ if and only if $ e $ is the Gödel number of a unary partial recursive function $ \phi $ such that for any natural number $ a $, $ arA $ implies that $ \phi $ is defined at $ a $ and $ \phi ( a) rB $.

5) $ er( \neg A) $ if and only if $ er( A \supset 1= 0) $.

Let $ A( x) $ be a formula without free variables other than $ x $; if $ n $ is a natural number, then $ \overline{n}\; $ is a term which denotes the number $ n $ in formal arithmetic.

6) $ er( \exists xA( x)) $ if and only if $ e = 2 ^ {n} \cdot 3 ^ {a} $ and $ arA( \overline{n}\; ) $.

7) $ er( \forall xA( x)) $ if and only if $ e $ is the Gödel number of a recursive function $ f $ such that for any natural number $ n $ the number $ f( n) $ realizes $ A( \overline{n}\; ) $.

A closed formula $ F $ is called realizable if there is a number $ e $ which realizes $ F $. A formula $ A( y _ {1} \dots y _ {m} ) $ containing the free variables $ y _ {1} \dots y _ {m} $ can be regarded as a predicate in $ y _ {1} \dots y _ {m} $( "the formula Ay1…ym is realizable" ). If a formula $ F $ is derivable from realizable formulas in intuitionistic arithmetic, then $ F $ is realizable (see [3]). In particular, every formula which can be proved in intuitionistic arithmetic is realizable. A formula $ A( x) $ can be given for which the formula $ \forall x ( A( x) \lor \neg A( x)) $ is not realizable. Accordingly, in this case the formula $ \neg \forall x( A( x) \lor \neg A( x)) $ is realizable although it is classically false.

Every predicate formula $ \mathfrak U $ which is provable in intuitionistic predicate calculus has the property that each arithmetical formula obtained from $ \mathfrak U $ by substitution is realizable. Predicate formulas possessing this property are called realizable. It has been shown [4] that the propositional formula:

$$ (( \neg \neg D \supset D) \supset ( \neg \neg D \lor \neg D)) \supset ( \neg \neg D \lor \neg D), $$

where $ D $ denotes the formula $ \neg p \lor \neg q $, is realizable but cannot be derived in intuitionistic propositional calculus.

References

[1] S.C. Kleene, "On the interpretation of intuitionistic number theory" J. Symbolic Logic , 10 (1945) pp. 109–124
[2] S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[3] D. Nelson, "Recursive functions and intuitionistic number theory" Trans. Amer. Math. Soc. , 61 (1947) pp. 307–368
[4] G.F. Rose, "Propositional calculus and realizability" Trans. Amer. Math. Soc. , 75 (1953) pp. 1–19
[5] P.S. Novikov, "Constructive mathematical logic from a classical point of view" , Moscow (1977) (In Russian)

Comments

References

[a1] M.J. Beeson, "Foundations of constructive mathematics" , Springer (1985)
[a2] D. Mumford, "Abelian varieties" , Oxford Univ. Press (1974)
How to Cite This Entry:
Recursive realizability. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Recursive_realizability&oldid=48460
This article was adapted from an original article by V.E. Plisko (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article