On strengthening intuitionistic logic.
R. E. Vesley · Notre Dame Journal of Formal Logic · 1963
Leblanc and Belnap [2] have shown that standard Gentzen rules of inference (N-version) for intuitionistic propositional calculus (PCj) become rules for classical propositional calculus (PC^) upon strengthening the '='elimination rule.They conjecture that PCj can be strengthened to PC^ only by strengthening rules for *nJ or '3* or f =\ We show that the addition of a clause (c) to their two part V-introduction rule turns their formulation of PCr into one of PCr The new rule is: DI C : (a) A f-A v B, (b) B f-A v B, (c) // \-A* and A, P \-Q, then \-A v P,