Two separation theorems for natural deduction.
Hugues Leblanc · Notre Dame Journal of Formal Logic · 1966
Extending a result of mine in [7], I shall first establish that a Gentzen sequent of the sort A\yA.2a ... , An -^ B)where A^A^ . . .y A n (n ^0), and B are wffs of the first-order functional calculus (FC), is invariably provable -when intuitionistically valid-by means of the four structural rules R, E, P, and C in Table I below and the intelim rules of that table for such (and only such) of the seven operators '~', 'D', '&', V, '=\ <V, and '3' as occur in the sequent.I shall then establish that, save when in {v,V}, {v,&,V}, {v,V,3}, or {v,&,V, 3}, a sequent of the selfsame sort is provable -when classically valid-by means of R, E, P, C, and the intelim rules of Table ΠI below for such (and only such) of the seven operators '~9 9 'D', '&', 'v', '=', 'V', and '3' as occur in the sequent.The two results have interesting corollaries: one to the effect that a wff A of FC, when intuitionistically implied by a set S of wffs of FC, is invariably deducible from S by means of rule GR' in Table VI below and the intelim rules of that table for such (and only such) of the seven operators ( ~\ *D', '&', 'v', ζ =' 9 'V\ and '3' as occur in a member of S or in A\ another to the effect that A, when classically implied by S, is in all but four cases deducible from S by means of GR T and the intelim rules of Table VII below for such (and only such) of the seven operators in question as occur in a member of S or in A. IWith all seven of <~', 'D', <&', <v', <=',