BHK Semantics and Homtopy Type Theory

Question

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'

Answer 1

It is correct that in homotopy type theory two terms x1, x2 : X of type X may be different, while being equivalent, as witnessed by an equivalence or homotopy between them. Since under BHK we may think of x1 and x2 as being proofs of a proposition -- namely the proposition represented by the (-1)-truncation isInhab(X) of X, this means that these two proofs are thereby equivalent.

Regarding the discussion in the comments above, notice that one needs to distinguish here the type X from its (-1)-truncation isInhab(X). Not every two terms of the former need to be connected by a homotopy, this will only be the case if X is a connected type. On the other hand, by construction any two terms of isInhab(X) are equivalent, reflecting the fact that this is really a mere proposition.

Finally regarding the statement that homotopy is "analytic, in that the paths are built out of points": this is really only true in the particular presentation of homotopy theory by topological spaces up to weak homotopy equivalence. Arguably more "direct" is the presentation by infinity-groupoids which, specifically when thought of as Kan complexes. In this presentation homotopies are "elementary" and not "built out of points".