I’m concerned that you’re pushing second order logic too hard, using a false fork—such and so cannot be done in first order logic therefore second-order logic. “Second order” logic is a particular thing—for example it is a logic based on model theory. http://en.wikipedia.org/wiki/Second-order_logic#History_and_disputed_value
There are lots of alternative directions to go when you go beyond the general consensus of first-order logic. Freek Wiedijk’s paper “Is ZF a hack?” is a great tour of alternative foundations of mathematics—first order logic and the Zermelo-Frankel axioms for set theory turns out to be the smallest by many measures, but the others are generally higher order in one way or another. http://www.cs.ru.nl/~freek/zfc-etc/zfc-etc.pdf
“First order logic can’t talk about finiteness vs. infiniteness.” is sortof true in that first-order logic in a fixed language is necessarily local—it can step from object to object (along relation links) but the number of steps bounded by the size of the first-order formula. However, a standard move is to change the language, introducing a new sort of object “sets” and some axioms regarding relations between the old objects and the new objects such as inclusion, and then you can talk about properties of these new objects such as finiteness and infiniteness. Admittedly this standard move is informal or metatheoretic; we’re saying “this theory is the same as that theory except for these new objects and axioms”.
This is what the Zermelo-Frankel axioms do, and the vast majority of mathematics can be done within ZF or ZFC. Almost any time you encounter “finiteness” and “infiniteness” in a branch of mathematics other than logic, they are formalizable as first-order properties of first-order entities called sets.
I’m concerned that you’re pushing second order logic too hard, using a false fork—such and so cannot be done in first order logic therefore second-order logic. “Second order” logic is a particular thing—for example it is a logic based on model theory. http://en.wikipedia.org/wiki/Second-order_logic#History_and_disputed_value
There are lots of alternative directions to go when you go beyond the general consensus of first-order logic. Freek Wiedijk’s paper “Is ZF a hack?” is a great tour of alternative foundations of mathematics—first order logic and the Zermelo-Frankel axioms for set theory turns out to be the smallest by many measures, but the others are generally higher order in one way or another. http://www.cs.ru.nl/~freek/zfc-etc/zfc-etc.pdf
“First order logic can’t talk about finiteness vs. infiniteness.” is sortof true in that first-order logic in a fixed language is necessarily local—it can step from object to object (along relation links) but the number of steps bounded by the size of the first-order formula. However, a standard move is to change the language, introducing a new sort of object “sets” and some axioms regarding relations between the old objects and the new objects such as inclusion, and then you can talk about properties of these new objects such as finiteness and infiniteness. Admittedly this standard move is informal or metatheoretic; we’re saying “this theory is the same as that theory except for these new objects and axioms”.
This is what the Zermelo-Frankel axioms do, and the vast majority of mathematics can be done within ZF or ZFC. Almost any time you encounter “finiteness” and “infiniteness” in a branch of mathematics other than logic, they are formalizable as first-order properties of first-order entities called sets.