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

[Dimitris Tsementzis]

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

But isn’t the disjoint variable condition a condition expressed in (informal) FOL=? A fragment of FOL=, perhaps, but still first-order in the usual sense. 

I would certainly like to understand more in what sense you think Metamath provides a non-FOL= way of manipulating symbols. Perhaps also to see if we mean it in the same sense.

Dimitris


> On Apr 6, 2016, at 02:18, Mario Carneiro <di.gama at gmail.com> wrote:
> 
> 
> 
> On Tue, Apr 5, 2016 at 1:58 PM, Dimitris Tsementzis <dtsement at princeton.edu <mailto: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
> _______________________________________________
> 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/20160408/1fe5fa2a/attachment-0001.html>