On 11/29/21 8:15 PM, Norman Megill wrote:
I'm not saying you are wrong, only that I don't understand the reasoning or advantage and need to be educated. :) I know that many books show ZFC axioms and even FOL axiomatizations with universal closures, and I've never understood why.
I don't really know whether avoiding the free variables is just convention/tradition or whether it really is easier to learn this way. But it is pretty common in how people teach logic. For example: "a statement is a formula with no free variables (Margaris, p. 21) and "a formal proof is a finite sequence of statements" (p. 13) (these quotes are a bit out of context, in the sense that later chapters of Margaris, which aim to be more rigorous, are stated differently). Certainly when I was learning predicate logic I found ax-gen to be very confusing (perhaps because it really is hard to get your head around the idea that something can have a truth value when it contains free variables, or perhaps because of this educational tradition which will say a formula cannot have a truth value when it contains free variables).
Now, some sources may not be worrying about pedagogy but may be thinking of measuring quantifier alternations or other topics I understand dimly if it all. So there may be reasons for the universal quantifiers in some contexts that I'm not really aware of. But in the context of set.mm/iset.mm (which is where I spend my time these days), I have certainly gotten used to the statement meaning the same thing with or without the quantifier. It looks like in http://us.metamath.org/ileuni/onintexmid.html we picked the style without the quantifier but in others like http://us.metamath.org/ileuni/ordtriexmid.html (admittedly, a restricted quantifier here) or http://us.metamath.org/ileuni/ssfiexmid.html (here an unrestricted quantifier) we picked the style with the quantifier. Would http://us.metamath.org/ileuni/acexmid.html be easier to read if there was an "A. x" at the start, which would prevent the eye from having to hunt for the free variable in a fairly long formula? I sort of gave up on having a strong opinion one way or the other a while ago.
-- 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/78bc02be-d1c6-4cdb-dd44-d12b24382ece%40panix.com.
