Independence questions in a finite axiom-schematization of first-order logic

Abstract

We review some independence results in a finite axiom-schematization of classical first-order logic introduced by Norman Megill. We also prove that a certain axiom scheme of this system is independent although all of its instances are provable from the other axiom schemes.

arXiv comment25 pages; v2: typos, add a partial independence result; v3: revisions following reviewer's remarks: strengthen Prop 1.1, new Prop 1.2 (to fix proof of Prop 3.5), new Prop 1.4, strengthen and/or fix independence results for modus ponens, peirce, generalization, spec, modal5, equality axioms, predicate axioms, vacGen, new Prop 3.11, various clarifications and typos