While it is not explicitly based on Väänänen's article, I should note that the Peano arithmetic formulation that I'm working on in peano.mm1 ( https://github.com/digama0/mm0/blob/master/examples/peano.mm1#L974-L977) is quite similar to this. It axiomatizes PA in much the same way as set.mm axiomatizes ZFC. There are "class variables" (called "set" denoting possibly infinite sets of natural numbers), as well as a sort "nat" for individual variables, and there is only quantification over nat, resulting in a "slightly second order" conservative extension of PA.
On Wed, Mar 11, 2020 at 11:57 AM 'fl' via Metamath < [email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/e63e5824-1b42-40d1-94a4-f6b7965d4ca5%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSs%2BW5TTpeHVuAVWU5YZ3y1ixStv3xGAEUvVfDZ7bK_bkw%40mail.gmail.com.
