BRICS RS-01-51 U. Kohlenbach: On Weak Markov’s Principle BRICS

Basic Research in Computer Science

On Weak Markov’s Principle

Ulrich Kohlenbach BRICS Report Series RS-01-51 ISSN 0909-0878 December 2001 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2001, 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 subdirectory RS/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 classical 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 constructive 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 comprehension (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 Mandelkern 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 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 constructive mathematics ([2],[3],[4]). In order to state WMP we first need the notion of ‘pseudo-positivity’:

∗Basic Research in Computer Science, funded by the Danish National Research Foundation.

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 + \frac{1}{n+1})’ 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 appropriate continuity principle and also from the extended Church’s thesis ECT_{0} (see [10]). So WMP holds both in Russian constructive mathematics as well as in intuitionistic 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. However, 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_{¬} : ∃Φ^{\underline{ρ}→0}∀\underline{x}\underline{ρ}(Φ(\underline{x}) =_{0} 0 ↔ ¬A(\underline{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} : ∃Φ^{\underline{ρ}→0}∀\underline{x}\underline{ρ}(Φ(\underline{x}) =_{0} 0 ↔ A(\underline{x})), A ∃-free,

which allows e.g. to derive the classical binary König’s lemma WKL (and even the uniform binary König’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

∀x_{1}, x_{2} ∈ X(d_{Y} (f(x_{1}), f(x_{2})) > 0 → d_{X}(x_{1}, x_{1}) > 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 form s =_{0} t which are decidable and therefore stable.

The following theorem was proved in [12](thm.3.3)

Theorem 5 ([12]) Let δ, ρ, γ be arbitrary types and G be a sentence of the form

G ≡ ∀x^{δ}(A → ∃y ≤_{ρ} sx¬B(x, y))

and

G̃ :≡ ∃Y ≤ s∀x(A → ¬B(x, Y (x))),

where s is a closed term of E-HA^{ω} and x_{1} ≤_{ρ} x_{2} is pointwise defined as ∀\underline{v}(x_{1}\underline{v} ≤_{0} x_{2}\underline{v}) for a suitable tuple \underline{v} of variables. Let C(u, v), D(u, v, w) only contain u, v resp. u, v, w as free variables. Then

E-HA^{ω}+AC+IP_{¬} + G ⊢ ∀u^{1}∀v ≤_{γ} tu(¬C(u, v) → ∃w^{0}D(u, v, w))

⇒ there exists a closed term Φ of E-HA^{ω} s.t.^{2}

E-HA^{ω}+AC+IP_{¬} + G̃ ⊢ ∀u^{1}∀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_{¬} ⊢ ∀u^{1}∀v ≤_{γ} tu(¬C(u, v) → ∃w^{0}D(u, v, w))

⇒ there exists a closed term Φ of E-HA^{ω} s.t.

E-HA^{ω}+AC+IP_{¬}+CA_{¬} ⊢ ∀u^{1}∀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 parameterfree since parameters \underline{a} in A can be taken into the comprehension together with \underline{x}, (ii) every parameter-free instance of CA_{¬} is – relative to E-HA^{ω} – equivalent to a sentence G as considered in the theorem (with A :≡ 0 = 0, x a dummy variable and s := λx.1)^{3}

∃Φ ≤ 1¬¬∀\underline{x}(Φ(\underline{x}) =_{0} 0 ↔ ¬A(\underline{x})),

with G̃ ≡ G. □

Remark 7 In the presence of CA_{¬} one can actually derive IP_{¬}.

2I.e. Φ is a primitive recursive functional in the sense of Gödel’s T.

3Here 1^{ρ} := λ\underline{v}.1^{0} for a suitable tuple of variables \underline{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 AC^{0,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 codes j(n, m) of pairs (n, m) of natural numbers n, m. j(n, m) represents the rational number \frac{n}{m+1}, if n ≤ m + 1 and 0, otherwise.

Here j e.g. is Cantor’s surjective pairing function j(x, y) := \frac{1}{2}((x + y)^{2} + 3x + y). On the codes of Q ∩ [0, 1], i.e. on IN, we have an equivalence relation by

n_{1} =Q n_{2} :≡ n_{1}, n_{2} 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 \frac{1}{k+1} instead of its code j(1, k) in IN.

By the coding of rational numbers in [0, 1] as natural numbers, sequences of such rationals are just functions f^{1} (and every function f^{1} can 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 f^{1} 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̂n := \{ \begin{matrix}fn, if ∀k, m, m̃ ≤_{0} n(m, m̃ ≥_{0} k → |fm −Q fm̃| ≤Q \frac{1}{k+1}) \\ f(n_{0} − 1) for n_{0} := min l ≤_{0} n such that \\ [∃k, m, m̃ ≤_{0} l(m, m̃ ≥_{0} k ∧ |fm −Q fm̃| >Q \frac{1}{k+1})], \\ otherwise. \end{matrix}

1) if f^{1} represents a Cauchy sequence of rational numbers in [0, 1] with modulus 1/(k + 1), then ∀n^{0}(fn =_{0} f̂n),

2) for every f^{1} the function f̂ represents 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 f̂.

Definition 9 1) f_{1} =_{IR} f_{2} :≡ ∀k^{0}(|f̂_{1}(k) −Q f̂_{2}(k)| ≤Q \frac{3}{k+1});

2) f_{1} <_{IR} f_{2} :≡ ∃k^{0}(f̂_{2}(k) − f̂_{1}(k) >Q \frac{3}{k+1});

3) f_{1} ≤_{IR} f_{2} :≡ ¬(f_{2} <_{IR} f_{1});

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 \frac{i}{3(n+1)} (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 \frac{1}{3(n+1)}–net for [0,1]. Primitive recursively in f we define

f̃(k) = μi ≤_{0} M(k)[∀j ≤_{0} M(k)(|f̂(3(k + 1)) −Q j| ≥Q |f̂(3(k + 1)) −Q i|)].

f̃ has (provably in E-HA^{ω}) the following properties (using that ˆ f̃ =_{1} f̃):

1) ∀f^{1}(f̃ ≤_{1} M).

2) ∀f^{1}(f =_{IR} f̃).

Using this construction we can reduce e.g. quantification ∀x ∈ [0, 1] A(x) to quantification of the form ∀f ≤_{1} M A(f) and equivalently ∀f^{1}A(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 (restricting w.l.g. a, x to [0, 1])

T ⊢ ∀a ∈ [0, 1](∀x ∈ [0, 1](¬¬(0 < x) ∨ ¬¬(x < a)) → ∃k^{0}(a > \frac{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(∀x^{1}(¬¬(0 <_{IR} x) ∨ ¬¬(x <_{IR} a)) → ∃k^{0}(a >_{IR} \frac{1}{k + 1})).

This is equivalent to

\begin{matrix}T ⊢ ∀a ≤_{1} M(∀x^{1}∃n ≤_{0} 1[(n = 0 → ¬¬(0 <_{IR} x)) ∧ (n ≠ 0 → ¬¬(x <_{IR} a))] \\ → ∃k^{0}(a >_{IR} \frac{1}{k+1})), \end{matrix}

which implies

\begin{matrix}T ⊢ ∀a ≤_{1} M ∀N ≤_{2} 1 \\ (∀x^{1}[(N(x) = 0 → ¬¬(0 <_{IR} x)) ∧ (N(x) ≠ 0 → ¬¬(x <_{IR} a))] → ∃k^{0}(a >_{IR} \frac{1}{k+1})). \end{matrix}

The premise ‘∀x^{1}[(N(x) = 0 → ¬¬(0 <_{IR} x)) ∧ (N(x) ≠ 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 t^{0} which can be reduced to a numeral \overline{m} s.t.

\begin{matrix}T ⊢ ∀a ≤_{1} M ∀N ≤_{2} 1 \\ (∀x^{1}[(N(x) = 0 → ¬¬(0 <_{IR} x)) ∧ (N(x) ≠ 0 → ¬¬(x <_{IR} a))] → a >_{IR} \frac{1}{\overline{m}+1}). \end{matrix}

Using AC this yields

\begin{matrix}T ⊢ ∀a ≤_{1} M \\ (∀x^{1}∃n ≤_{0} 1[(n = 0 → ¬¬(0 <_{IR} x)) ∧ (n ≠ 0 → ¬¬(x <_{IR} a))] → a >_{IR} \frac{1}{\overline{m}+1}) \end{matrix}

and hence

T ⊢ ∀a ∈ [0, 1](a pseudo-positive → a > \frac{1}{\overline{m} + 1})

which obviously is absurd. □

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 as X the Baire space with the usual metric and as Y the discrete space IN. In E-HA^{ω} the extensionality axiom implies that every functional F^{2} is a function : IN^{IN} → IN. If the above mentioned principle were derivable in E-HA^{ω}+AC then one could derive that every F^{2} is strongly extensional which in this particular case is equivalent to the statement

∀f^{1}, g^{1}(F (f) ≠_{0} F (g) → ∃x^{0}(f(x) ≠_{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ödel functional (‘Dialectica’) interpretation 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 formulation 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 interpretation (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 concerning 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 Mathematical Soc. LNS 97, Cambridge University Press (1987).

[5] Buss, S.R. (editor), Handbook of Proof Theory. Studies in Logic and the Foundations of Mathematics Vol 137, Elsevier, vii+811 pp. (1998).

[6] Goodman, N.D., Myhill, J.,The formalization of Bishop’s constructive mathematics. 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öf’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önig’s lemma. Ann. Pure Applied Logic 114, pp. 103-116 (2002).

[14] Mandelkern, M., Constructive continuity. Mem.Amer.Math.Soc. 277, Providence, 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ří Srba. Note on the Tableau Technique for Commutative Transition Systems. December 2001. To appear in the proceedings 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. December 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ård and Gudmund Skovbjerg Frandsen. An Extended Quadratic Frobenius Primality Test with Average Case Error Estimates. November 2001. 43 pp.

RS-01-44 M. Oliver Möller, Harald Rueß, and Maria Sorea. Predicate Abstraction for Dense Real-Time Systems. November 2001. 27 pp.

RS-01-43 Ivan B. Damgård and Jesper Buus Nielsen. From Known-Plaintext Security to Chosen-Plaintext Security. November 2001. 18 pp.

RS-01-42 Zoltán Ésik and Werner Kuich. Rationally Additive Semirings. November 2001. 11 pp.

RS-01-41 Ivan B. Damgård 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. October 2001. 14 pp.