[FOM] foundations meeting/FOMUS/discussion

[Jay Sulzberger]

On Wed, 23 Mar 2016, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

> I am very familiar with Martin Löf's intuitionistic type theory
> as it was in 1982, and his explanation of the rules makes
> perfect sense from the point of view of Heyting’s explanation
> of intuitionism. His system can be regarded as a straight
> formalisation of Heyting’s philosophy, and I believe it is also
> backed by some proof-theoretic results. I don’t know how easily
> it could be interpreted in ZF, because you can write things
> such as \lambda x. x (the unrestricted identity function),
> which is a proper class rather than a set. I am much less
> familiar with the type theory or theories underlying Coq and
> with the question of set-theoretic models there.
> 
> Heyting’s explanation of the logical connectives involves a
> certain idea of evidence, where for example evidence for a
> conjunction is an ordered pair, evidence for a disjunction is
> an element of a disjoint sum and evidence for an implication is
> a (computable) function. This may not have much to do with
> traditional mathematical practice, but it has strong
> connections to computer science, and this explains the
> considerable interest in constructive mathematics on the part
> of theoretical computer scientists. My impression is that
> mainstream mathematicians are much less interested in
> intuitionism.

>

> In Martin Löf's 1982 type theory, evidence for a proof of
> equality was effectively vacuous. This made equality
> extensional. I remember reading Martin Löf's justification of
> this apparently controversial decision. In a nutshell, the
> point was that once we know that a=b we no longer need to know
> the reason. From my point of view, one advantage of this choice
> was that it kept the “evidence” relatively small even when it
> was based on a long and complicated proof. I did a lot of work
> connected with this type theory in the early 1980s. But
> sometime in 1984 or 1985, an intensional of equality was
> announced and the previous system was dismissed as
> flawed. Interest in the earlier system vanished not because of
> some paradox but because one man changed his mind, and all of
> my own work was rendered useless because it relied on
> extensional equality. That marked the end of my interest in
> constructive type theory.
> 
> The Coq type theory is somewhat different but also has
> intensional equality. That means for examples that n+0 = n and
> 0+n = n (where n is a natural number) are quite different
> statements, one holding by definition and the other proved by
> induction. One of the claimed advantages of HTT is that it
> simplifies the treatment of equality. There is an obvious
> rejoinder to this.
> 
> Larry Paulson

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?

Now certainly the beginner is not mistaken in their logic.
Problem 1 and Problem 2 are quite different in their logical
structure.  Of course, if the problem solver has to hand the tool
(allow me for now the imprecision of language here) "the
operation + is commutative" then the solver may use the tool to
see that any solution to 1 is also a solution to 2 and vice
versa.

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

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

Now indeed if we apply the forgetful functor First to any element
(c1, cs1) of Class2 we get an element c1 of Class1.  A partial
converse holds: Let c1 be any element of Class1.  Then we may
choose (if we can perhaps, here "constructivity" comes in) a cs1
and form the pair (c1, cs1) which is an element of Class2.

Now what is one difference between Class1 and Class2?  Well the
leap-to-the-eye categories, call them Cat1 and Cat2 are
completely different, in many cases.  This is, in part, how in
the development of type theory, and in particular HoTT,
categories come in.

Yes, these are trivial facts.  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.  These logical^Wfactual distinctions come up in the
design of proof assistants for all the popular candidates known
to me for the title "Foundations of Mathematics".  They come up
in the design of proof assistants for systems based on ZFC and
for all the new "type theoretic".  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.

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.  Here is a slogan for
propagandists for HoTT^WUnivalent Foundations:

   Univalent Foundations is the General Theory of Cryptomorphisms.

Let us apply this slogan to the problem "Are there different
proofs of 'x = y'?".  The answer is clearly "yes".  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.  Rota
liked to repeat Hegel's apercu "Everything was off handedly
remarked on by somebody who did not discover it.".  Certainly our
examples here are trivial and immediately understood by students
of logic.  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.

oo--JS.


