|
Lidenbaum Maximalization Theorem
René Gazzari
Department of Computer Science, University of Tübingen, Germany
Department of Philosophy, PUC-Rio, Brazil
rene.gazzari@uni-tuebingen.de
Lindenbaum’s Theorem plays a small, but essential role within the canonical proof of the Completeness Theorem in logic: Lindenbaum’s Theorem provides maximal consistent extensions of consistent theories and allows, due to the max- imality of those extensions, the construction of models.
Usually, Lindenbaum’s Theorem is proved by an application of a set-theoretical theorem, as the Axiom of Choice or Zorn’s Lemma. Thereby, Lindenbaum’s Theorem is a non-constructive method for obtaining special logically relevant objects, similarly to theorems of other disciplines of mathematics such as, for example, Hahn-Banach Theorem in functional analysis, Krull’s Theorem in ring theory et cetera.
- First Session -
In the first session, we follow Tarski’s abstract approach to logic and introduce deductive systems and consequence operations. In this context, we are able to present the original version of Lindenbaum’s Theorem (provable in set theory without the Axiom of Choice).
Due to the abstract approach, we find a great number of versions of this theorem: within logic we find versions of Lindenbaum’s Theorem of different logical strength related to specific kinds of logic (as, for example, propositional logic, classical logic or intuitionistic logic). But we also can identify versions of Lindenbaum’s Theorem with respect to non-standard interpretation of deductive systems.
In this tutorial we are especially interested in some special versions of Lin- denbaum’s Theorem, formulated in the abstract context of (slightly generalised) deductive systems, all equivalent to the Axiom of Choice. By these equivalences we have an indirect prove (via the axiom of choice) that the special versions are all equivalent among each other.
- Second Session -
In the second session, we investigate a problem raised by Miller. He demands to re-prove the equivalence of the special versions of Lindenbaum’s Theorem, but allows only proofs without an application of the Axiom of Choice.
We discuss the standard set-theoretical approach of Miller and Gazzari to this mathematical problem and provide some partial solutions based on special constructions of deductive systems. From a mathematical point of view, those partial solutions are unproblematic.
But from a more philosophical perspective, we observe a problem: having only an informal description of our restrictions on proofs it is not clear, whether those solutions satisfy our own demand for avoiding the Axiom of Choice or not. There are crucial philosophical questions, which need some (formal) clarification in order to get an adequate criterion for our problem. In particular:
• What does it mean to avoid an axiom in a proof ?
• What does it mean to avoid a detour in a proof ?
• Which formulae qualify to be a version of Lindenbaum’s Theorem?
We sketch our ideas towards a formal criterion for our demands under the light of the philosophical problems and discuss the relationship of this criterion to pure, direct or simple proofs.
- Third Session -
In the third session, we discuss a proof-theoretical approach to find a proof of the equivalence of the special versions of Lindenbaum’s Theorem such that the Axiom of Choice is not applied.
We investigate composed proofs of the desired equivalence, which first prove a variant of the Axiom of Choice out of a special version of Lindenbaum’s Theorem before inferring another version of Lindenbaum’s Theorem. Clearly, such proofs do not satisfy our demands.
But analysing the normalisation of proofs, we will argue that the normal form of the composed proof has changed relevant properties. Our claim is that this resulting proof satisfies any adequate formalisation of our intuitive demands with respect to the application of the Axiom of Choice.
|
|
Bibliography
• R. Gazzari, Direct Proofs of Lindenbaum Conditionals. Logica Universalis 8 (2014), 321-343.
• D. W. Miller, Some Lindenbaum Theorems Equivalent to the Axiom of Choice. Logica Universalis 1 (2007), 183-199.
• A. Tarski, Fundamental Concepts of the Methodology of the Deductive
Sciences.
in: A. Tarski, Logic, Semantic, Metamathematics. Clarendon Press, Ox- ford, 1956, 60-109.
• A. Tarski, Foundations of the Calculus of Systems. in: A. Tarski, Logic, Semantic, Metamathematics. Clarendon Press, Ox- ford, 1956, 342-3
|