Thank you for all these interesting remarks. I think I will spend some time on the logic of the second degree. So I note that there are two ways to formalize second-order logic: either by typing or by using separate quantifiers. And that the case of typing can be subdivided into two sub-cases: either by adding the type to the variable or by using different letters (as Metamath does). I find your code rather readable.
-- FL > -- 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 on the web visit https://groups.google.com/d/msgid/metamath/c85185b4-ca33-4df8-bf59-308ca052683f%40googlegroups.com.
