Gentzen has proved cut-elimination and normalization theorems for sequent and natural deduction calculi. These theorems, it is sometimes said, convey information about the proofs represented by the derivations of these calculi. This dissertation is concerned with investigating this claim. ;The partial correspondence between the two theorems is described and the reasons why it is only partial are explained in terms of certain deficiencies of natural deduction systems. It is then argued that any s…
Read moreGentzen has proved cut-elimination and normalization theorems for sequent and natural deduction calculi. These theorems, it is sometimes said, convey information about the proofs represented by the derivations of these calculi. This dissertation is concerned with investigating this claim. ;The partial correspondence between the two theorems is described and the reasons why it is only partial are explained in terms of certain deficiencies of natural deduction systems. It is then argued that any system which purports to represent proofs will suffer from these or related deficiencies, and that this poses problems for the interpretation of Gentzen's theorems in terms of proofs. A multiple-conclusion version of natural deduction is then presented, and Gentzen's theorems are extended to it and compared with one another. Finally, it is argued that the obstacles in the way of establishing a full correspondence between the theorems and of interpreting them as conveying information about proofs indicate that traditional ideas about proofs are too narrow
