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

[Mario Carneiro]

On Fri, Apr 15, 2016 at 12:34 PM, Dimitris Tsementzis <
dtsement at princeton.edu> wrote:

> Dear Mario,
>
> Well, certainly this is the case, just the same as it is true that HoTT
> and ZFC and any other foundation can be presented, *at the meta level*, in
> terms of a FOL foundation.
>
>
> Yes exactly. But what I called “Friedman’s challenge” in this thread was
> exactly to see whether HoTT/UF can provide a way to present deductive
> systems, at the meta level, in terms of some alternative “logic” whatever
> that could mean. It’s a very strong challenge, and an unfair one of course
> and perhaps even unintelligible at this point. But unfair and very strong
> and perhaps not-yet-fully-intelligible challenges are exactly what might
> produce interesting discussion and thinking.
>

Well, since all these systems are inter-interpretable, each one is powerful
enough to model the others (or more accurately, each is strong enough to
model deductions in the others, which only needs the strength of PA). It is
certainly easy to formalize Metamath's string operations in ZFC, and
conversely of course there is an extensive ZFC database in Metamath.

 But I distinguish this from the idea that the system itself is based on
> FOL, because derivations in it need not have an analogue in FOL.
>
>
> Fair enough, yes. But is there something “fundamental to deductive
> thought” on which it is based, and which is completely distinct from FOL?
> You’ve already explained what it is — and perhaps I’ll convince myself too
> if I read more. But it’s not clear to me yet. I see some operations, and
> that’s it.
>

Well, is deduction itself “fundamental to deductive thought”? There are
formulas (of some kind) going in, then a horizontal line, then formulas
come out. All deductive systems, including of course ZFC and HoTT, fit this
mold. Metamath is designed to be general enough so that the target formal
system can be plugged in without swapping out the machinery.

INTERESTING THAT YOU SHOULD MENTION THIS, as it happens (shameless plug) I
> recently wrote a paper http://arxiv.org/abs/1601.07699 addressing this
> exact issue.
>
>
> OK, that seems to be a natural and interesting question to address, so I
> will read your paper before saying anything else. I am speaking vaguely
> here, because I am ignorant. But it seems to me, from your description,
> that a model for Metamath is something like a generalized deductive system.
> Which makes sense, of course, given the purpose of the system. But it does
> not have a kind of “ontology” associated with it, as e.g. does HoTT. You
> seem to be a finitist, so that’s alright with you, but I can’t see any
> alternative “logic” emerging without at least an alternative conception of
> the basic objects of mathematics.
>

This is a good way to put it. Metamath well handles the practical concern
of the mathematician, in describing deductive systems in a very general
way. It does not come with any ontological content, and this "models" work
is quite recent - before this we didn't really have any clear conception of
what it might look like. So as far as Friedman's "gauntlet" is concerned,
it is not really a contender, and all of its "meaning explanation" is
derived through modeling in basically ZFC.

The "Models" paper is a bit of an oddity in working with completely general
Metamath formal sytems - usually we concern ourselves with an extension of
a particular foundation, meaning that we already have axioms for the basic
notions, and we are modifying it with maybe extra axioms. For example, the
primary Metamath database, called set.mm, contains axioms describing the
FOL primitives, equality and elementhood, then goes on to add the ZFC
axioms one at a time. It is simple to consider subsystems of this dropping
this axiom or that (because axiom use is tracked on a per-theorem basis),
but generally one keeps at least FOL, so that the usual mental model with a
single universe with certain relations on it is sufficient to understand
what is being said. (IMHO, the set.mm formalization does not differ
appreciably from Friedman's favorite foundation, "sugared ZFC".)

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160416/5e33765e/attachment.html>