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

[Dimitris Tsementzis]

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. 

>  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.

> INTERESTING THAT YOU SHOULD MENTION THIS, as it happens (shameless plug) I recently wrote a paper http://arxiv.org/abs/1601.07699 <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.

Best,

Dimtiris


> On Apr 12, 2016, at 21:57, Mario Carneiro <di.gama at gmail.com> wrote:
> 
> 
> 
> On Mon, Apr 11, 2016 at 11:16 PM, Dimitris Tsementzis <dtsement at princeton.edu <mailto: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 <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 <http://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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160415/3ad981d6/attachment-0001.html>