[FOM] A Meaning Explanation for HoTT?

[Harvey Friedman]

Dimitris started his attempted philosophically coherent presentation
of HoTT with http://www.cs.nyu.edu/pipermail/fom/2016-April/019726.html

On Thu, Apr 14, 2016 at 6:16 PM, Dimitris Tsementzis
<dtsement at princeton.edu> wrote:

FRIEDMAN:

> 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.
>
DIMITRIS:

> 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. ...
>
> 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... 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. ... What,
> if any, is the *intuitive* justification of the validity of the rules of
> (any) HoTT? ...
...
> 5) I do not see this as a “challenge” or as a “war”. I see it as a healthy
> and lively conversation. ... I disagree with Friedman that “I can do
> better what you can do” is the right attitude to take here. ...  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”.

> 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.

Before you even begin, this is going to be a rather tall order to get
a general purpose foundation for mathematics. Mathematicians are
always very clearly using "not, and, or, if then, iff, there exists,
for all" and making abbreviations that amount to a growing
hierarchically organized list of atomic formulas. One thing that they
are also doing is of course forming and using compound terms and
equality.

So when a working mathematician uses say if then, then this is going
to have to reflected somehow in a rule. But what if they hypothesize
something that has an if then embedded in it? Then probably you are
going to have to take this as hypothesizing some sort of equational or
quantifier free statement. Or maybe the whole idea of what I call
HAVE/WANT calculus is radically altered. Maybe the whole idea of
hypothesization is thrown out the window. This is a very tall order,
because you are endeavoring to present this as clear transparent
general purpose foundations for mathematics. I am all ears.
>
> So with this in mind, here is the basic idea:
>
> BASIC IDEA: The rules of HoTT are instructions for constructing new shapes
> from old.

Actually this suggests the program which I think Tarski tried, and his
students also developed some, which is quantifier free set theory. The
idea here is that in set theory you have fundamental operations that
take sets to sets. Most notably, union, power set, unordered pair,
separation. But the really interesting idea is to NOT just separation,
but rather replace it by some little operations. This should be done
for WZ, and for NBG, which are finitely axiomatized. There are things
of this kind around. But I think that they can be seriously simplified
and streamlined in interesting ways. I needed to fool around with such
things when I did my work on Impossible Counting, but only for
technical reasons there.

This whole matter of quantifier free set theory or equational set
theory should probably be revisited with various modern tools. There
was an FOM posting with some references to work perhaps in this
direction, and there has been so much FOM traffic of late that it
might be more convenient for the person who made that post to post a
reply to this thread under "A Meaning Explanation for HoTT?" - even
better with some short account of some basic features of it.

> 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.

In presenting set theory, I always start with a discussion of trivial
special cases. I talk about these four aggregates:

nothing
just emptyset
just emptyset, {emptyset}
just emptyset, {emptyset}, {{emptyset}}, {emptyset, {emptyset}}.
just those obvious 16 obvious sets.

Then I like to say that "there is nothing going on in set theory that
isn't pretty much implicit in the above".

NOTE: I am working on a theory that supports a principled move from
the above four level setup to the whole of ZFC. I would love
eventually to have a principled way of going from just

nothing
just emptyset
just emptyset, {emptyset}
just emptyset, {emptyset}, {{emptyset}}, {emptyset, {emptyset}}.
just those obvious 16 obvious sets.
just those obvious 2^16 sets.

to all or a lot of our large cardinal extensions of ZFC. There really
should be more than enough complexity in just the above to properly
represent what is going on in ZFC and large cardinals.

What we need from Dimitris is a similarly simple account of the baby
stuff that tells the tale, just like the above baby stuff tells the
tale of set theory.
>
> B. JUDGMENTS AS OBSERVATIONS
>
Dimitris starts with

> (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.

We now need to see 1-4 in action with some baby examples. Perhaps a bit like

nothing
just emptyset
just emptyset, {emptyset}
just emptyset, {emptyset}, {{emptyset}}, {emptyset, {emptyset}}.
just those obvious 16 obvious sets.

By way of example of something that I DO THINK has a fundamental
intuition of the kind that we are looking for is this. Aristotle's
conception of the continuum.

I am not an historian, nor do I have the slightest ambition to become
one. So I am only interested in useful idealized history for making
new advances.

Aristotle's idea is supposed to be that the continuum is not made of
points, but has parts. For the modern treatment, these parts are
intervals, where the endpoint situation can be handled in various
ways, either by an equivalence relation or by fiat that there are no
endpoints, or whatever you like it. But for Aristotle, the notion of
endpoint makes no sense in the first place, as there are no points.

You can do some very nice things with this setup, including beautiful
axiomatizations and decision procedures and consistency proofs. This
is all low level logically. All interpretable in EFA.

But it is arguably a genuinely geometric foundation which a status
that is totally independent of set theoretic foundations.

CHALLENGE. Do something this compelling, or approaching this level of
being compelling, that interprets ZFC, or even ZFC + large cardinals.
Even significant fragments of ZFC or even PA would be serious
foundational progress.

Now I am working on something very much along these lines based on the
pointless conception of the continuum, that gets us at least to Z_2 =
second order arithmetic ~ ZFC without power set. In terms of
interpretation power, this is far more than the vast bulk of
mathematics. So one can make an argument that this approach is moving
to some sort of general purpose foundation for a huge bulk of
mathematics. However, interpretation power is not all that we want.

CHALENGE. Take what i do along these lines, that interprets Z2, and
augment it, keeping its fundamental geometric intuition, in such a way
that the interpretation of the vast bulk of mathematics is readily
intuitive just like the interpretation of the vast bulk of mathematics
is ready intuitively interpretable in ZFC without power set.

Actually, something that probably has not been explored as well as it
should. Look at sugared ZFC without power set ---- better, sugared
(ZFC without power set), designed to form a general purpose foundation
for the vast bulk of mathematics Of course there is an immediate
problem. The real line does not provably exist in ZFC without power
set. But it does provably exist in sugared (ZFC without power set).
This needs to be fleshed out properly with modern tools.

Harvey