[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.

[nyrikki]

Cantor's proofs showing that Z and Q are countable and R is uncountable.

Cantor's "diagonalization proof" showed that.

Turing extended to the computable numbers K, which can be conceptualized as a number where you can write a f(n) that returns the nth digit in a number.

The reals numbers are un-computable almost everywhere, this property holds for all real numbers in a set except a subset of measure zero, the computable reals K which is Aleph Zero, a countable infinity.

The set of computable reals is only as big as N, and can be mapped to N.

It is not 'non-standard numbers' that are inaccessible, it is most of the real line is inaccessible to any algorithm.

Note the following section for the first part.

"Non-Absoluteness of Truth in Second-Order Logic"

https://plato.stanford.edu/entries/logic-higher-order/#NonAb...

[nyrikki]

Well-founded relations is probably a good lens on why the above is important.