Week 3, 28 January (17:00-19:00 Watson 310)

Study group: HoTT chapter 2

Speaker: David Miller (Warwick)
Proving choice without choice


The Lindenbaum extension theorem (used in many proofs of the completeness theorem for elementary logic) says that if the zero element S of a deductive system is finitely axiomatizable then every consistent theory has a maximal consistent extension; that is, if YS then Y can be extended to a theory Z whose only proper extension is S. Maximal consistency can be generalized in this way: Y is y-saturated iff Y does not imply y but every proper extension of Y implies y. The Lindenbaum theorem (and its proof) can be generalized likewise: for every deductive system, if Y does not imply y then Y has a y-saturated extension. Each version of the Lindenbaum theorem is implied by the axiom of choice AC, which is usually cited in the proof of the theorem.

Although the original Lindenbaum theorem for classical logic is known to be strictly weaker than AC, Dzik (1981) proved that the generalized Lindenbaum theorem is equivalent to AC. His proof of AC, however, assumes much less than the Lindenbaum theorem itself. It is enough to assume, for example, that for every extremal deductive system, if Y does not imply y then Y has a y-saturated extension, where a system Cn is called extremal if for any set X, Cn(X) takes either the (set-theoretically) smallest possible value X or the largest possible value S. The question accordingly arises whether the generalized Lindenbaum theorem for all systems can be proved directly from its restriction to extremal systems, that is, without a detour through AC (to which both forms of the theorem are equivalent).

In 'Some Restricted Lindenbaum Theorems Equivalent to the Axiom of Choice' (Logica Universalis 1, 2007, pp.183-199) I made a start on this and similar questions. The investigation has been imaginatively extended by René Gazzari ('Direct Proofs of Lindenbaum Conditionals', Logica Universalis, 2013, published on line 27.viii.2013). In the present talk I should like to look at one or two of Gazzari's improvements, and also to discuss some of the philosophical questions he raises about the directness of the direct proofs that he and I claim to have presented.

About the seminar

The Midlands Logic Seminar was founded in 2011 and aims to cover all areas of mathematical logic, as well as related areas of theoretical computer science, and philosophy of mathematics.


All meetings for Term 2, 2013-14 will be Tuesday from 17:00-19:00 in room 310 of Watson Building (School of Mathematics) on the campus of the University of Birmingham.
  • campus map
  • google maps
    To get to campus, take the train from Birmingham New Street to the University stop (7 minutes).


    Dr Richard Kaye
    School of Mathematics
    University of Birmingham


    Dr Walter Dean
    Department of Philosophy
    University of Warwick