Are first order variables in Metamath Zero variables of the object logic?

[Bulhwi Cha]

A computer science graduate student asked the following question:
> Are first order variables in Metamath Zero variables of the object
> logic, or are they variables in the metalogic, that is, Metamath Zero?

I think they're variables in MM0, but usually there will be exactly one
FOL variable corresponding to each first order variable in the MM0
theorem.

On page 19 (Section 1.2.1 Bundling) of the Metamath Zero paper[0]:
> Usually all or almost all first order variables will be distinct from
> each other, in which case there is exactly one corresponding FOL
> theorem (up to alpha renaming).

[0] https://digama0.github.io/mm0/thesis.pdf

[Bulhwi Cha]

On Fri Aug 29, 2025 at 4:49 PM KST, 'Bulhwi Cha' via Metamath wrote:
> I think they're variables in MM0, but usually there will be exactly
> one FOL variable corresponding to each first order variable in the MM0
> theorem.

I forgot to end the above sentence with the phrase "up to alpha
renaming."

The CS graduate student had said:
> One should be able to instantiate variables in the metalogic by
> variables in the object logic. However, expressions can't be
> substituted directly for first order variables, so it's impossible to
> instantiate these variables by variables in the object logic.
>
> It appears that first order variables in Metamath Zero are variables
> in the object logic, not in the metalogic.

[Mario Carneiro]

Yes, MM0 first-order variables can be one-to-one translated to variables in the object logic. They are literally variables in the metalogic, given that MM0 is the metalogic and we are talking about (first-order) variables in MM0, but the property of first-order variables is that they are interpreted as first-order variables of the object logic. Second-order variables are also variables of the MM0 metalogic, but they correspond to either second order variables in SOL or HOL, or alternatively to scheme variables ranging over expressions of the target sort in a FOL scheme.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/DCET8ZOZO9IK.1TYQ30CWKBRWW%40semmalgil.com.