On Not Strengthening Intuitionistic Logic


Συγγραφέας: N. D. Belnap


N. D. Belnap: On Not Strengthening Intuitionistic Logic (pdf, 844K)
We wish to reexamine —-in the wake of R. E. Vesiey’s [7] —the question of converting so-called structural and intelim rules for PC], the intuitionis— tic sequenzen-kalkul of Gentzen, into rules for PCC, the classical sequenzenkalkiil. We shall limit ourselves here to sequenzen or turnstile statements of the form A1, A2, . . . , A,, |- B, where A1, A2, . . . , An, (n 20), andB are wffs consisting of propositional variables, zero or more of the connectives ‘&’, "v’, ‘~’, ‘D’, and ‘E ’, and zero or more parentheses. One can pass from _PC] to PCC by amending the intelim rules for ‘~ ’, a result of long standing, or by amending the intelim rulesqfor either one of ‘;>’ and ‘E ’, a more recent find} 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 [5]: