# BHK Semantics and Homtopy Type Theory

There are different ways of associating interpretations to intuitionistic propositional logic, one of which is to interpret it by Heyting algebras this is the analogue of the standard interpretation of classical logic by Boolean algebras.

Tarski, the On the Concept of Truth in Formal Languages, argued for a properly semantic interpretation of truth, where for example the following sentence:

'p is true' iff p is true

or to give an example in plain English

'Snow is white' iff Snow is white

In both instances the the first sentence is placed in quotes since it should be seen as a purely formal, that is it is built up purely from the grammatical features of the language under consideration.

In this Tarski was considering solely classical logic, and the interpretation is the logical form of the philosophical position of correspondance, where true linguistic propositions correspond to actually true propositions of the world ( the resemblance to model theory here is unmistakable). in the corresponding interpretation of this for intuitionistic logic, the so called BHK interpretation (for Brouwer, Heyting & Kolgomorov), the position is what one might call a constructive position, in that one must supply an account justifying the proposition, that is:

'snow is white' iff Snow is White and this is why...

the formal analogue of this is

'p is true' iff p is provable

One might then associate to the formal proposition all proofs of that proposition. The BHK interpretation also stipulates that each proof is modifiable into another.

Philosophically speaking why should I expect there to be such a mapping? If I have two proofs of a certain proposition why should I expect there to be some means of modifying the first proof into the second?

Presumably this is where homotopy comes in - if we conceive a proof as a path from axioms to the proposition and think of such a modification as a homotopy - a proof that one proof can be modified into another. And then we can carry on further and ask for homotopies between homotopies.

(Homotopy in topology is analytic, in that the paths are built out of points. We could conceive here a proof as analytic in that a proof is built out of propositions linked together via inference rules, but one could take a possibly synthetic approach, I expect, where proofs themselves are basic and not analysable into propositions).

Is this because we can conceive of a proof also as a proposition, or to be more precise, we can see the following as a purely grammatical proposition?

'proof P of p can be modified into a proof Q of p'

• I agree. Recall the relation of beta/weak reduction between terms in the simply typed lambda calculus/combinatory logic. From the Curry-Howard perspective, if term A reduces to term B, then there is a corresponding simplification of a proof of a proposition (that is the subject of term A) to a proof of another proposition (that is the subject of term B). This simplification is obviously a modification relation, but it's certainly not true that for arbitrary terms A,B we have: A reduces to B or B reduces to A, so there may be proofs that aren't linked by this modification relation. Mar 7, 2014 at 7:09