An Automated Derivation of the Hilbert/Ackerman Grundzuege Sentential Calculus from Lukasiewicz's CN

摘要

Two logics are implicationally equivalent if the axioms and inference rules of each imply the axioms of the other. Characterizing the inferential equivalences of various formulations of the sentential calculi is thus foundational to the study of logic. Using an automated deduction system, I show that the sentential calculus, here called GTL, of Hilbert/Ackerman's Grundzuege der theoretischen Logik, can be derived from Lukasiewicz's CN. Although each of these systems is known to imply the other, the proof presented here appears to be novel. The automated prover first develops a single set of lemmas and propositions - an elementary "core" theory - that constitutes a large fraction of the proofs of five of the six axioms of the "Grundzuge" calculus. In passing, the proofs show that one of the "Grundzuge" axioms can be regarded as a lemma in the proofs of three of the other axioms of that system.