Matters of separation.
Hugues Leblanc, R. K. Meyer · Notre Dame Journal of Formal Logic · 1972
Extending in some respects, sharpening in others, results in the literature, we establish here that:(1) Every classically valid wff A of QC=, the first-order quantificational calculus with identity, is provable by means of axiom schemata A1-A3 and rule Rl in Table I, plus the axiom schemata and rules of that table for only such of the logical symbols ζ ~'9 '&', Ύ', c =\ 'V, '3', and '=' as occur in A,(2) Every intuitionistically valid wff A of QC= is provable by means of axiom schemata A1-A2 and rule Rl in Table I, plus the axiom schemata and the seven rules of that table for only such of the logical symbols in question as occur in A.In the first of our two theorems R2 is to serve as rule for 'V; in the second, R2 or R2 ; according as '&' occurs or not in A. TABLE I Axiom schemata For o> : Al. A15. (A 3 5) 3 ((i? D A) D (A Ξ 5)) For 'V: A16. (VX) A Z) A(Y/X) For '3': A17. A(F/X) z> (3X)A