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

[Hendrik Boom]

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