> 
> 
> > On 23 Mar 2016, at 02:38, Harvey Friedman <hmflogic at gmail.com> wrote:
> > 
> > On Sat, Mar 19, 2016 at 12:18 PM, Louis Garde <louis.garde at free.fr> wrote:
> >> Le 18/03/2016 04:40, Harvey Friedman a écrit :
> >>> 
> >>> Among the obvious merits of ZFC as a foundation for mathematics, there
> >>> is one that I often see not sufficiently emphasized. That is, its
> >>> PHILOSOPHICAL COHERENCE.
> >>> 
> >>> ../..
> >>> 
> >>> But my impression is that the more radical proposals, particularly
> >>> HOTT, philosophical coherence is proudly thrown away.
> > 
> > That is my understanding, which may or may not be correct. (However,
> > see below for a pointer to an internet manuscript ).This certainly
> > prima facie precludes HOTT as any kind of reasonable "foundation for
> > mathematics" in any standard sense.
> > 
> > However, there does remain the possibility that HOTT could have some
> > impact on the subject: foundations of mathematics. For instance, there
> > may be interesting metatheorems to the effect that if you take a HOTT
> > point of view in a certain kind of mathematical context, regardless of
> > its philosophical coherence, then you can always replace it with a
> > standard point of view - i.e., you still get a theorem of ZFC or
> > variant. I am under the impression that just this sort of thing is
> > being done.
> > 
> > Also it may well be the case that if you take a HOTT point of view in
> > a certain of mathematical context, then proof structure gets
> > simplified, and/or it gets easier to formally verify certain kind of
> > results.
> > 
> > Such developments promise to be relevant  to f.o.m. However, that it
> > not to say that it rises to the level of a new foundation for
> > mathematics. For that, the standards are rather high - and
> > philosophical coherence is absolutely essential.
> > 
> >> Could you clarify what you mean by "philosophical coherence"?
> >> Don't you think that constructiveness brings a very strong "philosophical
> >> coherence" ?
> > 
> > Philosophical coherence is a notion that has been in implicit use
> > since at least the great Greek philosophers. I am not really the best
> > one to try to clarify this notion. I think that the leading
> > philosophers can do a much better job of this.
> > 
> > Yes, constructiveness does have a sufficiently strong philosophical
> > coherence to offer an alternative foundation for mathematics that is
> > worthy of consideration. At the moment, it is doubtful if it is as
> > philosophically coherent as traditional non constructiveness, but it
> > is sufficiently philosophically coherence to be taken seriously as an
> > alternative foundation for mathematics.
> > 
> > However, the most readily digestible versions of constructive
> > foundations are trivially restrictions on classical foundations, and
> > so their value as an alternative is in terms of placing additional
> > demands.
> > 
> > But there are other versions of constructive foundations which cannot
> > be readily construed as obvious restrictions on classical foundations.
> > Here the philosophical coherence generally becomes much less clear.
> >> 
> >> With my own understanding, the philosophical coherence of Martin Löf's
> >> intuitionistic type theory is at least as strong as ZFC's one.
> > 
> > It would be valuable for the FOM readers to give a brief simple
> > account of Martin Lof's intuitionistic type theory, here on the FOM.
> > 
> > E.g., what do you think of the account in
> > http://www.math.unipd.it/~silvio/papers/TypeTheory/InnIntro.pdf ?
> > 
> > There is nothing there that on a casual reading, has anything like the
> > philosophical coherence of the usual fragments of ZFC. Furthermore, on
> > a casual reading, there is one notion after another that is foreign to
> > the way working mathematicians think. This is already not a good sign.
> > On a casual reading, this appears to be incomparably more complicated
> > than the usual fragments of ZFC. Another not so good sign. Again, we
> > are talking about prima facie casual readings.
> > 
> > Philosophical coherence and complexity here can be nicely judged by
> > comparing descriptions and discussions side by side. In the case of
> > ZFC and its usual fragments, the philosophical coherence, complexity,
> > and descriptions are exceedingly well known and accepted, and so I am
> > not sure if there is any point in me displaying such things here on
> > the FOM. However, there does seem to be a point in trying to provide a
> > comparative treatment here on the FOM for the ITT side. Even before
> > one gets to the main event of HOTT.
> > 
> > I found the following on the Internet:
> > http://www.bristol.ac.uk/media-library/sites/arts/research/homotopy-type/documents/identity-in-hott-part-one.pdf
> > Unfortunately, I do not see any indication of who the authors are of
> > this internet manuscript, which is a bit strange and frustrating.
> > There they do claim that HOTT can be cast in a way that provides an
> > alternative foundation for mathematics. They appear to be quite
> > sensitive to the correct view that in order for HOTT to rise to the
> > level of a legitimate alternative foundation, it has to be cast in a
> > way that does not depend on specialized esoteric mathematics.
> > 
> > A quick read of this does not reveal any kind of clearly stated
> > philosophically coherent foundational proposal. It would of course be
> > very interesting to FOM readers to see such a proposal stated in
> > simple clear terms.
> > 
> >> And, to put it very briefly, HoTT is a natural extension of it: its
> >> definition of identity types makes it applicable to homotopy theory, but you
> >> do not need homotopy concepts to justify the rules defining identity types.
> >> 
> > Mathematicians use one single robust notion of equality which is so
> > ingrained in their thinking that it does not require any conscious
> > thought. Identity sometimes becomes an issue, and that is normally
> > handled through equivalence relations and taking equivalence classes,
> > as taught in undergraduate math.
> > 
> > Having nuanced notions of equality of a nature that is generally
> > foreign to what is normally taught and used is prima facie rather
> > dubious, and the burden of proof is on the proposer if they wish to
> > maintain philosophical coherence. This is by no means impossible. It
> > just means that a high bar has to be met, with carefully constructed
> > and rather easily grasped accounts. One should be particularly
> > suspicious of rule based concepts.
> > 
> > Now ultimately, I doubt if anybody is going to convince the
> > mathematical or philosophical communities that alternatives like HOTT
> > are philosophically coherent unless they in some ways rely on an
> > interpretation of it into fragments of ZFC (or maybe standard
> > extensions of ZFC). Of course, once one does have such an
> > interpretation, there is the question of what has been gained by the
> > whole enterprise.
> > 
> > For instance, there is the extremely crucial perennial question of
> > whether the current foundations for mathematics is sufficient to
> > establish mathematically important results of a computational nature.
> > I mention computational here because those kinds of statements do not
> > have rival formulations. I.e., you have the same computational
> > statements independently of whether you are doing ZFC, ITT, HOTT, or
> > S:EOIAFHEIOEWAUOFN. Now if you develop mutually interpretations of the
> > usual kind that one expects and has done, then one gets as an
> > immediate Corollary, that computational statements are going to be
> > provable under one philosophically coherent foundational framework if
> > and only if it is provable under any other rival philosophically
> > coherent foundational framework.
> > 
> > So one thing that is NOT going to be gained by replacing the usual set
> > theoretic foundations with HOTT or SEOFINIOENFOWENFOIEN is any kind of
> > difference with regard to the derivability of mathematical results of
> > a computational nature (derivability in the usual sense).
> > 
> > So the argument for the value of having an alternative foundational
> > framework is likely going to have to rest on more focused practical
> > issues, rather than the classic foundational issues everybody is
> > familiar with.
> > 
> > One is of course that it is supposed to facilitate or even make
> > possible the creation of formal proofs. My impression is that, SO FAR,
> > the evidence for this is confined to a few examples from specialized
> > esoteric contexts, together with the "claim" that formal proofs cannot
> > be done with the usual set theoretic foundations in the pragmatic
> > sense. But how is such a "claim" justified? Merely saying that one has
> > failed to be able to come up with formal proofs under the usual
> > foundational framework is not remotely convincing. What is needed here
> > is an ATTRACTIVE challenge problem: can you get a formal proof of such
> > and such simple basic attractive theorem using the usual foundational
> > framework? One should be able to have some rather basic and intriguing
> > ATTRACtIVE challenge problems IF the aim is to go beyond specialized
> > esoteric mathematical contexts.
> > 
> > What other benefits are adherents envisioning for such alternative
> > foundational frameworks? (See the second and third paragraphs of this
> > posting).
> > 
> > Harvey Friedman