Constructive selection principle

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