internal-methods VS Reals-as-Oracles

Setting philosophy aside, one of the major applications of constructive logic is that it's the internal language of toposes (and related kinds of categories). This usually simplifies proofs considerably and can produce new results.

Some examples, Joyal and Tierney's An extension of the Galois theory of Grothendieck, CJ Mulvey's papers from the 70s (Intuitionistic algebra and representations of rings for example) and Blechschmidt's A General Nullstellensatz for Generalized Spaces.

Johnstone's Sketches of an Elephant often has both internal and external proofs for comparison and it's easily seen that the internal version is both easier to write and to understand.

For an article explicitly focused on using internal languages in algebraic geometry, see Blechschmidt's notes [0]. In particular, section 20 is dedicated to proving things that are difficult without the internal language.

[0] https://github.com/iblech/internal-methods

I think having a language that helps understand those limitations is a useful achievement. Much of mathematics does have that. A notable exception is the definition of real numbers. They are usually presented as a string of infinite decimals, or a converging sequence, or a set of numbers less than something. All of those notions obscure the basic limitation of knowing the real number and give a veneer of similarity to rational number. Rational numbers are numbers that we can have in our hand while irrational numbers are ones which we can never have. It is important to have a setup that respects that difference.

This is what motivated me to come up with a new definition of real numbers, namely, they are objects (I call them oracles) that answer Yes or No when asked if the number ought to be between two given rational numbers. Abstracting out what properties such an object should have, one can come up with a space of these oracles, define an arithmetic, and prove that they satisfy the axioms of real numbers.

For details: https://github.com/jostylr/Reals-as-Oracles/

In many ways, this is giving a definitional support to the use of interval analysis which is, of course, a very practical concern. It also brings our some cool stuff about mediants and continued fractions (nothing new about that, but nicely motivated).

It also fits in with the adjacent post about busy beaver numbers and its conclusion about knowing a number is in an interval.