Markov's Rule
   HOME

TheInfoList



OR:

Markov's principle (also known as the Leningrad principle), named after
Andrey Markov Jr Andrey (Андрей) is a masculine given name predominantly used in Slavic languages, including Belarusian, Bulgarian, and Russian. The name is derived from the ancient Greek Andreas (Ἀνδρέας), meaning "man" or "warrior". In Eastern ...
, is a conditional existence statement for which there are many equivalent formulations, as discussed below. The principle is logically valid classically, but not in intuitionistic constructive mathematics. However, many particular instances of it are nevertheless provable in a constructive context as well.


History

The principle was first studied and adopted by the Russian school of constructivism, together with choice principles and often with a
realizability In mathematical logic, realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them. Formulas from a formal theory are "realized" by objects, known as "realizers", in a way ...
perspective on the notion of mathematical function.


In computability theory

In the language of
computability theory Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since ex ...
, Markov's principle is a formal expression of the claim that if it is impossible that an algorithm does not terminate, then for some input it does terminate. This is equivalent to the claim that if a set and its complement are both
computably enumerable In computability theory, a set ''S'' of natural numbers is called computably enumerable (c.e.), recursively enumerable (r.e.), semidecidable, partially decidable, listable, provable or Turing-recognizable if: *There is an algorithm such that the ...
, then the set is decidable. These statements are provable in classical logic.


In intuitionistic logic

In
predicate logic First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables ove ...
, a predicate ''P'' over some domain is called ''decidable'' if for every ''x'' in the domain, either ''P''(''x'') holds, or the negation of ''P''(''x'') holds. This is not trivially true constructively. Markov's principle then states: For a decidable predicate ''P'' over the
natural number In mathematics, the natural numbers are the numbers 0, 1, 2, 3, and so on, possibly excluding 0. Some start counting with 0, defining the natural numbers as the non-negative integers , while others start with 1, defining them as the positive in ...
s, if ''P'' cannot be false for all natural numbers ''n'', then it is true for some ''n''. Written using quantifiers: :\Big(\forall n \big(P(n) \vee \neg P(n)\big) \wedge \neg \forall n\, \neg P(n)\Big) \rightarrow \exists n\, P(n)


Markov's rule

Markov's rule is the formulation of Markov's principle as a rule. It states that \exists n\;P(n) is derivable as soon as \neg \neg \exists n\;P(n) is, for P decidable. Formally, :\forall n \big(P(n)\lor \neg P(n)\big),\ \neg \neg \exists n\;P(n)\ \ \vdash\ \ \exists n\;P(n)
Anne Troelstra Anne Sjerp Troelstra (10 August 1939 – 7 March 2019) was a professor of pure mathematics and foundations of mathematics at the Institute for Logic, Language and Computation (ILLC) of the University of Amsterdam. He was a constructivist logici ...
proved that it is an
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 ...
in
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. Axiomatization Heyting arithmetic can be characterized jus ...
. Later, the logician Harvey Friedman showed that Markov's rule is an admissible rule in first-order intuitionistic logic,
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. Axiomatization Heyting arithmetic can be characterized jus ...
, and various other intuitionistic theories, using the
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 ...
.


In Heyting arithmetic

