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.
signature.asc
Description: PGP signature
