D-COMPLETE AXIOMS FOR THE CLASSICAL EQUIVALENTIAL CALCULUS
Dolph Ulrich · 2005
Virtually all previously known axiom sets for the classical equivalential calculus, EQ, are D-incomplete: not all theorems derivable by substitution and detachment can be derived using the rule D of condensed detachment alone. The only exception known to the author is Wajsberg’s base fEEpEqrErEqp, EEEppppg. This axiom set, albeit inorganic since one of its members contains a theorem of EQ as a proper subformula, is here shown to be D-complete. D-complete single axioms for EQ are then constructed, culminating with EEpqEErqEsEsEsEsEpr which has the distinction of being both D-complete and organic.