Markov's principle is equivalent in the language of
arithmetic Arithmetic is an elementary branch of mathematics that deals with numerical operations like addition, subtraction, multiplication, and division. In a wider sense, it also includes exponentiation, extraction of roots, and taking logarithms. ...
to: :\neg \neg \exists n\;f(n)=0 \rightarrow \exists n\;f(n)=0 for f a total recursive function on the natural numbers. In the presence of the Church's thesis principle, Markov's principle is equivalent to its form for
primitive recursive functions In computability theory, a primitive recursive function is, roughly speaking, a function that can be computed by a computer program whose loops are all "for" loops (that is, an upper bound of the number of iterations of every loop is fixed befor ...
. Using
Kleene's T predicate In computability theory, the T predicate, first studied by mathematician Stephen Cole Kleene, is a particular set of triples of natural numbers that is used to represent computable functions within formal theories of arithmetic. Informally, the ' ...
, the latter may be expressed as double-negation elimination for \exists w\; T_1(e, x, w), i.e. :\forall e\;\forall x\;\big(\neg \neg \exists w\; T_1(e, x, w) \rightarrow \exists w\; T_1(e, x, w)\big)


Realizability

If constructive arithmetic is translated using
realizability In mathematical logic, realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them. Formulas from a formal theory are "realized" by objects, known as "realizers", in a way ...
into a classical meta-theory that proves the \omega-consistency of the relevant classical theory (for example, Peano arithmetic if we are studying
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. Axiomatization Heyting arithmetic can be characterized jus ...
), then Markov's principle is justified: a realizer is the constant function that takes a realization that P is not everywhere false to the
unbounded search Boundedness, bounded, or unbounded may refer to: Economics * Bounded rationality, the idea that human rationality in decision-making is bounded by the available information, the cognitive limitations, and the time available to make the decision ...
that successively checks if P(0), P(1), P(2),\dots is true. If P is not everywhere false, then by \omega-consistency there must be a term for which P holds, and each term will be checked by the search eventually. If however P does not hold anywhere, then the domain of the constant function must be empty, so although the search does not halt it still holds vacuously that the function is a realizer. By the Law of the Excluded Middle (in our classical metatheory), P must either hold nowhere or not hold nowhere, therefore this constant function is a realizer. If instead the realizability interpretation is used in a constructive meta-theory, then it is not justified. Indeed, for
first-order arithmetic In first-order logic, a first-order theory is given by a set of axioms in some language. This entry lists some of the more common examples used in model theory and some of their properties. Preliminaries For every natural mathematical structure ...
, Markov's principle exactly captures the difference between a constructive and classical meta-theory. Specifically, a statement is provable in
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. Axiomatization Heyting arithmetic can be characterized jus ...
with extended Church's thesis if and only if there is a number that provably realizes it in
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. Axiomatization Heyting arithmetic can be characterized jus ...
; and it is provable in
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. Axiomatization Heyting arithmetic can be characterized jus ...
with extended Church's thesis ''and Markov's principle'' if and only if there is a number that provably realizes it in
Peano arithmetic In mathematical logic, the Peano axioms (, ), also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th-century Italian mathematician Giuseppe Peano. These axioms have been used nea ...
.


In constructive analysis

Markov's principle is equivalent, in the language of
real analysis In mathematics, the branch of real analysis studies the behavior of real numbers, sequences and series of real numbers, and real functions. Some particular properties of real-valued sequences and functions that real analysis studies include co ...
, to the following principles: * For each
real number In mathematics, a real number is a number that can be used to measure a continuous one- dimensional quantity such as a duration or temperature. Here, ''continuous'' means that pairs of values can have arbitrarily small differences. Every re ...
''x'', if it is contradictory that ''x'' is equal to 0, then there exists a
rational number In mathematics, a rational number is a number that can be expressed as the quotient or fraction of two integers, a numerator and a non-zero denominator . For example, is a rational number, as is every integer (for example, The set of all ...
''y'' such that 0 < ''y'' < , ''x'', , often expressed by saying that ''x'' is apart from, or constructively unequal to, 0. * For each real number ''x'', if it is contradictory that ''x'' is equal to 0, then there exists a real number ''y'' such that ''xy'' = 1. Modified
realizability In mathematical logic, realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them. Formulas from a formal theory are "realized" by objects, known as "realizers", in a way ...
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 The simply typed lambda calculus (), a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor () that builds function types. It is the canonical and simplest example of a typed lambda calculus. The ...
as this language is not
Turing-complete In computability theory, a system of data-manipulation rules (such as a model of computation, a computer's instruction set, a programming language, or a cellular automaton) is said to be Turing-complete or computationally universal if it can be ...
and arbitrary loops cannot be defined in it.


Weak Markov's principle

The weak Markov's principle is a weaker form of the principle. It may be stated in the language of analysis, as a conditional statement for the positivity of a real number: :\forall (x\in\mathbb)\, \Big(\forall(y\in\mathbb) \big(\neg\neg(0 < y) \lor \neg\neg(y < x)\big)\Big) \,\to\, (0 < x). This form can be justified by Brouwer's continuity principles, whereas the stronger form contradicts them. Thus the weak Markov principle can be derived from intuitionistic, realizability, and classical reasoning, in each case for different reasons, but it is not valid in the general constructive sense of
Bishop A bishop is an ordained member of the clergy who is entrusted with a position of Episcopal polity, authority and oversight in a religious institution. In Christianity, bishops are normally responsible for the governance and administration of di ...
,
Ulrich Kohlenbach Ulrich Wilhelm Kohlenbach (born 27 July 1962 in Frankfurt am Main) is a German mathematician and professor of algebra and logic at the Technische Universität Darmstadt. His research interests lie in the field of proof mining. Kohlenbach was p ...
,
On weak Markov's principle
. ''Mathematical Logic Quarterly'' (2002), vol 48, issue S1, pp. 59–65.
nor provable in the set theory . To understand what the principle is about, it helps to inspect a stronger statement. The following expresses that any real number x, such that no non-positive y is not below it, is positive: :\nexists(y \le 0)\, x \le y \,\to\, (0 < x), where x \leq y denotes the negation of y < x. This is a stronger implication because the antecedent is looser. Note that here a logically positive statement is concluded from a logically negative one. It is implied by the weak Markov's principle when elevating the
De Morgan's law In propositional logic and Boolean algebra, De Morgan's laws, also known as De Morgan's theorem, are a pair of transformation rules that are both valid rules of inference. They are named after Augustus De Morgan, a 19th-century British mathemat ...
for \neg A\lor \neg B to an equivalence. Assuming classical double-negation elimination, the weak Markov's principle becomes trivial, expressing that a number larger than all non-positive numbers is positive.


Extensionality of functions

A function f: X \to Y between
metric spaces In mathematics, a metric space is a set together with a notion of ''distance'' between its elements, usually called points. The distance is measured by a function called a metric or distance function. Metric spaces are a general setting for ...
is called ''strongly extensional'' if d(f(x),f(y)) > 0 implies d(x,y) > 0, which is classically just the
contraposition In logic and mathematics, contraposition, or ''transposition'', refers to the inference of going from a conditional statement into its logically equivalent contrapositive, and an associated proof method known as . The contrapositive of a stateme ...
of the function preserving equality. Markov's principle can be shown to be equivalent to the proposition that all functions between arbitrary metric spaces are strongly extensional, while the weak Markov's principle is equivalent to the proposition that all functions from
complete Complete may refer to: Logic * Completeness (logic) * Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable Mathematics * The completeness of the real numbers, which implies t ...
metric spaces to metric spaces are strongly extensional.


See also

*
Constructive analysis In mathematics, constructive analysis is mathematical analysis done according to some principles of constructive mathematics. Introduction The name of the subject contrasts with ''classical analysis'', which in this context means analysis done acc ...
*
Church's thesis (constructive mathematics) In constructive mathematics, Church's thesis is the principle stating that all total functions are computable functions. The similarly named Church–Turing thesis states that every '' effectively calculable function'' is a ''computable function' ...
* Limited principle of omniscience


References


External links


Constructive Mathematics (Stanford Encyclopedia of Philosophy)
{{DEFAULTSORT:Markov's Principle Logic Constructivism (mathematics) Mathematical principles