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

[Mario Carneiro]

On Fri, Apr 8, 2016 at 7:51 PM, Dimitris Tsementzis <dtsement at princeton.edu>
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.
>

No, it is not the "x is free/bound" predicate from FOL. For example, x is
disjoint from the string "( ph /\ A. y y = z )", provided that x is
disjoint from ph, y, and z; but it is not disjoint from "x = x" or "x = y"
or "A. x x = y". It is basically just a test of whether "x" is a substring
of the expression, but with disjointness also factoring down to any
variables (so that it remains valid under substitutions to the expression).
It is a strictly stronger statement than just "x is bound", since in the
example "A. x x = y", x is bound but not disjoint from the expression.
There is no recursive definition over the shape of the expression - in fact
it can be determined for any string of constants and variables at all. For
example, x is disjoint from "( ) + ph + y y" if x is disjoint from ph and
y, even though the expression itself is meaningless as a formula.

The only thing you need to know to implement a Metamath verifier is string
substitution (replace letter x with string S in string T) and the operation
"get the set of letters from alphabet V from a string on alphabet (C union
V)".

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160409/fc4fed12/attachment-0001.html>