On not strengthening intuitionistic logic.
Nuel Belnap, Hugues Leblanc, Richmond H. Thomason · Notre Dame Journal of Formal Logic · 1963
We wish to reexamine -in the wake of R. E. Vesley's Γ7] -the question of converting so-called structural and intelim rules for PC/, the intuitionistic sequenzen-kalkύl of Gentzen, into rules for PCc, the classical sequenzenkalkίil.We shall limit ourselves here to sequenzen or turnstile statements of the form A l9 A 2 , . . ., A n h B, where A u A 2 , . . ., A n , (n s* 0), and B are wff s consisting of propositional variables, zero or more of the connectives '&', \' f '~', tf ^>', and 6 =\ and zero or more parentheses.One can pass from PC] to PCc by amending the intelim rules for ζ ~9, a result of long standing, or by amending the intelim rules for either one of ζ 'Ό 9 and ' Ξ ', a more recent find. 1 In a talk at Yale University in 1961, however, Leblanc conjectured that amending the intelim rules for either one of '&' and 'V' will not do the trick.The point, mentioned in Leblanc [4], appears as follows in Leblanc and Belnap [5J:We also conjecture, by the way, that any structural rule which holds in PCc also holds in PCy, that any elimination or introduction rule for '&' and V which holds in PCc also holds in PCi, and hence that the only way of turning standard Gentzen rules of inference for PCi into rules for PCc is to strengthen the elimination or introduction rules for *~9 or those for ' D ', or those for '='.Leblanc's conjecture, to which we devote the rest of this paper, has had a rather checkered career: proved true at one time or another by three different writers in two different ways, it has also been proved false once. 2 To resolve this seeming contradiction and sort out what has been proved true and what false, we shall have another look at some of the key terms in the above quotation.It will turn out that the readings of Leblanc's conjecture in [l], [2], and [7] are not quite apposite, and that of two fresh ones which we consider here one is unrestrictedly true, while the other holds under a slight restriction.