Home Philosophy Advances in Proof-Theoretic Semantics
A First Comparison Between Heyting's and Gentzen's Approaches
Both Heyting and Gentzen approached questions of meaning in relation to what it is to prove something, but as seen from the above, their approaches were still very different. Gentzen was concerned with what justifies inferences and thereby with what makes something a valid form of reasoning. These concerns were absent from Heyting's explanations of mathematical propositions and assertions. The constructions that Heyting refers to in his meaning explanations, called proofs in the BHK-interpretation, are mathematical objects, naturally seen as belonging to a hierarchy of effective operations as suggested by Kreisel. They are not proofs built up from inferences. Nor does a proof in Heyting's sense, the realization of an intended construction, constitute a proof built up of inferences, although it does constitute what is required to assert the proposition in question. As was later remarked by Heyting (1958) , the steps taken in the realization of the intended construction, in other words, in the construction of the intended object, can be seen as corresponding to inference steps in a proof as traditionally conceived.
These differences between what I am calling BHK-proofs and Gentzen proofs do not rule out the possibility that the existence of such proofs nevertheless comes materially to the same. For instance, a BHK-proof of an implication A ⊃ B is defined as an operation that takes a BHK-proof of A into one of B, and a closed Gentzen proof of A ⊃ B affords similarly a construction that takes a Gentzen proof of A into one of B; the latter holds because the validity of a closed deduction of A ⊃ B guarantees a closed valid deduction in canonical form (by principle II when seen as a clause in an inductive definition) containing a valid deduction of B from the assumption A (principle I), which gives rise to a closed valid deduction of B when a closed valid deduction of A is substituted for the assumption (principle III). Such similarities may make one expect that one can construct a BHK-proof given a Gentzen proof and vice versa.
However, the ideas of Gentzen discussed above are confined to a specific formal system with particular elimination rules associated with reductions, while there is no comparable restriction of the effective operations that make up a BHK-proof. It is easily seen that for each (valid) deduction in that system there is a corresponding BHK-proof (provided that there are BHK-proofs corresponding to the deductions of atomic sentences), but the converse does not hold. For instance, there is a BHKproof (over the set of proofs of arithmetical identities) of the conclusion obtained by an application of mathematical induction if there are BHK-proofs of the premisses, but there is no corresponding valid deduction unless we associate a reduction to applications of mathematical induction. If Gentzen proofs are to match BHK-proofs, Gentzen's ideas have first to be generalized, making them free from any particular formal system.
|< Prev||CONTENTS||Next >|