[FOM] foundations meeting/FOMUS/discussion

[Lawrence Paulson]

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


> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom