BRICSRS-01-51U.Kohlenbach:OnWeakMarkov’sPrinciple
BRICS
Basic Research in Computer Science
On Weak Markov’s Principle
Ulrich Kohlenbach
BRICS Report Series RS-01-51
Copyright c2001, Ulrich Kohlenbach.
BRICS, Department of Computer Science University of Aarhus. All rights reserved.
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.
See back inner page for a list of recent BRICS Report Series publications.
Copies may be obtained by contacting:
BRICS
Department of Computer Science University of Aarhus
Ny Munkegade, building 540 DK–8000 Aarhus C
Denmark
Telephone: +45 8942 3360 Telefax: +45 8942 3255 Internet: BRICS@brics.dk
BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:
http://www.brics.dk ftp://ftp.brics.dk
This document in subdirectoryRS/01/51/
On weak Markov’s principle
Ulrich Kohlenbach
BRICS
∗Department of Computer Science University of Aarhus
Ny Munkegade
DK-8000 Aarhus C, Denmark kohlenb@brics.dk
Keywords: Markov’s principle, intuitionism, constructive analysis, restricted clas- sical logic, modified realizability.
AMS Classification: 03F60, 03F10, 03F35, 03F50.
Abstract
We show that the so-called weak Markov’s principle (WMP) which states that every pseudo-positive real number is positive is underivable in Tω :=E- HAω+AC. Since Tω allows to formalize (at least large parts of) Bishop’s con- structive mathematics this makes it unlikely that WMP can be proved within the framework of Bishop-style mathematics (which has been open for about 20 years). The underivability even holds if the ineffective schema of full compre- hension (in all types) for negated formulas (in particular for ∃-free formulas) is added which allows to derive the law of excluded middle for such formulas.
1 Introduction
The so-called weak Markov’s principle (WMP) has been first considered by Mandelk- ern in [14],[15] (in the former paper under the name ‘almost separating principle’
(ASP) and in the latter as ‘weak limited principle of existence’ (WLPE)). Under
∗Basic Research in Computer Science, funded by the Danish National Research Foundation.
the currently common name of weak Markov’s principle it has been investigated by Ishihara ([8],[9]). WMP plays a crucial role in the study of the interrelations between various continuity principles within the framework of Bishop-style construc- tive mathematics ([2],[3],[4]). In order to state WMP we first need the notion of
‘pseudo-positivity’:
Definition 1 1) A real number a∈IR is pseudo-positive if
∀x∈IR(¬¬(0< x)∨ ¬¬(x < a)).
2) a∈IR is positive if a >0.
Remark 2 1) It is clear that we can without loss of generality restrict x ∈IR in the definition of pseudo-positivity to x∈[0,1].
2) ‘x > y’ for x, y ∈IR is to be read as a positive existence statement
‘∃n ∈ IN(x ≥ y+ n+11 )’ which has – constructively – to be distinguished from the negative statement ‘¬(y≤x)’.
Definition 3 Weak Markov’s principle is the schema
(WMP): Every pseudo-positive real number is positive.
WMP follows easily from the well-know Markov’s principle as well as from an ap- propriate continuity principle and also from the extended Church’s thesis ECT0 (see [10]). So WMP holds both in Russian constructive mathematics as well as in intu- itionistic mathematics (in the sense of [4]).
Since about 20 years it has been an open problem whether WMP is derivable in Bishop-style mathematics. The problem is, of course, not completely precise as no particular formal system has been identified with Bishop-style mathematics. How- ever, it is commonly agreed that Heyting arithmetic in all finite types HAω (see [17]) plus the axiom of choice AC in all types
ACρ,τ : ∀xρ∃yτA(x, y)→ ∃Yρ→τ∀xρA(x, Y(x))
is a framework which is quite capable of formalizing existing constructive (in the sense of Bishop) mathematics (see also [1],[6]).
In this note we show that WMP is underivable even in E-HAω+AC, where E-HAω is Heyting arithmetic in all finite types with the full axiom of extensionality (see again [17] for a precise definition). Our proof even establishes that this underivability
remains true if the (highly non-constructive) schema of full comprehension in all types for arbitrary negated formulas
CA¬ : ∃Φρ→0∀xρ(Φ(x) =0 0↔ ¬A(x))
is added to E-HAω+AC which e.g. allows to derive the law of excluded middle for all negated formulas
¬A∨ ¬¬A.
Moreover, since E-HAω proves that every ∃-free formula A (i.e. A contains neither
‘∃’ nor ‘∨’) is equivalent to its double negation ¬¬A,1 we also get comprehension (and consequently the corresponding law of excluded middle) for∃-free formulas
CA∃-free : ∃Φρ→0∀xρ(Φ(x) =0 0↔A(x)), A ∃-free,
which allows e.g. to derive the classical binary K¨onig’s lemma WKL (and even the uniform binary K¨onig’s lemma UWKL which states the existence of a functional which selects an infinite path uniformly in an infinite binary tree, see [13]).
Many equivalent formulations have of WMP have been found meanwhile. One of those, due to Ishihara [8], is particularly interesting and reads as follows
Every mapping of a complete metric space into a metric space is strongly extensional where f :X →Y is strong extensional if
∀x1, x2 ∈X(dY(f(x1), f(x2))>0→dX(x1, x1)>0).
In this formulation, the underivability of WMP is particularly easy to prove as we indicate at the end of this paper. However, to conclude from there the underivability of the usual formulation of WMP in E-HAω+AC we would have to undertake the tedious task of verifying that Ishihara’s equivalence proof can be formalized in E- HAω+AC. Richman [16] has shown that the proof that WMP implies Ishihara’s strong extensionality statement requires a weak form of countable choice and fails in certain sheaf models.
2 The independence result
Definition 4 (Independence-of-premise for negated formulas) IP¬ : (¬A→ ∃xρB)→ ∃xρ(¬A→B), where x does not occur free in A.
1Note that E-HAωonly has prime formulas of the forms=0twhich are decidable and therefore stable.
The following theorem was proved in [12](thm.3.3)
Theorem 5 ([12]) Let δ, ρ, γ be arbitrary types and Gbe a sentence of the form G≡ ∀xδ(A→ ∃y≤ρ sx¬B(x, y))
and
G˜ :≡ ∃Y ≤s∀x(A→ ¬B(x, Y(x))),
wheresis a closed term of E-HAωandx1 ≤ρx2is pointwise defined as∀v(x1v ≤0 x2v) for a suitable tuple v of variables.
LetC(u, v), D(u, v, w) only contain u, v resp. u, v, w as free variables. Then
E-HAω+AC+IP¬+G` ∀u1∀v ≤γ tu(¬C(u, v)→ ∃w0D(u, v, w))
⇒there exists a closed term Φ of E-HAω s.t.2
E-HAω+AC+IP¬+ ˜G` ∀u1∀v ≤γ tu∃w≤0 Φ(u)(¬C →D(w)).
Note that the bound Φ(u) does not depend on v.
Corollary 6
E-HAω+AC+IP¬+CA¬ ` ∀u1∀v ≤γ tu(¬C(u, v)→ ∃w0D(u, v, w))
⇒there exists a closed term Φ of E-HAω s.t.
E-HAω+AC+IP¬+CA¬ ` ∀u1∀v ≤γ tu∃w≤0 Φ(u)(¬C →D(w)).
Proof: The corollary follows from the previous theorem by observing that:
(i) we can without loss of generality assume that all instances of CA¬ are parameter- free since parameters a in A can be taken into the comprehension together with x, (ii) every parameter-free instance of CA¬ is – relative to E-HAω – equivalent to a sentenceG as considered in the theorem (withA :≡0 = 0, x a dummy variable and s:=λx.1)3
∃Φ≤1¬¬∀x(Φ(x) =0 0↔ ¬A(x)), with ˜G≡G.2
Remark 7 In the presence of CA¬ one can actually derive IP¬.
2I.e. Φ is a primitive recursive functional in the sense of G¨odel’sT.
3Here 1ρ:=λv.10for a suitable tuple of variables v.
In order to formalize WMP in the language of E-HAω we have to represent real numbers in [0,1]. Furthermore, we show that we can arrange the representation such that the names of reals in [0,1] used belong to a compact subspace of the Baire space.
We represent real numbers (as in Bishop’s original treatment) as Cauchy sequences with a fixed rate of convergence (the latter is inessential in a setting as ours which contains AC since – using only AC0,0 from integers to integers – we can replace an arbitrary Cauchy sequence by one with a fixed rate of convergence which has the same limit).
Rational numbers in [0,1] are represented as codesj(n, m) of pairs (n, m) of natural numbers n, m.
j(n, m) represents the rational number m+1n , if n ≤m+ 1 and 0, otherwise.
Herej e.g. is Cantor’s surjective pairing functionj(x, y) := 12((x+y)2+ 3x+y). On the codes of Q∩[0,1], i.e. on IN, we have an equivalence relation by
n1 =Q n2 :≡ n1, n2 represent the same rational number.
On IN one easily defines a primitive recursive function| · −Q· |representing the usual distance function on [0,1]∩Q] and relations <Q,≤Q which represent the relations on Q∩[0,1]. For convenience we will write k+11 instead of its code j(1, k) in IN.
By the coding of rational numbers in [0,1] as natural numbers, sequences of such rationalsare just functionsf1 (and every functionf1can be conceived as a sequence of rational numbers in [0,1] in a unique way). So real numbers in [0,1] can be represented by functions f1 modulo this coding. We now show that every function can be conceived as a representative of a uniquely determined Cauchy sequence of rationals in [0,1] with modulus 1/(k + 1) and therefore can be conceived as an representative of a uniquely determined real number. Finally we show, that we can restrict ourselves to codes f ≤1 M for some primitive recursive function M.
Definition 8 Primitive recursively in f we define
f nb :=
f n, if ∀k, m,m˜ ≤0 n(m,m˜ ≥0 k → |f m−Qfm˜| ≤Q 1 k+1) f(n0−1) for n0 := minl ≤0 n such that
[∃k, m,m˜ ≤0 l(m,m˜ ≥0 k∧ |f m−Qfm˜|>Q k+11 )], otherwise.
1) if f1 represents a Cauchy sequence of rational numbers in [0,1] with modulus 1/(k+ 1), then ∀n0(f n=0 f n),b
2) for every f1 the function fbrepresents a Cauchy sequence of rational numbers in [0,1] with modulus 1/(k+ 1).
Hence every function f gives a uniquely determined real number in [0,1], namely that number which is represented by fb.
Definition 9 1) f1 =IR f2 :≡ ∀k0(|fb1(k)−Qfb2(k)| ≤Q 3 k+1);
2) f1 <IR f2 :≡ ∃k0(fb2(k)−fb1(k)>Q k+13 );
3) f1 ≤IR f2 :≡ ¬(f2 <IRf1);
We can restrict the set of representing functions for [0,1] to the compact (in the sense of the Baire space) set{f :f ≤1 M}, where M(n) :=j(3(n+ 1),3(n+ 1)−1): Each fraction r having the form 3(n+1)i (with i ≤ 3(n+ 1)) is represented by a number k ≤ M(n), i.e. k ≤M(n)∧k codes r. Thus {k :k ≤M(n)} contains (modulo this coding) an 3(n+1)1 –net for [0,1]. Primitive recursively in f we define
f(k) =˜ µi≤0 M(k)[∀j ≤0 M(k)(|fb(3(k+ 1))−Qj| ≥Q |f(3(kb + 1))−Q i|)].
f˜has (provably in E-HAω) the following properties (using thatfb˜=1 f):˜ 1) ∀f1( ˜f ≤1 M).
2) ∀f1(f =IR f˜).
Using this construction we can reduce e.g. quantification∀x ∈[0,1]A(x) to quantifi- cation of the form ∀f ≤1 M A(f) and equivalently ∀f1A(f) for properties A which are =IR–extensional.
Theorem 10 E-HAω+AC+IP¬+CA¬`/ WMP.
Proof: Let T :=E-HAω+AC+IP¬+CA¬ and assume that T ` WMP. Then (re- stricting w.l.g. a, x to [0,1])
T ` ∀a∈[0,1](∀x∈[0,1](¬¬(0< x)∨ ¬¬(x < a))→ ∃k0(a > 1 k+ 1))
which can – modulo our representation of x, a∈[0,1] in E-HAω – be written in the form
T ` ∀a ≤1 M(∀x1(¬¬(0<IR x)∨ ¬¬(x <IRa))→ ∃k0(a >IR 1 k+ 1)).
This is equivalent to
T ` ∀a≤1 M(∀x1∃n ≤0 1[(n = 0→ ¬¬(0<IRx))∧(n 6= 0→ ¬¬(x <IR a))]
→ ∃k0(a >IR k+11 )), which implies
T ` ∀a≤1 M∀N ≤2 1
(∀x1[(N(x) = 0→ ¬¬(0<IR x))∧(N(x)6= 0→ ¬¬(x <IR a))]→ ∃k0(a >IR k+11 )).
The premise ‘∀x1[(N(x) = 0 → ¬¬(0 <IR x))∧(N(x) 6= 0 → ¬¬(x <IR a))]’ can easily be proved (relative to E-HAω) to be equivalent to its double negation and hence is equivalent to a negated formula ¬B. So by corollary 6 we get a closed number term t0 which can be reduced to a numeralm s.t.
T ` ∀a≤1 M∀N ≤2 1
(∀x1[(N(x) = 0→ ¬¬(0<IRx))∧(N(x)6= 0→ ¬¬(x <IRa))]→a >IR m+11 ).
Using AC this yields T ` ∀a≤1 M
(∀x1∃n≤0 1[(n= 0 → ¬¬(0<IRx))∧(n6= 0→ ¬¬(x <IRa))]→a >IR m+11 ) and hence
T ` ∀a ∈[0,1](a pseudo-positive →a > 1 m+ 1) which obviously is absurd. 2
Final Remark:
1) As mentioned in the introduction, the statement that every mapping f :X → Y from a complete metric space into a metric space is strongly extensional, which was shown by Ishihara [8] to be equivalent to WMP, can be seen to be underivable in the systems considered in this paper particularly easy: choose asX the Baire space with the usual metric and as Y the discrete space IN. In E-HAω the extensionality axiom implies that every functionalF2 is a function : ININ →IN. If the above mentioned principle were derivable in E-HAω+AC then one could derive that every F2 is strongly extensional which in this particular case is equivalent to the statement
∀f1, g1(F(f)6=0 F(g)→ ∃x0(f(x)6=0 g(x)).
By modified realizability (which is sound for E-HAω+AC, see [17],[18]) one could extract a closed term t of E-HAω witnessing ‘∃x’ uniformly in F, f, g.
However, such a term would satisfy the G¨odel functional (‘Dialectica’) inter- pretation of the extensionality axiom for functionals of type 2. As shown by Howard [7] such a term does not exist in E-HAω as it would not be majorizable whereas all closed terms in E-HAω are.4 For Using our theorem 5 instead we can also extend this proof to the situation where CA¬ is added to E-HAω+AC.
Note that the proof of theorem 5 in [12] uses modified realizability and Howard’s concept of majorizability too. Our proof for the underivability of the usual for- mulation of WMP is more direct as the argument sketched in this remark relies on Ishihara’s proof of the fact that WMP implies the principle mentioned above which, moreover, would have to be proved to be formalizable in E-HAω+AC first.
2) Our proof of the underivability of WMP in E-HAω+AC+CA¬ generalizes to extensions by any further principles whose monotone modified realizability in- terpretation (in the sense of [12]) is realizable by closed terms of E-HAω. Acknowledgement: We are grateful to Bas Spitters for bringing the problem treated in this paper to our attention and providing bibliographic information con- cerning WMP.
4In this way one can also show that E-HAω+AC is not closed under Markov’s rule (see [11] for more information on this).
References
[1] Beeson, M., Foundations of Constructive Mathematics. Springer Verlag, Berlin, Heidelberg, New York, xxiii+466pp. (1985).
[2] Bishop, E., Foundations of Constructive Analysis. McGraw-Hill, New York (1967).
[3] Bishop, E., Bridges, D.S., Constructive Analysis. Springer Verlag, Berlin (1985).
[4] Bridges, D., Richman, F., Varieties of Constructive Mathematics. London Math- ematical Soc. LNS97, Cambridge University Press (1987).
[5] Buss, S.R. (editor), Handbook of Proof Theory. Studies in Logic and the Foun- dations of Mathematics Vol 137, Elsevier, vii+811 pp. (1998).
[6] Goodman, N.D., Myhill, J.,The formalization of Bishop’s constructive math- ematics. In: Lawvere, F.W. (ed.), Toposes, Algebraic Geometry and Logic.
Springer LNM 274, pp. 83-96 (1972).
[7] Howard, W.A., Hereditarily majorizable functionals of finite type. In: [17], pp.
454-461. Springer LNM 344 (1973).
[8] Ishihara, H., Continuity and nondiscontinuity in constructive mathematics. J.
Symbolic Logic 56, pp. 1349-1354 (1991).
[9] Ishihara, H., Continuity properties in constructive mathematics. J. Symbolic Logic 57, pp. 557-565 (1992).
[10] Ishihara, H., Markov’s principle, Chruch’s thesis and Lindel¨of’s theorem. Idag.
Math. 4, pp. 321-325 (1993).
[11] Jørgensen, K.F., Finite Type Arithmetic: computable existence analysed by modified realizability and functional interpretation. Master Thesis, University of Roskilde, viii+121 pages (2001).
[12] Kohlenbach, U., Relative constructivity. J. Symbolic Logic 63, pp. 1218-1238 (1998).
[13] Kohlenbach, U., On the uniform weak K¨onig’s lemma. Ann. Pure Applied Logic 114, pp. 103-116 (2002).
[14] Mandelkern, M., Constructive continuity. Mem.Amer.Math.Soc. 277, Provi- dence, Rhode Island (1983).
[15] Mandelkern, M., Constructive complete finite sets. Zeitschr. f. math. Logik u.
Grundlagen d. Math. 34, pp. 97-103 (1988).
[16] Richman, F., Weak Markov’s principle, strong extensionality, and countable choice. Preprint 5pp. (2000).
[17] Troelstra, A.S. (ed.) Metamathematical investigation of intuitionistic arithmetic and analysis. Springer Lecture Notes in Mathematics 344 (1973).
[18] Troelstra, A.S., Realizability. In: [5], pp. 407-473 (1998).
Recent BRICS Report Series Publications
RS-01-51 Ulrich Kohlenbach. On Weak Markov’s Principle. December 2001. 10 pp.
RS-01-50 Jiˇr´ı Srba. Note on the Tableau Technique for Commutative Transition Systems. December 2001. To appear in the pro- ceedings of FOSSACS ’02.
RS-01-49 Olivier Danvy and Lasse R. Nielsen. A First-Order One-Pass CPS Transformation. 2001. Extended version of a paper to appear in the proceedings of FOSSACS ’02.
RS-01-48 Mogens Nielsen and Frank D. Valencia. Temporal Concurrent Constraint Programming: Applications and Behavior. Decem- ber 2001. 36 pp.
RS-01-47 Jesper Buus Nielsen. Non-Committing Encryption is Too Easy in the Random Oracle Model. December 2001. 20 pp.
RS-01-46 Lars Kristiansen. The Implicit Computational Complexity of Imperative Programming Languages. November 2001. 46 pp.
RS-01-45 Ivan B. Damg˚ard and Gudmund Skovbjerg Frandsen. An Ex- tended Quadratic Frobenius Primality Test with Average Case Error Estimates. November 2001. 43 pp.
RS-01-44 M. Oliver M¨oller, Harald Rueß, and Maria Sorea. Predi- cate Abstraction for Dense Real-Time Systems. November 2001.
27 pp.
RS-01-43 Ivan B. Damg˚ard and Jesper Buus Nielsen. From Known- Plaintext Security to Chosen-Plaintext Security. November 2001. 18 pp.
RS-01-42 Zolt´an ´Esik and Werner Kuich. Rationally Additive Semirings.
November 2001. 11 pp.
RS-01-41 Ivan B. Damg˚ard and Jesper Buus Nielsen. Perfect Hiding and Perfect Binding Universally Composable Commitment Schemes with Constant Expansion Factor. October 2001. 43 pp.
RS-01-40 Daniel Damian and Olivier Danvy. CPS Transformation of Flow Information, Part II: Administrative Reductions. October 2001. 9 pp.
RS-01-39 Olivier Danvy and Mayer Goldberg. There and Back Again.
