What is the relationship between the BHK interpretation of propositional logic and Natural Deduction?

Question

This is a repost from MathSE.

I've been getting into intuitionistic logic lately, starting from propositional logic. I am interested in proof-theoretic semantics, meaning the idea that the truth of a proposition is derived from the existence of a proof of it. I have read different texts and while some authors mention Gentzen's Natural Deduction as the beginning of this proof theoretic semantics, many don't mention it at all and only refer to it as a proof system which is not based on axioms. Those authors generally mention the Brouwer Heyting Kolmogorov interpretation as the source of this proof theoretic point of view, or Per Martin Lof's theory of verification. My question is, how exactly are those three things related? Does Natural Deduction, except for being a proof system, provide proof theoretic semantics for propositional calculus? Lastly, what is the BHK interpretation regarded as exactly? I mean does it define a system of sorts?

Answer 1

Propositions in intuitionistic logic (IL) can be translated into S4 modal logic via the Gödel-McKinsey-Tarski translation.

IL        |  S4 Modal

A         |    □A 

A ∧ B     |    □A ∧ □B

A ∨ B     |   □A ∨ □B

A → B     |   □(□A → □B) 

¬A        |   □(¬□A)

If you read □ as something like “I can prove that…” then in effect you get the BHK interpretation of IL. BHK is not a ‘system’ just a way of understanding what an intuitionistic proposition is saying. It means that IL has the natural semantics of being the logic of proof or verifiability. By contrast, classical logic (CL) is usually understood as having the natural semantics of truth, i.e. it is concerned with what is the case, whether or not it can be verified. A valid argument in CL can be described as preserving truth, while a valid argument in IL preserves provability or verifiability.

There is no direct connection to natural deduction, since both of these logics can be expressed using it, or for that matter using sequent calculus. CL extends IL by adding the law of the excluded middle (or double negation elimination) and in the case of quantifier logic, by tweaking the quantification rules a little.

The idea that the meaning of a sentence is given by its verification conditions, as opposed to its truth conditions, was a popular one with the logical positivists. It has the consequence that if you don’t know how to verify a sentence then you don’t know its meaning, and by extension, if nobody knows how to verify it, then it is meaningless. This is one way of stating the notorious ‘verification principle’ that the positivists used to claim that much of philosophical language is indeed meaningless.

Positivism fell out of favour for many reasons, not least of which is that it doesn’t really work, although Michael Dummett continued to defend the idea that IL is the ‘correct’ logic and that the semantics of the classical logical constants cannot be justified.

As a rider, it is worth noting that the Curry-Howard correspondence, which relates proof to computability, does extend to CL. So even though CL is normally thought of as non-constructive and IL as constructive, many classical proofs can be extracted as computations. This rather blurs the line between saying that CL is about truth, and IL about provability.

Answer 2

As I understand it, any proof system can be understood as a proof theoretic semantics for the propositions in that logic. The absence of axioms in ND makes it particularly suitable for that task, as one might then be able to state purely structural properties of the proof that have significance (say, the absence of "detours"). Gentzen himself took a similar approach, but had more success with sequent calculi.

The BHK interpretation is usually not taken to be as well fleshed out as an actual mathematical construct, in particular Brower eschewed strict formalization of his discussions. However, Heyting did extensive work on formalizing the core idea behind the BHK interpretation, which is based on the notion of (constructible) evidence for propositions being the content of those propositions.

There is a lot of debate on whether a proof systems can accurately capture the propositions which are true under the BHK interpretation, or even whether this notion is meaningful. Some candidates, however are MLTT, as you mentioned, and various logical frameworks based on realizability, in the Kleene style or Kreisel's "modified" realizability.

Tying the two together, Heyting showed that there was a straightforward modification of Gentzen's natural deduction that lent itself to being translated into Kleene's realizability framework. More recently, work has shown that this can be done to some extent in sequent calculi, with the computational content of classical constructs being "suspensions" or "continuations". This is still a somewhat active field of research.