Content area
Full Text
Abstract.
The standard omniscience principles are interpreted in a systematic way within the context of binary trees. With this dictionary at hand we revisit the weak König lemma (WKL) and Brouwer's fan theorem (FAN). We first study how one can arrive from FAN at WKL, and then give a direct decomposition, without coding, of WKL into the lesser limited principle of omniscience and an instance of the principle of dependent choices. As a complement we provide, among other equivalents of the standard omniscience principles, a uniform method to formulate most of them.
(ProQuest: ... denotes formulae omitted.)
1. Introduction
This paper begins with a systematic interpretation in the context of binary trees of the following fragments of the law of excluded middle: the limited, the weak limited, the lesser limited, and the weak lesser limited principle of omniscience; and Markov's principle.
Using this interpretation, we study the interrelations of the following properties, including their negations and double negations, of a binary tree ?: G is finite; ? is well-founded; G has an infinite path. This enables us to decompose the weak König lemma into the fan theorem and a higher-type instance of the law of excluded middle.
We further have a closer look at the two fragments of De Morgan's law that occur in this context: the lesser limited and the weak lesser limited principle of omniscience. Among other things, the former principle proves tantamount to a variant of the weak König lemma.
Next, we consider some forms of countable and dependent choice for disjunctions, and show how the weak König lemma can be decomposed into such a form of dependent choice plus the lesser limited principle of omniscience. Finally, we provide a uniform method to formulate all but one of the aforementioned fragments of the law of excluded middle: as the implication from ? =? ? to -?? ? restricted to certain classes of assertions A, B.
This paper is a contribution to the constructive variant, put forward as a programme in [15, 16], of "reverse mathematics" [31]. 1 An...