ELIMINATING DISJUNCTIONS BY DISJUNCTION ELIMINATION

Abstract

Abstract Completeness and other forms of Zorn’s Lemma are sometimes invoked for semantic proofs of conservation in relatively elementary mathematical contexts in which the corresponding syntactical conservation would suffice. We now show how a fairly general syntactical conservation theorem that covers plenty of the semantic approaches follows from an utmost versatile criterion for conservation given by Scott in 1974. To this end we work with multi-conclusion entailment relations as extending single-conclusion entailment relations. In a nutshell, the additional axioms with disjunctions in positive position can be eliminated by reducing them to the corresponding disjunction elimination rules, which in turn prove admissible in all known mathematical instances. In deduction terms this means to fold up branchings of proof trees by way of properties of the relevant mathematical structures. Applications include the syntactical counterparts of the theorems or lemmas known under the names of Artin–Schreier, Krull–Lindenbaum, and Szpilrajn. Related work has been done before on individual instances, e.g., in locale theory, dynamical algebra, formal topology and proof analysis.