Markov's principle
Encyclopedia
Markov's principle, named after Andrey Markov Jr
, is a classical tautology
that is not intuitionistically
valid but that may be justified by constructive
means.
There are many equivalent formulations of Markov's principle.
, Markov's principle is a formal expression of the claim that if it is impossible that an algorithm does not terminate, then it does terminate. This is equivalent to the claim that if a set and its complement are both computably enumerable, then the set is decidable
.
In predicate logic
, if P is a predicate over the natural number
s, it is expressed as:
That is, if P is decidable, and it cannot be false for every natural number n, then it is true for some n. (In general, a predicate P over some domain is called decidable if for every x in the domain, either P(x) is true, or P(x) is not true, which is not always the case constructively.)
It is equivalent in the language of arithmetic
to:
for
a total recursive function
on the natural numbers.
It is equivalent, in the language of real analysis
, to the following principles:
can be used to justify Markov's principle: a realizer is the unbounded search that successively checks if
is true. Because 
is not everywhere false, the search cannot go on forever. Using classical logic one concludes that the search therefore stops, namely at a value at which 
holds.
Modified realizability
does not justify Markov's principle, even if classical logic is used in the meta-theory: there is no realizer in the language of simply typed lambda calculus
as this language is not Turing-complete and arbitrary loops cannot be defined in it.
is derivable as soon as 
is, for 
decidable. The logician Harvey Friedman
showed that Markov's rule is an admissible rule
in intuitionistic logic
, Heyting arithmetic
, and various other intuitionistic theories, using the Friedman translation
.
This form can be justified by Brouwer's continuity principles, whereas the stronger form contradicts them. Thus it can be derived from intuitionistic, realizability, and classical reasoning, in each case for different reasons, but this principle is not valid in the general constructive sense of Bishop.
Andrey Markov (Soviet mathematician)
Andrey Andreyevich Markov Jr. was a Soviet mathematician, the son of the great Russian mathematician Andrey Andreyevich Markov Sr, and one of the key founders of the Russian school of constructive mathematics and logic...
, is a classical tautology
Tautology (logic)
In logic, a tautology is a formula which is true in every possible interpretation. Philosopher Ludwig Wittgenstein first applied the term to redundancies of propositional logic in 1921; it had been used earlier to refer to rhetorical tautologies, and continues to be used in that alternate sense...
that is not intuitionistically
Intuitionistic logic
Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
valid but that may be justified by constructive
Constructivism (mathematics)
In the philosophy of mathematics, constructivism asserts that it is necessary to find a mathematical object to prove that it exists. When one assumes that an object does not exist and derives a contradiction from that assumption, one still has not found the object and therefore not proved its...
means.
There are many equivalent formulations of Markov's principle.
Statements of the principle
In the language of computability theoryComputability theory
Computability theory, also called recursion theory, is a branch of mathematical logic that originated in the 1930s with the study of computable functions and Turing degrees. The field has grown to include the study of generalized computability and definability...
, Markov's principle is a formal expression of the claim that if it is impossible that an algorithm does not terminate, then it does terminate. This is equivalent to the claim that if a set and its complement are both computably enumerable, then the set is decidable
Recursive set
In computability theory, a set of natural numbers is called recursive, computable or decidable if there is an algorithm which terminates after a finite amount of time and correctly decides whether or not a given number belongs to the set....
.
In predicate logic
Predicate logic
In mathematical logic, predicate logic is the generic term for symbolic formal systems like first-order logic, second-order logic, many-sorted logic or infinitary logic. This formal system is distinguished from other systems in that its formulae contain variables which can be quantified...
, if P is a predicate over the natural number
Natural number
In mathematics, the natural numbers are the ordinary whole numbers used for counting and ordering . These purposes are related to the linguistic notions of cardinal and ordinal numbers, respectively...
s, it is expressed as:
That is, if P is decidable, and it cannot be false for every natural number n, then it is true for some n. (In general, a predicate P over some domain is called decidable if for every x in the domain, either P(x) is true, or P(x) is not true, which is not always the case constructively.)
It is equivalent in the language of arithmetic
Heyting arithmetic
In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it....
to:
for
a total recursive functionComputable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm. They are used to discuss computability without referring to any concrete model of computation such as Turing machines or register...
on the natural numbers.
It is equivalent, in the language of real analysis
Real analysis
Real analysis, is a branch of mathematical analysis dealing with the set of real numbers and functions of a real variable. In particular, it deals with the analytic properties of real functions and sequences, including convergence and limits of sequences of real numbers, the calculus of the real...
, to the following principles:
- For each real number x, if it is contradictory that x is equal to 0, then there exists y ∈ QRational numberIn mathematics, a rational number is any number that can be expressed as the quotient or fraction a/b of two integers, with the denominator b not equal to zero. Since b may be equal to 1, every integer is a rational number...
such that 0 < y < |x|, often expressed by saying that x is apartApartness relationIn constructive mathematics, an apartness relation is a constructive form of inequality, and is often taken to be more basic than equality. It is often written as # to distinguish from the negation of equality ≠, which is weaker....
from, or constructively unequal to, 0. - For each real number x, if it is contradictory that x is equal to 0, then there exists y ∈ R such that xy = 1.
Realizability
RealizabilityRealizability
Realizability is a part of proof theory which can be used to handle information about formulas instead of about the proofs of formulas. A natural number n is said to realize a statement in the language of arithmetic of natural numbers...
can be used to justify Markov's principle: a realizer is the unbounded search that successively checks if
is true. Because is not everywhere false, the search cannot go on forever. Using classical logic one concludes that the search therefore stops, namely at a value at which holds.Modified realizability
Realizability
Realizability is a part of proof theory which can be used to handle information about formulas instead of about the proofs of formulas. A natural number n is said to realize a statement in the language of arithmetic of natural numbers...
does not justify Markov's principle, even if classical logic is used in the meta-theory: there is no realizer in the language of simply typed lambda calculus
Simply typed lambda calculus
The simply typed lambda calculus , a formof type theory, is a typed interpretation of the lambda calculus with only one type constructor: \to that builds function types. It is the canonical and simplest example of a typed lambda calculus...
as this language is not Turing-complete and arbitrary loops cannot be defined in it.
Markov's rule
Markov's rule is the formulation of Markov's principle as a rule. It states that is derivable as soon as is, for decidable. The logician Harvey FriedmanHarvey Friedman
Harvey Friedman is a mathematical logician at Ohio State University in Columbus, Ohio. He is noted especially for his work on reverse mathematics, a project intended to derive the axioms of mathematics from the theorems considered to be necessary...
showed that Markov's rule is an admissible rule
Admissible rule
In logic, a rule of inference is admissible in a formal system if the set of theorems of the system does not change when that rule is added to the existing rules of the system. In other words, every formula that can be derived using that rule is already derivable without that rule, so, in a sense,...
in intuitionistic logic
Intuitionistic logic
Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
, Heyting arithmetic
Heyting arithmetic
In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it....
, and various other intuitionistic theories, using the Friedman translation
Friedman translation
In mathematical logic, the Friedman translation is a certain transformation of intuitionistic formulas. Among other things it can be used to show that the Π02-theorems of various first-order theories of classical mathematics are also theorems of intuitionistic mathematics...
.
Weak Markov's principle
A weaker form of Markov's principle may be stated in the language of analysis as
This form can be justified by Brouwer's continuity principles, whereas the stronger form contradicts them. Thus it can be derived from intuitionistic, realizability, and classical reasoning, in each case for different reasons, but this principle is not valid in the general constructive sense of Bishop.