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

[Mario Carneiro]

On Mon, Apr 11, 2016 at 11:16 PM, Dimitris Tsementzis <
dtsement at princeton.edu> wrote:

> Dear Hendrik and Mario,
>
> I don’t want to abuse your patience here because we might still be talking
> at cross purposes and I also have zero familiarity with Metamath. But
> looking at Appendix C in the Metamath book, it seems to me that the
> Metamath system can be described as a first-order theory; indeed, as
> expected, a quite simple one. So that, for me, still makes it a first-order
> way of manipulating strings of symbols.
>

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. (In fact, Appendix C assumes ZFC, or at least a
little naive set theory, for its presentation.) 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. (One of the classic examples of an
"exotic" Metamath formal system is Hofstadter's MIU system, which is quite
obviously not FOL by any stretch.) Like I said, in order to write a
*Metamath verifier*, that takes a proof and reports if it is correct, one
need not build in any FOL primitives like proper substitution, although to
verify the correctness of the verifier you would need some reasonably
powerful meta-theory (PA is probably sufficient) in order to formalize
Appendix C.


> So perhaps to get some further clarity: what do you understand to be a
> “model” of Metamath? (Also, what do you understand it to be a model *of*?)
>

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. The short answer is that it is not simple; since Metamath is
so general, the models of it can be exceedingly complex until you add some
axioms to tame the models a bit. In the most general case you have a
universe for each sort, so for example with set.mm (the ZFC formalization)
there are four sorts, "set" (set variables), "class" (classes, subsets of
the universe with finitely many parameters), "wff" (predicates with
finitely many parameters), and "|-" (provable wffs, i.e. the constant true
function). Then there is an interpretation function that maps each string
and each valuation to a member of the right universe, or is undefined if
the string is not well-formed. Finally, there is a freshness relation that
says whether two elements of the universe are valid for a disjoint variable
condition (for example a wff might be fresh for a set variable if it is
constant with respect to that variable), and these all have to satisfy
various composition identities.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160412/58db2948/attachment.html>