Namespaces
Variants
Actions

Difference between revisions of "Constructive selection principle"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
(TeX)
Line 1: Line 1:
 +
{{TEX|done}}
 
''Markov's principle''
 
''Markov's principle''
  
A logical-philosophical principle in [[Constructive mathematics|constructive mathematics]] put forth by A.A. Markov [[#References|[1]]], [[#References|[2]]] which, in its general form, asserts that if a constructive process, given by some prescription, is not potentially infinite (unboundedly extendable), then it terminates. In constructive mathematics several concrete versions of this principle are used which are equivalent in their content. 1) Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c0254101.png" /> be a [[Normal algorithm|normal algorithm]] and let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c0254102.png" /> be a word over its alphabet. If the proposition that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c0254103.png" /> is not applicable to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c0254104.png" /> is refuted, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c0254105.png" /> is applicable to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c0254106.png" />; symbolically
+
A logical-philosophical principle in [[Constructive mathematics|constructive mathematics]] put forth by A.A. Markov [[#References|[1]]], [[#References|[2]]] which, in its general form, asserts that if a constructive process, given by some prescription, is not potentially infinite (unboundedly extendable), then it terminates. In constructive mathematics several concrete versions of this principle are used which are equivalent in their content. 1) Let $\Psi$ be a [[Normal algorithm|normal algorithm]] and let $P$ be a word over its alphabet. If the proposition that $\Psi$ is not applicable to $P$ is refuted, then $\Psi$ is applicable to $P$; symbolically
  
<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/c/c025/c025410/c0254107.png" /></td> </tr></table>
+
$$\neg\neg!\Psi(P)\supset!\Psi(P).$$
  
 
2) In formal arithmetic (cf. [[Arithmetic, formal|Arithmetic, formal]]) the constructive selection principle can be expressed by the following arithmetic formula
 
2) In formal arithmetic (cf. [[Arithmetic, formal|Arithmetic, formal]]) the constructive selection principle can be expressed by the following arithmetic formula
  
<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/c/c025/c025410/c0254108.png" /></td> </tr></table>
+
$$\forall z\forall x[\neg\forall y\neg T_1(z,x,y)\supset\exists yT_1(z,x,y)],$$
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c0254109.png" /> is a primitive recursive predicate such that the partial recursive function with Gödel number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c02541010.png" /> is defined at <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c02541011.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c02541012.png" /> (cf. [[#References|[3]]]). 3) If a recursively-enumerable set is non-empty, then it contains some element. 4) Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c02541013.png" /> be an algorithmically-verifiable property of natural numbers. If the proposition that there does not exist a number with property <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c02541014.png" /> is refuted, then there is a natural number with property <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c02541015.png" />. The corresponding logical scheme is written in the form
+
where $T_1$ is a primitive recursive predicate such that the partial recursive function with Gödel number $z$ is defined at $x$ if and only if $\exists yT_1(z,x,y)$ (cf. [[#References|[3]]]). 3) If a recursively-enumerable set is non-empty, then it contains some element. 4) Let $A$ be an algorithmically-verifiable property of natural numbers. If the proposition that there does not exist a number with property $A$ is refuted, then there is a natural number with property $A$. The corresponding logical scheme is written in the form
  
<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/c/c025/c025410/c02541016.png" /></td> </tr></table>
+
$$\forall x(A(x)\lor\neg A(x))\supset(\neg\neg\exists xA(x)\supset\exists yA(y)).$$
  
Sometimes the term  "constructive selection principle"  is specially linked to this latter form of argument, since the number being sought is  "selected"  in the course of the following constructive process: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c02541017.png" /> is checked; if it is true, then 0 is selected as the required number; otherwise one proceeds to check <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c02541018.png" />; etc.
+
Sometimes the term  "constructive selection principle"  is specially linked to this latter form of argument, since the number being sought is  "selected"  in the course of the following constructive process: $A(0)$ is checked; if it is true, then 0 is selected as the required number; otherwise one proceeds to check $A(1)$; etc.
  
 
The intuitive justification of the constructive selection principle within the framework of the system of abstractions applicable in constructive mathematics consists in the following: If the impossibility of potential infinity of a given constructive process is conclusively proved, then the termination of this process is potentially attainable as a result of carrying it out sequentially, step by step. Thus, in the assertion of the existence of a [[Constructive object|constructive object]] (for example, the result of applying a normal algorithm to a word) on the basis of the constructive selection principle, one is not going beyond the framework of the abstraction of potential realizability.
 
The intuitive justification of the constructive selection principle within the framework of the system of abstractions applicable in constructive mathematics consists in the following: If the impossibility of potential infinity of a given constructive process is conclusively proved, then the termination of this process is potentially attainable as a result of carrying it out sequentially, step by step. Thus, in the assertion of the existence of a [[Constructive object|constructive object]] (for example, the result of applying a normal algorithm to a word) on the basis of the constructive selection principle, one is not going beyond the framework of the abstraction of potential realizability.
  
The constructive selection principle is absolutely admissible from the point of view of classical logic, since it is a special case of the general rule of removing a double negation and the law of the excluded middle. The application of these logical rules is reduced to the constructive selection principle in many constructions of the theory of recursive functions (cf. [[Recursive function|Recursive function]]), which make these constructions valuable in constructive mathematics. The use of the constructive selection principle also enables one to obtain a number of significant results in [[Constructive analysis|constructive analysis]], in particular the theorem on the continuity of algorithmic operators and on the extendability of effective functionals to partial recursive functionals (see also [[Constructive metric space|Constructive metric space]]). Another sphere of application of the constructive selection principle is that of constructive semantics [[#References|[4]]]. Even before the formulation of the constructive selection principle as a general principle in constructive mathematics, investigations were carried out on the basis of various forms of this principle within different constructive contexts. Here one must mention the following basic result of P.S. Novikov obtained in 1943 (see [[#References|[5]]]): Suppose that for a formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c02541019.png" /> in one variable, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c02541020.png" /> is derivable in constructive formal arithmetic for every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c02541021.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c02541022.png" /> is derivable in classical arithmetic; then the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c02541023.png" /> is derivable in constructive arithmetic. In
+
The constructive selection principle is absolutely admissible from the point of view of classical logic, since it is a special case of the general rule of removing a double negation and the law of the excluded middle. The application of these logical rules is reduced to the constructive selection principle in many constructions of the theory of recursive functions (cf. [[Recursive function|Recursive function]]), which make these constructions valuable in constructive mathematics. The use of the constructive selection principle also enables one to obtain a number of significant results in [[Constructive analysis|constructive analysis]], in particular the theorem on the continuity of algorithmic operators and on the extendability of effective functionals to partial recursive functionals (see also [[Constructive metric space|Constructive metric space]]). Another sphere of application of the constructive selection principle is that of constructive semantics [[#References|[4]]]. Even before the formulation of the constructive selection principle as a general principle in constructive mathematics, investigations were carried out on the basis of various forms of this principle within different constructive contexts. Here one must mention the following basic result of P.S. Novikov obtained in 1943 (see [[#References|[5]]]): Suppose that for a formula $A(x)$ in one variable, $A(n)\lor\neg A(n)$ is derivable in constructive formal arithmetic for every $n$ and $\exists xA(x)$ is derivable in classical arithmetic; then the formula $\exists xA(x)$ is derivable in constructive arithmetic. In
  
 
a justification of the constructive selection principle was obtained within the framework of a new system of constructive semantics, subsequently developed by Markov.
 
a justification of the constructive selection principle was obtained within the framework of a new system of constructive semantics, subsequently developed by Markov.
Line 28: Line 29:
  
 
====References====
 
====References====
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  A.A. Markov,  "On the continuity of constructive functions"  ''Uspekhi Mat. Nauk'' , '''9''' :  3  (1934)  pp. 226–230  (In Russian)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  A.A. Markov,  "On a principle of constructive mathematical logic" , ''Proc. 3-th All-Union Math. Congress'' , '''2''' , Moscow  (1956)  pp. 146–147  (In Russian)</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  S.C. Kleene,  "Introduction to metamathematics" , North-Holland  (1951)</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  N.A. Shanin,  "On the constructive understanding of mathematical reasonings"  ''Trudy Mat. Inst. Steklov.'' , '''52'''  (1958)  pp. 226–311  (In Russian)</TD></TR><TR><TD valign="top">[5]</TD> <TD valign="top">  P.S. Novikov,  "On the consistency of certain logical calculus"  ''Mat. Sb.'' , '''12''' :  2  (1943)  pp. 231–261  (In Russian)</TD></TR><TR><TD valign="top">[6a]</TD> <TD valign="top">  A.A. Markov,  "On the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c02541024.png" />"  ''Soviet Math. Doklady'' , '''15'''  (1974)  pp. 242–246  ''Dokl. Akad. Nauk SSSR'' , '''214''' :  4  (1974)  pp. 765–768</TD></TR><TR><TD valign="top">[6b]</TD> <TD valign="top">  A.A. Markov,  "On the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025410/c02541025.png" />"  ''Soviet Math. Doklady'' , '''15'''  (1974)  pp. 443–447  ''Dokl. Akad. Nauk SSSR'' , '''215''' :  1  (1974)  pp. 57–60</TD></TR><TR><TD valign="top">[7]</TD> <TD valign="top">  S.C. Kleene,  R.E. Vesley,  "The foundations of intuitionistic mathematics: especially in relation to recursive functions" , North-Holland  (1965)</TD></TR><TR><TD valign="top">[8]</TD> <TD valign="top">  A.S. Troelstra,  "Markov's principle and Markov's rule for theories of choice sequences" , ''ISILC. Proof theory symposium'' , ''Lect. notes in math.'' , '''500''' , Springer  (1975)  pp. 370–383</TD></TR></table>
+
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  A.A. Markov,  "On the continuity of constructive functions"  ''Uspekhi Mat. Nauk'' , '''9''' :  3  (1934)  pp. 226–230  (In Russian)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  A.A. Markov,  "On a principle of constructive mathematical logic" , ''Proc. 3-th All-Union Math. Congress'' , '''2''' , Moscow  (1956)  pp. 146–147  (In Russian)</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  S.C. Kleene,  "Introduction to metamathematics" , North-Holland  (1951)</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  N.A. Shanin,  "On the constructive understanding of mathematical reasonings"  ''Trudy Mat. Inst. Steklov.'' , '''52'''  (1958)  pp. 226–311  (In Russian)</TD></TR><TR><TD valign="top">[5]</TD> <TD valign="top">  P.S. Novikov,  "On the consistency of certain logical calculus"  ''Mat. Sb.'' , '''12''' :  2  (1943)  pp. 231–261  (In Russian)</TD></TR><TR><TD valign="top">[6a]</TD> <TD valign="top">  A.A. Markov,  "On the language $Ya_3$"  ''Soviet Math. Doklady'' , '''15'''  (1974)  pp. 242–246  ''Dokl. Akad. Nauk SSSR'' , '''214''' :  4  (1974)  pp. 765–768</TD></TR><TR><TD valign="top">[6b]</TD> <TD valign="top">  A.A. Markov,  "On the language $Ya_\omega$"  ''Soviet Math. Doklady'' , '''15'''  (1974)  pp. 443–447  ''Dokl. Akad. Nauk SSSR'' , '''215''' :  1  (1974)  pp. 57–60</TD></TR><TR><TD valign="top">[7]</TD> <TD valign="top">  S.C. Kleene,  R.E. Vesley,  "The foundations of intuitionistic mathematics: especially in relation to recursive functions" , North-Holland  (1965)</TD></TR><TR><TD valign="top">[8]</TD> <TD valign="top">  A.S. Troelstra,  "Markov's principle and Markov's rule for theories of choice sequences" , ''ISILC. Proof theory symposium'' , ''Lect. notes in math.'' , '''500''' , Springer  (1975)  pp. 370–383</TD></TR></table>

Revision as of 12:58, 19 August 2014

Markov's principle

A logical-philosophical principle in constructive mathematics put forth by A.A. Markov [1], [2] which, in its general form, asserts that if a constructive process, given by some prescription, is not potentially infinite (unboundedly extendable), then it terminates. In constructive mathematics several concrete versions of this principle are used which are equivalent in their content. 1) Let $\Psi$ be a normal algorithm and let $P$ be a word over its alphabet. If the proposition that $\Psi$ is not applicable to $P$ is refuted, then $\Psi$ is applicable to $P$; symbolically

$$\neg\neg!\Psi(P)\supset!\Psi(P).$$

2) In formal arithmetic (cf. Arithmetic, formal) the constructive selection principle can be expressed by the following arithmetic formula

$$\forall z\forall x[\neg\forall y\neg T_1(z,x,y)\supset\exists yT_1(z,x,y)],$$

where $T_1$ is a primitive recursive predicate such that the partial recursive function with Gödel number $z$ is defined at $x$ if and only if $\exists yT_1(z,x,y)$ (cf. [3]). 3) If a recursively-enumerable set is non-empty, then it contains some element. 4) Let $A$ be an algorithmically-verifiable property of natural numbers. If the proposition that there does not exist a number with property $A$ is refuted, then there is a natural number with property $A$. The corresponding logical scheme is written in the form

$$\forall x(A(x)\lor\neg A(x))\supset(\neg\neg\exists xA(x)\supset\exists yA(y)).$$

Sometimes the term "constructive selection principle" is specially linked to this latter form of argument, since the number being sought is "selected" in the course of the following constructive process: $A(0)$ is checked; if it is true, then 0 is selected as the required number; otherwise one proceeds to check $A(1)$; etc.

The intuitive justification of the constructive selection principle within the framework of the system of abstractions applicable in constructive mathematics consists in the following: If the impossibility of potential infinity of a given constructive process is conclusively proved, then the termination of this process is potentially attainable as a result of carrying it out sequentially, step by step. Thus, in the assertion of the existence of a constructive object (for example, the result of applying a normal algorithm to a word) on the basis of the constructive selection principle, one is not going beyond the framework of the abstraction of potential realizability.

The constructive selection principle is absolutely admissible from the point of view of classical logic, since it is a special case of the general rule of removing a double negation and the law of the excluded middle. The application of these logical rules is reduced to the constructive selection principle in many constructions of the theory of recursive functions (cf. Recursive function), which make these constructions valuable in constructive mathematics. The use of the constructive selection principle also enables one to obtain a number of significant results in constructive analysis, in particular the theorem on the continuity of algorithmic operators and on the extendability of effective functionals to partial recursive functionals (see also Constructive metric space). Another sphere of application of the constructive selection principle is that of constructive semantics [4]. Even before the formulation of the constructive selection principle as a general principle in constructive mathematics, investigations were carried out on the basis of various forms of this principle within different constructive contexts. Here one must mention the following basic result of P.S. Novikov obtained in 1943 (see [5]): Suppose that for a formula $A(x)$ in one variable, $A(n)\lor\neg A(n)$ is derivable in constructive formal arithmetic for every $n$ and $\exists xA(x)$ is derivable in classical arithmetic; then the formula $\exists xA(x)$ is derivable in constructive arithmetic. In

a justification of the constructive selection principle was obtained within the framework of a new system of constructive semantics, subsequently developed by Markov.

Being apparently one of the least direct of the initial statements in constructive mathematics, the constructive selection principle has been applied by some advocates with known reservations. The constructive selection principle is also rejected by intuitionists as being insufficiently convincing from an intuitive point of view. On the other hand, in connection with the formalization of a number of branches of intuitionistic mathematics, one has studied in detail questions on the relation between corresponding systems with formal schemes expressing the constructive selection principle. In particular, it has been established that the schemes

and

are independent of the axioms of intuitionistic predicate calculus, arithmetic and analysis (see [2], [7], [8]).

References

[1] A.A. Markov, "On the continuity of constructive functions" Uspekhi Mat. Nauk , 9 : 3 (1934) pp. 226–230 (In Russian)
[2] A.A. Markov, "On a principle of constructive mathematical logic" , Proc. 3-th All-Union Math. Congress , 2 , Moscow (1956) pp. 146–147 (In Russian)
[3] S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[4] N.A. Shanin, "On the constructive understanding of mathematical reasonings" Trudy Mat. Inst. Steklov. , 52 (1958) pp. 226–311 (In Russian)
[5] P.S. Novikov, "On the consistency of certain logical calculus" Mat. Sb. , 12 : 2 (1943) pp. 231–261 (In Russian)
[6a] A.A. Markov, "On the language $Ya_3$" Soviet Math. Doklady , 15 (1974) pp. 242–246 Dokl. Akad. Nauk SSSR , 214 : 4 (1974) pp. 765–768
[6b] A.A. Markov, "On the language $Ya_\omega$" Soviet Math. Doklady , 15 (1974) pp. 443–447 Dokl. Akad. Nauk SSSR , 215 : 1 (1974) pp. 57–60
[7] S.C. Kleene, R.E. Vesley, "The foundations of intuitionistic mathematics: especially in relation to recursive functions" , North-Holland (1965)
[8] A.S. Troelstra, "Markov's principle and Markov's rule for theories of choice sequences" , ISILC. Proof theory symposium , Lect. notes in math. , 500 , Springer (1975) pp. 370–383
How to Cite This Entry:
Constructive selection principle. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Constructive_selection_principle&oldid=18265
This article was adapted from an original article by B.A. Kushner (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article