I took a quick look at Jouko Väänänen's article in the Standford Encyclopedia, an article referenced by Mario in his Higher-Order Logic Explorer Home Page. I think it's a very good article because there were some things that were not clear to me until now that suddenly made sense. I would just like to make one comment. Mr. Väänänen says that in first-order logic it is impossible to talk about a collection of natural numbers. This seems suspicious to me because set.mm is full of propositions using a set of natural numbers. Suddenly I understood. The author doesn't have FOL + ZFC in mind, because in this case his remarks don't make sense; he thinks of FOL + Peano (the system of axioms for arithmetic designed by the Italian mathematician). In this case everything is perfectly clear since in such a system the individual variables can only denote isolated natural numbers.
I can also add that, in a way, the quantifier added to second order logic simply quantifies what, in set.mm, would be a propositional variable. In fact, this remark should only be seen as an analogy, because in second order logic propositional variables also exist. (If formalized in a "metamath" style.) It would be interesting to add a formalization of a second order logic with Peano's axioms and taking this paper as a basis. This would show concretely what all this means. -- 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/e63e5824-1b42-40d1-94a4-f6b7965d4ca5%40googlegroups.com.
