[FOM] A Meaning Explanation for HoTT?

Thu Apr 14 18:16:14 EDT 2016

> I would be very interested to see an approach to general foundations
> for mathematics based on your
> 
> shape, point, symmetry, observation, juxtaposition, amalgamation, path.
> 
> So go ahead and start presenting this.

OK, well, here goes. But first some disclaimers and clarifications:

1) This is my own explanation. I used it to convince myself and it was for my own personal reasons that I thought about it. So I am only speaking for myself here. No-one in the HoTT/UF community endorses or even knows about this. You should not in any way take this to be a way of thinking that anyone in the HoTT/UF community would subscribe to. I am certainly not convinced that it can be communicated clearly, nor that there is any point to do so. But it did help me feel “safer” with HoTT — and that’s all I can say about it. Since there has been a lot of copy-pasting on several forums, I would ask that if anyone copies what I say below anywhere else to please include this disclaimer. 

2) The issue of providing a “meaning explanation” (to borrow Martin-Löf’s [1] term) for HoTT seems not to be an active concern for the HoTT/UF community. Philosophically, I think this is a mistake. Pragmatically, I find it fully justified, since progress towards such a meaning explanation is unlikely to provide any new tool, nor have anything to say about new (formal) models of HoTT. Most of the HoTT/UF community is engaged in providing *formal* meaning explanations, i.e. interpretations into other formal systems. This is done with the simplicial model [2] and the cubical model [3] and in far more generality in Voevodsky’s project described here [4,5]. Friedman’s question, however, is not about such a formal interpretation, as I think has now become clear. 

3) The idea of such a meaning explanation is to provide a justification of the rules of HoTT that is *fully* independent of set theory. Many of the terms I will use have formal counterparts in set theory (e.g. “shape” could be made precise as a CW complex defined in some set theory) but they are not to depend on those formal counterparts in any way. They are meant to be intuitive. Thus, the question I want to tackle here is the following: What, if any, is the *intuitive* justification of the validity of the rules of (any) HoTT? Such an endeavor, to quote Martin-Löf, is

"[a] genuinely semantical or meaning theoretical investigation, which means that [one] must enter on something that [one] is not prepared for as a mathematical logician, whether model theorist or proof theorist: [one] must enter on an enterprise which is essentially philosophical or phenomenological [...] in nature. ([6], p. 408)"

This is what this is about. 

4) I will start doing this piece by piece, because I don’t want to write something massive if there are going to be too many objections at the very beginning. So this will be the first of maybe more installments if some consensus can be reached on everything I have included here.

5) I do not see this as a “challenge” or as a “war”. I see it as a healthy and lively conversation. I am not willing to argue at all about whether HoTT or ZFC does this or that “better”. I disagree with Friedman that “I can do better what you can do” is the right attitude to take here. This is not the attitude with which I am engaging with him, if that is indeed that attitude he has.  So what follows is not at all meant in the spirit of “throwing a gauntlet”. But I certainly think that the questions Friedman asks are important and need to be answered and it is of no use for people on any “camp” to say in response to such questions that “you have to be an expert to understand”. 

With that, I begin.

A. THE BASIC IDEA

As a formal system, HoTT differs from ZFC (understood as FOL=+axioms of ZFC) in that there are only inference rules and there is no a priori inductive construction of well-formed formulas. This means that a meaning explanation will have to involve *only* the justification of a certain number of inference rule, rather than to provide an argument for the “truth” of the axioms of ZFC, assuming that the inference rules of FOL= have already been justified. In other words, there is no ambient logic in MLTT or HoTT. So the seven notions I spoke about do not correspond to the membership relation. They correspond to the [membership relation + FOL=]. I hope this distinction is clear.

So with this in mind, here is the basic idea:

BASIC IDEA: The rules of HoTT are instructions for constructing new shapes from old.

A little more, but not fully, precisely: the meaning of type constructors and term constructors consists in describing what can be done on previously constructed shapes and their points. The rules of the system are then justified by arguing that moving from a given observation of a shape to to a new one is *correct*. And what is *correct* is determined by our spatial intuition. A little more, but not fully, precisely: a rule is justified if certain observations allow you to make certain other observations, based only on your spatial intuition. For a trivial example: If one can observe a transparent cube, one can also observe a square by shifting the cube around so that the “front” and “back” faces coincide. This is the kind of intuitive correctness I speak of, easily visualizable and immediate.

B. JUDGMENTS AS OBSERVATIONS

