Home Philosophy Advances in Proof-Theoretic Semantics
Further Development of Gentzen's Ideas
The generalization to be considered in this section will retain Gentzen's ideas of explaining the meaning of sentences in terms of certain canonical forms of reasoning and of connecting the meaning so explained with the justification of inferences. It should be mentioned however that Gentzen's and Heyting's ideas have also been developed in another way, resulting in a certain fusion of their ideas. The explanations in the BHK-interpretation may be enriched by saying à la Gentzen how proofs of sentences of various forms can be constructed. To Gentzen's introduction rules there then correspond canonical ways of forming BHK-proofs of compound sentences from BHK-proofs of the constituents, while to the elimination rules there correspond operations on BHK-proofs to BHK-proofs defined in essentially the same way as the reductions in natural deduction. These correspondences, which further develop the Curry-Howard isomorphism (Howard 1980 ), constitute cornerstones of MartinLöf's type theory (see especially Martin-Löf 1984 [15, p. 24]). In the other direction, I have suggested that a legitimate inference is to be seen as involving not only a transition from assertions to assertions but also an operation on grounds for the premisses that yields a ground for the conclusion, where grounds are BHK-proofs formed in the way just described (Prawitz 2015 ).
In this paper, I am not concerned with such fusions of Heyting's and Gentzen's ideas, but want to compare BHK-proofs with forms of reasoning that appear as valid in accordance with Gentzen's ideas about the justification of inferences, sufficiently generalized.
In outline the general idea is this: We consider pieces of reasoning, which will be called argument structures, proceeding by arbitrary inferences, and possible justifications of these inferences in the form of a set of reductions. An argument structure paired with a set of reductions is called an argument, and we define what it is for an argument to be valid by essentially the same three clauses that defined the notion of valid deduction. I shall develop two new notions of validity, called weak and strong validity. They are variants of notions of valid arguments that have been proposed earlier , and will be shown to have distinct features that are especially important when it comes to compare valid arguments and BHK-proofs.
At the end of the paper, I reflect upon the fact that all the variants of valid arguments considered so far deviate in one important respect from the intuitions connected with Gentzen's approach as described above, and point to how the notion of justification may be developed in another way that stays closer to the original ideas.
|< Prev||CONTENTS||Next >|