Orador: René Gazzari

(investigator do CMAT)

Data:  21 de Nov, as 15h

Local: a definir

Titulo: Proving Lindenbaum Conditionals – But without the Axiom of Choice!

Sumario: Lindenbaum’s Theorem (LT) plays a small, but crucial role in the completeness proofs of logic. The general version of this theorem formulated for deductive systems (a set theoretical abstraction of logic introduced by Tarski [3]) turns out to be equivalent to the Axiom of Choice (AC). Investigating the respective proofs, Miller [2] observes that a restricted version of LT is already sufficient to prove AC. He concludes that this constitutes a proof of the conditional that the restricted (and apparently weaker) version of LT implies its general version, but with a detour via AC. At this point, Miller raises the problem of providing a direct proof of this conditional, not using AC, but remaining completely in the context of deductive systems. Proving conditionals between intermediate versions of LT, some partial solutions were provided by Miller, some more by Gazzari [1], but the main problem was not solved. In the first part of our talk, we provide the necessary details needed to understand Miller’s problem, including a brief introduction into deductive systems, and sketch of the partial solutions. In the second part, we consider a proof theoretic strategy to solve the problem: the main idea is to start with the well-known proofs establishing the required conditional between both versions of LT via AC and to transform this composed proof into a direct proof with the desired properties.