>Yet first order logic encompasses 99.9% of the mathematics anyone ever does, even professional mathematicians.
I'm way out of my depth here, but I'm curious about this statement. In first order logic you can't even assert that the natural numbers cannot be put into a one-to-one correspondence with the real numbers, which seems like a fairly basic mathematical fact.
Right, but you can't ensure that the only models of 'bijective functions' are actually bijective functions. To switch to a slightly simpler example, you can translate statements such as "x is finite" into a first order language (for example, set theory), but you can't ensure that x actually is finite in the models of this statement.
To your first point: yeah, some discomfort around it is valid, but I see it as a non-issue. Informally/philosophically, because a model's job is to capture everything a first-order theory can see about your object of study - so it's fine for (say) an "actually" countable set to model the reals, and not be up to the task of "actually being" the reals. Formally, you differentiate between internal and external statements and don't expect them to be the same (a rigorous version of my pretentious use of scare quotes above :).
I'm way out of my depth here, but I'm curious about this statement. In first order logic you can't even assert that the natural numbers cannot be put into a one-to-one correspondence with the real numbers, which seems like a fairly basic mathematical fact.