[FOM] Friedman's challenge on HoTT-analogs of FOL=

[Mario Carneiro]

On Thu, Apr 7, 2016 at 3:20 AM, Harvey Friedman <hmflogic at gmail.com> wrote:

> I am skeptical that various people are really using the phrase
> "foundations for mathematics" or "general purpose foundations for
> mathematics" in the same way that I am using it.
>
> I don't think that there has been much (convincing) effort to
> abstractly define what we mean by a "general purpose foundation for
> mathematics".
>

As always in these discussions, the biggest problem is *defining your
terms*. Although you have stated a difference here, you don't actually
define what *you* mean by either "foundations for mathematics" or "general
purpose foundations for mathematics", so I won't guess.

What I can tell you is what I mean. The sense I used is a very literal one.
On a computer, if you are trying to write formal proofs, you need a tool to
encode your result, which will have some logic built in to it. Other things
may be built on top, or maybe this base logic is already powerful enough to
do what you need. That base logic is a foundation, and if you are proving
mathematical theorems, then it is a foundation for mathematics. The axioms
of the base logic are not subject to proof; if you are working in the
system then they are already being assumed. That's what makes them a
"foundation".

Notably, this does not presume that the base logic is simple, nor
"philosophically coherent". Metamath is notable for its incredible
simplicity, being even simpler to define than FOL. Conversely, it is not
particularly coherent with respect to its models; it is easiest to think of
as a pure deductive system, with no a priori semantic value assigned to the
expressible strings. Usually, it will be refined from this extreme
generality by axiomatic extensions, which will accord with some semantic
meaning that the axiom author recognizes. This is no different than the
addition of the axioms to FOL to get PA or ZFC, refining the semantics from
"a universe" to "the natural numbers" or "the universe of sets",
respectively; the common FOL part is the same, but the interpretation of
the expressions is different.


> Now the typical readers of the FOM know pretty well how I would, or
> they would, present a fairly brief philosophically coherent account of
> the standard f.o.m,, together with some absolutely remarkable
> reinforcing results of great clarity and obvious significance,
> etcetera. A very clear and convincing account that is readily
> digestible even by intellectually astute people of limited
> mathematical experience can be given even in one or two reasonable
> length FOM postings.


You know, there has been so much talk about this "absolutely clear and
convincing" stuff that I would be curious to see what that looks like.
Unlike you I have serious doubts that this is a common or easily accessible
phenomenon at all; it is extremely rare to see any account of anything that
has all the superlatives in this paragraph. If you think you can give such
an account of "standard f.o.m." (which seems to be your way of saying
"ZFC") then I would love to see it.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160407/20f50d2c/attachment-0001.html>