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

[Mario Carneiro]

On Tue, Apr 5, 2016 at 1:58 PM, Dimitris Tsementzis <dtsement at princeton.edu>
wrote:
>
> 3. Another, equivalent, way to put the CHALLENGE is this: it seems the
> only way we have of formalizing the syntax and deductive systems of HoTTs
> themselves is as first-order theories, namely as strings of symbols defined
> and manipulated using first-order axioms. Which leads to the question: Can
> there be a non-FOL=-based method for manipulating strings of symbols?
>

It's a little beside the point for the main thrust of this post, but this
sentence struck me, because this is exactly what Metamath is: a
non-FOL=-based method for manipulating strings of symbols.

To summarize, in Metamath there are expressions, which are strings of
constants and variables, and the only primitive is the direct substitution
of an expression for the variables in another expression, subject to
disjoint variable conditions (which say that the substitution may not
contain an "x" in the string anywhere). That's it. There are no bound
variables or proper substitution, so it is much closer to a string
rewriting system than FOL. Nevertheless, one can add axioms within this
system defining the meaning of implies, not, forall and out pops FOL. Or
you can add axioms for definitional equality and type judgement,
applications and pi types and lambdas, and the inductive types and
univalence, and out pops HoTT.

While I don't know whether it would be wise to point the full brunt of
cross-examination from FOM at Metamath, it is clear to me that in a
practical sense Metamath is a candidate for foundations of mathematics,
that is not FOL-based. (I don't know much about Isabelle/Pure, but I think
it could also stand in here.)

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160406/37b0e110/attachment-0001.html>