Midlands Logic Seminar

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 Y ≠ S 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.