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

[Dimitris Tsementzis]

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.

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

Dimitris

PS: What I meant by “informal FOL” was simply what is done in Appendix C, but without being explicit about the details of the axiomatization. 

> On Apr 9, 2016, at 10:56, Hendrik Boom <hendrik at topoi.pooq.com> wrote:
> 
> On Fri, Apr 08, 2016 at 07:51:16PM -0400, Dimitris Tsementzis wrote:
>>> 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.
> 
> I don't know how much scope the qualifier (informal) is meant to have 
> in modfying "FOL", but the disjoint variable restriction seems to be 
> expressed in English.
> 
> Specifically, there would seem to be "$d  statements" specified in one 
> paragraph of section 4.1.3 of http://us.metamath.org/downloads/metamath.pdf,
> as well as an algorithm specified in a subsection of 4.1.4.
> 
> I would find it difficult to express this merely in first-order logic.
> 
> And I would suspect that the real formalism used to express the 
> constraint isn't English, which is not very formal, but the code of one 
> of several computer programs.
> 
> Ultimately, whatever is used to express proofs and ideas, it must be 
> understood in some sense.  But it looks as if that can be done to 
> various degrees by a human being or a conputer.
> 
> I'd like to see some discussion on what could constitute "understanding" 
> in this context.
> 
> Everything ranging from direct perception of a platonic realm of sets to 
> Brouwer's mental constructions seem to be means of avoiding this topic.
> 
> -- hendrik
> 
> _______________________________________________
> 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/20160411/e325cea6/attachment.html>