[FOM] FOMUS/alternative foundations

[Harvey Friedman]

On Wed, Mar 23, 2016 at 5:43 PM, Jay Sulzberger <jays at panix.com> wrote:
>
> I think the obvious rejoinder amounts to a refusal to examine in
> detail certain proofs, and their situation in a chain of
> arguments.  A. Borovik has written about the difference between
> the two problems
>
> 1. Find a natural number x such that 7 + x = 10
>
> 2. Find a natural number x such that x + 7 = 10
>
> Borovik gave problem 1 to a beginner in arithmetic and the
> beginner was able to solve the problem by doing:
>
> 7 + 1 = 8
>
> 7 + 2 = 9
>
> 7 + 3 = 10 ; OK, solution!
>
> But problem 2 was more difficult: the puzzle is how to begin?

It is potentially very productive for the discussion to focus somewhat
on specific elementary examples that purportedly explain what these
alleged alternative foundational ideas are.

But I have a problem understanding just what this presentation is
about. What about this?

1 + 7 = 8

2 + 7 = 9

3 + 7 = 10 ; OK, solution!

So this doesn't appear to be a coherent description of any
foundational idea that I can recognize.

Perhaps what is missing in this presentation is the role of the
"principle", "axiom", "definition", or what?, that asserts

n + 0 = n
n + Sm = S(n+m)

If that is what is more or less going on, then yes, we have the very
short proof that

(there exists x)(7 + x) = 10

and the longer proof that

(there exists x)(x + 7) = 10

Bear in mind that I have replaced "find" with "there exists" here, and
I'm am not sure that this goes in the direction you want.

So at this point, we have the perfectly normal and somewhat
interesting question involving lengths of proofs. This fits squarely
into the usual foundational frameworks that we use, and can be dealt
with nicely in standard ways.

> I think the terms "intensional" and "extensional" are misleading
> here.  In the earlier "extensional" intuitionist type theory, the
> implicit analysis of what a proof of "x = y" could be is grossly
> wrong on its face.  For most x and y there exist different proofs
> of their equality, if indeed they are equal.

In the usual foundational framework, we simply do not consider
"proofs" as mathematical objects at all. They only become mathematical
objects when given some technical explicitly finite combinatorial
treatment. This is of course a huge advantage for the usual
foundational framework.

>Here is a possible
> source of confusion in many mathematical texts:
>
> Let A and B be mathematical structures.  Suppose in a proof we
> have the line:
>
>   A and B are isomorphic.
>
> Well there are two completely different meanings to this line:
>
> Meaning 1: We have a function f: Carrier(A) -> Carrier(B) which
> is an isomorphism.
>
> Meaning 2: We have a proof that there is some such f.

There is exactly one meaning in the usual foundational framework. This
is essentially Meaning 1. It is a set theoretic statement.
>
> In classes in elmentary logic we can see a near related distinction:
>
> Let us consider a class of structures Class1, which we define as
> follows: A structure c1 is in Class1 in case there is a
> substructure cs1 lying in c1 such that < relation obtains
> between cs1 and c1 >.
>
> Here is another class Class2, which we define as follows:
> the pair (c1, cs1) lies in Class2 iff we have < relation obtains
> between cs1 and c1 >.

The mathematical grammar here is sufficiently poor that I find the
above unreadable, and cannot easily perceive what the point is. I
think I may be able to see the point if this were more clearing
written.
>
> Yes, these are trivial facts.

In the first case, the numerical one, I have no idea what the "trivial
fact" is. I did my best to make some sense of it.

In the second case, I don't have any idea yet what the "trivial fact" is.

> But they are important facts, and
> they are the sort of facts which come up in the study of
> "foundations for mathematics" and also in the design of proof
> assistants.

So already I have no idea what is being said here.

> Any proof assistant to be
> sound must respect these distinctions, else they give sanction to
> crude logical errors.  The claim of the New Crazy Type Theory
> folk is that they attempt to be more honest in their dealings
> with these distinctions by aiming at a formalization of them.

So for me we need to get much clearer about what exactly these
"distinctions" are before the discussion can become productive.
>
> Gian-Carlo Rota invented the word "cryptomorphic".  He pointed
> out that the "matroids" may be defined in many different ways.
> Different at the level of logic: A rank function is simply not a
> collection of sets.  Indeed it would be a (type error | category
> mistake) to think they were the same.

Well, an ordered pair is "simply not {{a},{a,b}}". But this is not an
important use of the word "is" for the usual foundational framework.
So normally one simply defines <a,b> = {{a},{a,b}}, and everything
works just fine.

> Here is a slogan for
> propagandists for HoTT^WUnivalent Foundations:
>
>   Univalent Foundations is the General Theory of Cryptomorphisms.

I certainly do not understand at this point what the "General Theory
of Cryptomorphisms" is. I might be interested in it if I knew what it
was. And I am also interested in knowing what is to be gained by this,
and why it is an alternative foundational framework, and also whether
it is philosophically coherent.
>
> Let us apply this slogan to the problem "Are there different
> proofs of 'x = y'?".  The answer is clearly "yes".

This paragraph doesn't mean anything to me. I have no idea what kinds
of things x,y are or refer to, or whatever. In the usual foundational
framework, the above paragraph is totally meaningless.

> If x is given
> by a rank function, and y is given by the collection of
> independent sets, then the proof that 'x = y' will be logically
> different from the proof in the case that x, as before, is given
> by its rank function, and y by its coordinatizing matrix.

The use of the word "given" here needs to be clarified. Also the
background combinatorics here (ranks, independent sets, coordinating
matrix) should be defined in order to facilitate the discussion,
because you cannot expect the general reader interested in such issues
to recall these notions. After this has been clarified, probably we
can see how well or how badly the usual foundational framework handles
this situation

> Certainly our
> examples here are trivial and immediately understood by students
> of logic.

Not by this ignorant student of logic (me).

> But the program of HoTT is to take these striking
> trivialties and study them carefully, and that is different from
> shrugging them off as "mere trivialities".  After all it was not
> so long ago that many mathematicians thought that the study of
> sets was the study of useless trivialties and/or
> self-contradictions.

This is a very nice paragraph, but we need to go over these
trivialities with some serious care, seeing just how the usual
foundational framework deals with them.

Harvey Friedman