A rule-completeness theorem.
Nuel Belnap, Richmond H. Thomason · Notre Dame Journal of Formal Logic · 1963
From an intuitive standpoint it would seem that the connectives of conjunction and disjunction assume in intuitionistic logic the same role as in classical logic.We may lend precision to these intuitive ideas by considering Gentzen's formulation of intuitionistic logic, which separates the deductive roles of the various logical connectives, defining each connective by a pair of rules added to a structural system.Though it is possible to convert a Gentzen formulation of intuitionistic logic (with singular right sides) into a classical two-valued system by altering the rules for negation, implication, or equivalence, Leblanc has conjectured that no classically valid changes in structural rules (i.e., rules exhibiting no connectives) or rules for conjunction or disjunction can have this effect.We here verify this conjecture by showing that the conjunction-disjunction fragment is "rule-complete" (in a sense to be specified) under the ordinary two-valued interpretation.Notation.Let q ί9 q i7 . . .range over propositional variables, and A, B, A^ . ..over well-formed formulas (wffs) defined by the conditions (i) q l9 q 2 , . . .are well-formed, and (ii) if A and B are well-formed, then so are (A A β) and (A v B).Let S y S lf . . .range over statements having the form (I) A u ...,A n \-B.Let Oί and β range over finite (possibly null) sequences of well-formed formulas separated by commas, and let Σ, Σi, Σ 2 range over finite (possibly null) sequences of statements having the form (I).