On the Relation Between Heyting's and Gentzen's Approaches to Meaning

Abstract Proof-theoretic semantics explains meaning in terms of proofs. Two different concepts of proof are in question here. One has its roots in Heyting's explanation of a mathematical proposition as the expression of the intention of a construction, and the other in Gentzen's ideas about how the rules of Natural Deduction are justified in terms of the meaning of sentences. These two approaches to meaning give rise to two different concepts of proof, which have been developed much further, but the relation between them, the topic of this paper, has not been much studied so far. The recursive definition of proof given by the so-called BHK-interpretation is here used as an explication of Heyting's idea. Gentzen's approach has been developed as ideas about what it is that makes a piece of reasoning valid. It has resulted in a notion of valid argument, of which there are different variants. The differences turn out to be crucial when comparing valid arguments and BHK-proofs. It will be seen that for one variant, the existence of a valid argument can be proved to be extensionally equivalent to the existence of a BHK-proof, while for other variants, attempts at similar proofs break down at different points.

Keywords Proof • Valid argument • Meaning • Semantics • Heyting • Gentzen

Introduction

The term “proof-theoretic semantics” was introduced to stand for an approach to meaning based on what it is to have a proof of a sentence. The idea was, at least originally, that in contrast to a truth-conditional meaning theory, one should explain. This is an elaborated version of a talk at the “Second conference on proof-theoretic semantics” at Tübingen in March 2013. Earlier versions have also been presented elsewhere and have been circulated among some colleagues, which has given me the benefit of several comments. I thank especially Per Martin-Löf, Peter Schroeder-Heister and Luca Tranchini for their suggestions, which have stimulated me to prove stronger results and to improve the presentation the meaning of a sentence in terms of what it is to know that the sentence is true, which in mathematics amounts to having a proof of the sentence ^[1].

There are in particular two different concepts of proof that have been used in meaning theories of this kind, but the relation between them has not been paid much attention to. They have their roots in ideas that were put forward by Arend Heyting and Gerhard Gentzen in the first part of the 1930s. Their approaches to meaning are quite different and result in different concepts of proof. Nevertheless there are clear structural similarities between what they require of a proof. The aim of this paper has been to compare the two approaches more precisely, in particular as to whether the existence of proofs comes to the same.

I shall first retell briefly how Heyting and Gentzen formulated their ideas and how others have taken them. In particular, I shall consider how the ideas have been or can be developed so that they become sufficiently precise and general to allow a meaningful comparison, which will then be the object of the second part of the paper.

• [1] Schroeder-Heister (2006) [22], who coined the term and used it as the title of a conference that he arranged at Tübingen in 1999, writes that proof-theoretic semantics “is based on the fundamental assumption that the central notion in terms of which meanings can be assigned to expressions of our language … is that of proof rather than truth”