Markov's principle: Difference between revisions
No edit summary |
links, several minor |
||
Line 1: | Line 1: | ||
'''Markov's principle''' (also known as |
'''Markov's principle''' (also known as the '''Leningrad principle'''<ref name="MarkovSchool">{{cite journal |last1=Margenstern |first1=Maurice |title=L'école constructive de Markov |journal=Revue d'histoire des mathématiques |date=1995 |volume=1 |issue=2 |pages=271-305 |url=http://www.numdam.org/item/RHM_1995__1_2_271_0/ |access-date=27 March 2024}}</ref>), named after [[Andrey Markov (Soviet mathematician)|Andrey Markov Jr]], is a conditional existence statement for which there are many equivalent formulations, as discussed below. The principle is [[Validity (logic)|logically valid]] [[classical logic|classically]], but not in [[Intuitionistic logic | intuitionistic]] [[constructivism (mathematics)|constructive]] mathematics. However, many particular instances of it are nevertheless provable in a constructive context as well. |
||
The principle is [[Validity (logic)|logically valid]] [[classical logic|classically]], but not in [[Intuitionistic logic | intuitionistic]] [[constructivism (mathematics)|constructive]] mathematics. However, many particular instances of it are nevertheless provable in a constructive context as well. |
|||
== History == |
== History == |
||
The principle was first studied and adopted by the Russian school of constructivism, together with |
The principle was first studied and adopted by the Russian school of constructivism, together with[[Axiom of dependent choice | choice principles]] and often with a [[realizability]] perspective on the notion of mathematical function. |
||
==In computability theory== |
==In computability theory== |
||
In the language of [[computability theory]], 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]], then the set is [[recursive set|decidable]]. |
In the language of [[computability theory]], 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]], then the set is [[recursive set|decidable]]. These statements are provable in classical logic. |
||
==In intuitionistic logic== |
==In intuitionistic logic== |
||
In [[predicate logic]], 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. |
In [[predicate logic]], 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. |
||
For a decidable predicate ''P'' over the [[natural number]]s, |
Markov's principle then states: For a decidable predicate ''P'' over the [[natural number]]s, if ''P'' cannot be false for all natural numbers ''n'', then it is true for some ''n''. Written using [[Quantifier (logic)|quantifiers]]: |
||
:<math>\Big(\forall n \big(P(n) \vee \neg P(n)\big) \wedge \neg \forall n\, \neg P(n)\Big) \rightarrow \exists n\, P(n)</math> |
:<math>\Big(\forall n \big(P(n) \vee \neg P(n)\big) \wedge \neg \forall n\, \neg P(n)\Big) \rightarrow \exists n\, P(n)</math> |
||
That is, if ''P'' cannot be false for all natural numbers ''n'', then it is true for some ''n''. |
|||
===Markov's rule=== |
===Markov's rule=== |
||
Line 28: | Line 24: | ||
Markov's principle is equivalent in the language of [[Heyting arithmetic|arithmetic]] to: |
Markov's principle is equivalent in the language of [[Heyting arithmetic|arithmetic]] to: |
||
:<math>\neg \neg \exists n\;f(n)=0 \rightarrow \exists n\;f(n)=0</math> |
:<math>\neg \neg \exists n\;f(n)=0 \rightarrow \exists n\;f(n)=0</math> |
||
for <math>f</math> a [[computable function|total recursive function]] on the natural numbers. |
for <math>f</math> a [[computable function|total recursive function]] on the natural numbers. |
||
In the presence of [[Church's thesis (constructive mathematics)|Church's thesis principle]], the principle is equivalent to its form for [[primitive recursive functions]]. Using [[Kleene's T predicate]], the latter may be expressed as |
In the presence of [[Church's thesis (constructive mathematics)|Church's thesis principle]], the principle is equivalent to its form for [[primitive recursive functions]]. Using [[Kleene's T predicate]], the latter may be expressed as |
||
:<math>\forall e\;\forall x\;\big(\neg \neg \exists w\; T_1(e, x, w) \rightarrow \exists w\; T_1(e, x, w)\big)</math> |
:<math>\forall e\;\forall x\;\big(\neg \neg \exists w\; T_1(e, x, w) \rightarrow \exists w\; T_1(e, x, w)\big)</math> |
||
Line 40: | Line 37: | ||
Markov's principle is equivalent, in the language of [[real analysis]], to the following principles: |
Markov's principle is equivalent, in the language of [[real analysis]], to the following principles: |
||
* For each real number ''x'', if it is contradictory that ''x'' is equal to 0, then there exists |
* For each [[real number]] ''x'', if it is contradictory that ''x'' is equal to 0, then there exists a [[rational number]] ''y'' such that 0 < ''y'' < |''x''|, often expressed by saying that ''x'' is [[apartness relation|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 ''y'' |
* 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]] 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. |
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. |
||
Line 48: | Line 45: | ||
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: |
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: |
||
:<math>\forall (x\in\mathbb{R})\, \Big(\forall(y\in\mathbb{R}) \big(\neg\neg(0 < y) \lor \neg\neg(y < x)\big)\Big) \,\to\, (0 < x).</math> |
:<math>\forall (x\in\mathbb{R})\, \Big(\forall(y\in\mathbb{R}) \big(\neg\neg(0 < y) \lor \neg\neg(y < x)\big)\Big) \,\to\, (0 < x).</math> |
||
This form can be justified by [[L. E. J. Brouwer|Brouwer's]] [[Brouwer's continuity principles|continuity principles]], whereas the stronger form contradicts them. Thus |
This form can be justified by [[L. E. J. Brouwer|Brouwer's]] [[Brouwer's continuity principles|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 [[Errett Bishop|Bishop]],<ref>[[Ulrich Kohlenbach]], "[http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.7455 On weak Markov's principle]". ''Mathematical Logic Quarterly'' (2002), vol 48, issue S1, pp. 59–65.</ref> nor provable in the [[constructive set theory|set theory <math>{\mathsf {IZF}}</math>]]. |
||
To understand what the principle is about, it helps to inspect a stronger statement. The following expresses that any real number <math>x</math>, such that no non-positive <math>y</math> is not below it, is positive: |
To understand what the principle is about, it helps to inspect a stronger statement. The following expresses that any real number <math>x</math>, such that no non-positive <math>y</math> is not below it, is positive: |
||
Line 58: | Line 55: | ||
===Extensionality of functions=== |
===Extensionality of functions=== |
||
A function <math>f: X \to Y</math> between metric spaces is called ''strongly extensional'' if <math>d(f(x),f(y)) > 0 </math> implies <math>d(x,y) > 0</math>, which is classically just the [[contraposition]] 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 metric spaces to metric spaces are strongly extensional. |
A function <math>f: X \to Y</math> between [[Metric space|metric spaces]] is called ''strongly extensional'' if <math>d(f(x),f(y)) > 0 </math> implies <math>d(x,y) > 0</math>, which is classically just the [[contraposition]] 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 metric space|complete]] metric spaces to metric spaces are strongly extensional. |
||
== See also == |
== See also == |
Revision as of 14:43, 19 June 2024
Markov's principle (also known as the Leningrad principle[1]), named after Andrey Markov Jr, 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 perspective on the notion of mathematical function.
In computability theory
In the language of computability theory, 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, then the set is decidable. These statements are provable in classical logic.
In intuitionistic logic
In predicate logic, 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 numbers, if P cannot be false for all natural numbers n, then it is true for some n. Written using quantifiers:
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. Formally,
Anne Troelstra[2] proved that it is an admissible rule in Heyting arithmetic. Later, the logician Harvey Friedman showed that Markov's rule is an admissible rule in first-order intuitionistic logic, Heyting arithmetic, and various other intuitionistic theories,[3] using the Friedman translation.
In Heyting arithmetic
Markov's principle is equivalent in the language of arithmetic to:
for a total recursive function on the natural numbers.
In the presence of Church's thesis principle, the principle is equivalent to its form for primitive recursive functions. Using Kleene's T predicate, the latter may be expressed as
Realizability
If constructive arithmetic is translated using realizability into a classical meta-theory that proves the -consistency of the relevant classical theory (for example, Peano arithmetic if we are studying Heyting arithmetic), then Markov's principle is justified: a realizer is the constant function that takes a realization that is not everywhere false to the unbounded search that successively checks if is true. If is not everywhere false, then by -consistency there must be a term for which holds, and each term will be checked by the search eventually. If however 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), 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, Markov's principle exactly captures the difference between a constructive and classical meta-theory. Specifically, a statement is provable in Heyting arithmetic with extended Church's thesis if and only if there is a number that provably realizes it in Heyting arithmetic; and it is provable in Heyting arithmetic 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 constructive analysis
Markov's principle is equivalent, in the language of real analysis, to the following principles:
- For each real number x, if it is contradictory that x is equal to 0, then there exists a rational number 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 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.
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:
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,[4] 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 , such that no non-positive is not below it, is positive:
where denotes the negation of . 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 for 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 between metric spaces is called strongly extensional if implies , which is classically just the contraposition 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 metric spaces to metric spaces are strongly extensional.
See also
References
- ^ Margenstern, Maurice (1995). "L'école constructive de Markov". Revue d'histoire des mathématiques. 1 (2): 271–305. Retrieved 27 March 2024.
- ^ Anne S. Troelstra. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Springer Verlag (1973), Theorem 4.2.4 of the 2nd edition.
- ^ Harvey Friedman. Classically and Intuitionistically Provably Recursive Functions. In Scott, D. S. and Muller, G. H. Editors, Higher Set Theory, Volume 699 of Lecture Notes in Mathematics, Springer Verlag (1978), pp. 21–28.
- ^ Ulrich Kohlenbach, "On weak Markov's principle". Mathematical Logic Quarterly (2002), vol 48, issue S1, pp. 59–65.