Constructive connections between anti-Specker, positivity, and fan-theoretic properties

From NZJM

Jump to: navigation, search

New Zealand Journal of Mathematics

Vol. 44, (2014), Pages 21-33


Douglas Bridges

University of Canterbury,

Private Bag 4800,

Christchurch 8140,

New Zealand

mailto:douglas.bridges@canterbury.ac.nz

James Dent

mailto:semajdent@gmail.com

Maarten McKubre-Jordens

University of Canterbury,

Private Bag 4800,

Christchurch 8140,

New Zealand

mailto:maarten.jordens@canterbury.ac.nz


Abstract Two weakenings of the anti-Specker property---a principle of some significance in constructive reverse mathematics---are introduced, examined, and in one case applied, within Bishop-style constructive mathematics. The weaker of these anti-Specker properties is shown to be equivalent to a very weak version of Brouwer's fan theorem. This leads to a study of antitheses of various types of fan theorem---in particular, to new proofs of Diener's theorem on the equivalence of some of these antitheses. In addition, the antithesis of the positivity principle for uniformly continuous functions on [0,1] is shown to be equivalent to that of the fan theorem for detachable bars. Finally, a positivity principle for pointwise continuous functions is examined, partly in order to provide a neat application of the stronger of the two anti-Specker properties introduced early in the paper.

Keywords constructive mathematics; Bishop; fan theorems; Specker's theorem; anti-Specker; positivity principles.

Classification (MSC2000) 03F50.

Full text

Full paper

Personal tools