If I'm reading plato.stanford.edu/entries/philosophy-mathematics/#Cat correctly, a finiteness quantifier $\exists_\text{fin}$ allows us to construct a categorical axiomatization of arithmetic. Does this hold true for real analysis as well?

Also, how does one obtain a categorical axiomatization with this new primitive quantifier?

@user76284 - Not having read any literature on such a quantifier, my first thought is that if you're able to say "for any n, there are finitely many k below n" you will have specified that the order type of your model of arithmetic is omega.

@MaliceVidrine Indeed. Even PA− + your statement is enough, since every model of PA− has initial segment isomorphic to N.

@user76284 In general non-standard quantifiers are too 'powerful' to be actually useful, because they make it impossible to have a deductive system for it, and so the categoricity is simply a pointless illusion. I'm not sure if I mentioned before, but you do realize that, no matter what categoricity result you prove, you are still working within a computable meta-system MS and hence the categoricity is relative to MS, right?

It seems that the only use of categoricity is that it allows you to justify saying "the naturals" and "the reals", but even then it doesn't have any impact on the actual mathematics you prove about them.

Anyway, to answer your question about a categorical axiomatization of real analysis using finiteness quantifiers, you would need to decide what you want to capture. Here is one option that came to my mind:

Use a second-order theory with full impredicative comprehension and the second-order supremum axiom and construct N as described as in my post. Now you can use the finiteness quantifier to force N to be essentially unique, and this forces the rest of the structure R to be contained withing the real reals, since every element has an upper bound in N (exercise for you) and so every element is the supremum of some set of rationals.

Without the statement using the finiteness quantifier, this theory is stronger than Z2 (full second-order arithmetic), because you can construct any subset of N using quantifiers over subsets of N. In that sense it is capable of doing (almost) all real analysis. But even with the extra statement forcing N to be unique, it still doesn't force every model to be isomorphic to the reals, because there are countable ω-models of Z2.

So it doesn't quite work. There may be a way around this, let me think.

I give up. I can't even find a way to force a structure to have uncountable cardinality using the finiteness quantifier.

What about a different quantifier? Perhaps one that has a similar level of conceptual simplicity?

Somehow, I doubt so.