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.
On Fri, Aug 29, 2025 at 11:40 AM 'Bulhwi Cha' via Metamath < [email protected]> wrote: > 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. > > -- > 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 [email protected]. > To view this discussion visit > https://groups.google.com/d/msgid/metamath/DCET8ZOZO9IK.1TYQ30CWKBRWW%40semmalgil.com > . > -- 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 [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/CAFXXJSuBZDfLa_4iJG-BCn%3DT%3Dq6vpPcM%3DGLorMQJP3VKGPaMTA%40mail.gmail.com.