As may be clear to those with some familiarity with MLTT, what I am calling "observations'' refer to what in type theory are called "judgments’’.* So let me begin by giving the general meaning of the four kinds of observations. In MLTT we have (or "minimally'' have) the following judgments:

(1) Γ |- a : A
(2) Γ |- a=a' : A
(3) Γ |- a : A  Type
(4) Γ |- Α = A’ Type 

From now on I will call these judgment “observations” and re-write the last two more suggestively as follows (even though this formal notation means nothing at this point):

(1) Γ |- a : A
(2) Γ |- a=a' : A
(3) Γ |- a : A  Shape
(4) Γ |- Α = A’ Shape

The meaning of these four observations is then to be understood as follows (in the same order):

(1) From viewpoint Γ, a is a point of A
(2) From viewpoint Γ, a and a' are symmetric as points of A
(3) From viewpoint Γ, A is a shape
(4) From viewpoint Γ, A and A' are symmetric as shapes

As one can see, there are thus four new basic notions, on which the whole proposed meaning explanation is supposed to rest:

(1) Viewpoint (replacing "context'')
(2) Point (replacing "term'')
(3) Shape (replacing "type'')
(4) Symmetric (replacing "judgmentally equal'')

I claim that these four basic notions are intuitive enough to justify basing a meaning explanation upon. Inevitably, it is some kind of spatial intuition that has to be invoked. We can argue about the content of this intuition all we like -- but, for now, all that I require is that these notions are sufficiently primitive. I believe they are.

A feature of this set-up which may already appear striking is the absence of any mention of “truth". This is both intentional and, to a certain extent, inevitable. The ``observations'' of the four basic types (1)-(4) above are best understood within a ``problems-and-constructions'' view of mathematics, closer in spirit to the Euclid than to Russell. A notion of truth can then be recovered as a degenerate notion of construction, namely when we ignore all details of the construction itself and retain only the information that it exists (or that it is possible). 

This is the end of the first installment. I will see the reaction to this and decide if it is worth continuing. As a preview, for those with some familiarity with the formalism, the basic idea for the next part of the meaning explanation is the following: Σ-types will be interpreted as juxtapositions of shapes, Π-types will be interpreted as amalgamations of shapes, and Id-types will be (surprise surprise) be interpreted as shapes made out of paths.  

FOOTNOTES

*: There is an unfortunate terminological clash with \emph{Observational} Type Theory (OTT), a variant of MLTT. The terminological connection between my use of ``observation'' here and the use of the same word in OTT is just a coincidence

REFERENCES

[1] http://www.andrew.cmu.edu/user/ulrikb/80-518-818/MartinLof83.pdf <http://www.andrew.cmu.edu/user/ulrikb/80-518-818/MartinLof83.pdf>
[2] http://arxiv.org/abs/1211.2851 <http://arxiv.org/abs/1211.2851>
[3] https://www.math.ias.edu/~amortberg/papers/cubicaltt.pdf <https://www.math.ias.edu/~amortberg/papers/cubicaltt.pdf>
[4] http://arxiv.org/abs/1406.7413 <http://arxiv.org/abs/1406.7413>
[5] http://arxiv.org/abs/1402.5556 <http://arxiv.org/abs/1402.5556>
[6] http://link.springer.com/article/10.1007%2FBF00484985 <http://link.springer.com/article/10.1007/BF00484985>

> On Apr 12, 2016, at 01:57, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> Dimitris Tsementzis wrote:
> 
> "To be more precise, I can give you an account of the new foundations
> using seven basic notions: shape, point, symmetry, observation,
> juxtaposition, amalgamation, path. These are the notions I used to
> convince myself that I could justify the rules of HoTT without
> resorting to to set-theoretic topology. (Resorting to set-theoretic
> topology seems to me clearly the wrong way to go for an *intuitive*
> justification of the rules of HoTT. Rather, it is the way to go for a
> *formal* justification, i.e. for relative consistency results.) Anyway
> I am prepared to do that — and in any case, as I have mentioned to
> you, I believe such an account is possible, even if I have not found
> the clearest way to do it."
> 
> Now this is the first time I have seen anybody even indicate that they
> have any idea what I have in mind when I ask for a philosophically
> coherent presentation of seriously alternative foundations for
> mathematics.
> 
> I would be very interested to see an approach to general foundations
> for mathematics based on your
> 
> shape, point, symmetry, observation, juxtaposition, amalgamation, path.
> 
> So go ahead and start presenting this.
> 
> Harvey Friedman
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160414/23c776a5/attachment-0001.html>