An Automated Derivation of Frege's 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 foundational to the study of logic. Using an automated deduction system, I show that the sentential calculus of Frege's Begriffsschrift, the first sentential calculus, can be derived from Lukasiewicz's CN; the proof appears to be novel.