[A_D_E_P_T]

Yet the very notion of countability in ZFC, which is itself a first-order theory, is rendered completely relative by Löwenheim-Skolem. ZFC itself has a countable model.

[ginnungagap]

Of course, but what is your point?

[cubefox]

If "plenty of interesting properties of familiar mathematical objects cannot be captured by a first-order theory" then that also undermines ZFC, which is a first-order theory.

[nyrikki]

ZFC was specifically designed to be immune to the classic paradoxes of naive set theory: Russell's paradox, the Burali-Forti paradox, and Cantor's paradox.

You are arguing that the ground moves to perfectly fit the shape of a puddle.

Zermelo was one of the first to reference "Cantor's theorem" in his papers.

[cubefox]

These paradoxes do not occur in higher-order logic. You don't need ZFC or any first-order set theory for that. (Also, your comment doesn't address the sentence I quoted.)

[nyrikki]

They don't work in some axiomized higher logic because they chose the rules to avoid them.

HoL not having traditional NOT is an example.

Even in FoL, Peano arithmetic uses the SoL induction to be usable.

There is no free lunch.

[cubefox]

I don't understand what you mean. Higher-order logic does have classical negation. First-order PA tries to approximate the (second-order) induction axiom by replacing it with an infinite axiom schema, but that doesn't rule out non-standard numbers.

[nairboon]

Now where did these classical paradoxes originate in? They stem from Cantor's Mengenlehre