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 -- 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/DCEQWFT6KC8A.C73OV4OKIH69%40semmalgil.com.
signature.asc
Description: PGP signature
