scapp

You sound like you need to read this [0] answer to the question "Are real numbers countable in constructive mathematics?".

> You are using the word "constructive" in an unusual way. It is true that, in ZFC, the set of computable real numbers is countable, but that is not directly a statement about constructive mathematics.

> Not every school of constructive mathematics identifies real numbers with algorithms; that's a characteristic of the "Russian" school as I understand it. In other schools of constructivism that I am more familiar with, real numbers are coded by elements of 2^ω, or by a certain type of Dedekind cut on the rationals. In such schools it is not universally assumed that every real number is associated with a finite algorithm.

> Even in the Russian school, they would not say that the set of real numbers is countable. Because, if you identify real numbers with algorithms, there is no computable enumeration of computable reals that lists all computable reals, and so the translation of "the real numbers are countable" into this setting is false.

> That phenomenon also occurs in classical computable analysis. The subsystem RCA0 of second-order arithmetic has a model in which every real number is computable. But this subsystem still proves that there is no surjection N -> R.

---

It's worth noting that another answer to that question (Andrej Bauer's) gives a constructive proof that the real numbers are uncountable using with the axiom of countable choice. The question of whether it's provable without the axiom of countable choice is open (though see this [1] fairly recent paper on a proof for MacNeille reals).

[0] https://mathoverflow.net/questions/30643/are-real-numbers-co...

[1] https://arxiv.org/abs/1902.07366

You're right. I must have been thinking of one of those extensions you're talking about (F# maybe?). I should have remembered that System F is part of the lambda cube, so it's at least as consistent as CoC

System F isn't consistent as a logic (pretty much precisely because it has general recursion). In languages with general recursion, you can do things like

(Haskell)

    anyType :: a
    anyType = anyType

or

(Rust)

    fn any_type<T>() -> T {
        any_type()
    }

> A consequence of HOT in relation to programs is that you can compare programs for equality without running them. I rediscovered this a few years ago. It means that e.g. certain physical simulations could be known to not complete without running them to assumed termination. Currently we are wasting millions of dollars running simulations that we could show will not produce valid results.

I'm curious where you got this idea. Even if you express programs in HoTT so that equality of these programs corresponds to (say) identical outputs, there's no reason that this equality should be decidable any more than it is in ordinary mathematics.

You might be confused by the fact that HoTT is (by default) constructive, but just because you can define something in HoTT does not mean that its equality is decidable. In fact, that's a defining property of constructivity in this context: if every type has decidable equality, then the law of excluded middle holds. The proof isn't too hard: simply apply the decidability of equality to the type of propositions and for a given proposition P, check if P = True is true or false.

> systems where you do not accept the axiom of choice or, more interestingly, disregard it entirely.

I'm wondering what the difference between those two is. "not accept" and "disregard" are synonyms to me, but maybe you have something more precise in mind. There's a distinction between not accepting an axiom (so that you're agnostic on the question of whether it holds) and accepting its negation. Maybe that's what you're thinking of.

> it means real numbers "do not exist" as you can not write them down.

In light of your other comment, I'd phrase this as "there are particular real numbers that don't exist" or "some real numbers don't exist". As written, it reads as if the set of real numbers doesn't exist.

Even so, keep in mind the difference between not being able to prove something and being able to prove its negation. HoTT is consistent with adding in more axioms (as you alluded to above) which do imply that Chaitin's constant exists. So that means that the base theory can't prove that such constants don't exist (unless the base theory is inconsistent).

The Frobenius theorem characterizes finite-dimensional associative real division algebras as being isomorphic to the reals, the complex numbers or the quaternions. The hyperreals aren't finite-dimensional as a vector space over the reals (for example, if Ɛ is an infinitesimal hyperreal, then Ɛ, Ɛ², Ɛ³, Ɛ⁴ ... are linearly independent over the reals).

A simpler example of another real division algebra (and in fact, another field) is the field of rational functions with real coefficients. This field is also infinite dimensional over the reals (for example, 1, x, x², x³... are linearly independent).

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

> by the way, most infinite orders are isomorphic to the natural numbers as well, with the exception of the ones for which Cantor’s diagonal argument applies

There are at least two things wrong with this statement.

First, "the ones for which Cantor’s diagonal argument applies" is a bit vague. I assume it's supposed to be a reference to uncountable sets, but as written, it's (probably) referring to the general version of the argument that shows that the powerset of a set is strictly larger than the set itself. Thus, a set "for which Cantor's diagonal argument" applies is a powerset.

But not all uncountable sets (or even all uncountable total orders) are powersets. For example, any strong limit cardinal[0] can't be a powerset. Obviously, no uncountable total order can be isomorphic to a subset of the natural numbers. You can then well-order that strong limit cardinal to get a total order which isn't a powerset and isn't isomorphic to a subset of the natural numbers.

Second, even countable total orders are much more varied than subsets of the natural numbers. For example, the integers form a total order which can't be isomorphic to a subset of the naturals. The integers are unbounded below, but any subset of the naturals is bounded below (by 0, e.g.).

As another counterexample, the set of rational numbers in [0, 1] forms a total order which is dense: between any distinct elements of the total order, there's another distinct element between them.

You can get a nice theorem along these lines, though. Every countable total order is isomorphic to a subset of the rational numbers. [1]

Of course, the word "most" here is ambiguous, but seeing as there are uncountably many non-isomorphic, countable, total orders (for example, the number of countable ordinals is uncountable), but only countably many non-isomorphic subsets of the naturals, I think it's inappropriate.

[0] https://en.wikipedia.org/wiki/Limit_cardinal [1] https://www.whitman.edu/mathematics/higher_math_online/secti...