Famously it is impossible to express "finitely many" or "most" and so on in first-order logic, but we can apparently do so in second-order logic. Unfortunately, I cannot find anyone actually doing this and showing how it is done - only references to the fact that it is indeed possible. So my question is whether someone could show me how? I suspect the finite/infinite cases and the most/more cases will be similar to each other, but if not it would be appreciated if someone could illustrate the major differences.
I have proven the former results but I am stuck on this and answers to similar questions (such as this one https://math.stackexchange.com/questions/3661756/second-order-logic-infinity-and-finite) give hints that I unfortunately do not understand. Sorry if I've missed an obvious resource!
I have seen that other questions on this topic raise issues as to how "infinitely many" should be interpreted, as apparently if we take it as "no greatest member" this can be expressed in FOL. Specifically what I'm after is the SOL formula that is true in exactly those models where the extension of (say) F is finite/infinite. In FOL such a formula would violate compactness.
Thank you for your help!
Well, recall Dedekind's definition of finiteness. $A$ is finite if and only if every $f\colon A\to A$ which is injective is also surjective.
This is quite literally a 2nd order quantifier, i.e. "for every function".
Now we can say that there exists only finitely many objects satisfying a property if every injective function defined on the collection of all such objects is also surjective. Infinitely many is just the negation of this, and "cofinitely many" is just the strong negation, i.e. the set of counterexamples is finite.