scapp

7 ms·

31.
by scapp 5y ago
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
32.
by scapp 5y ago
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
33.
by scapp 5y ago
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_typ
34.
by scapp 5y ago
> 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 withou
35.
by scapp 5y ago
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 r
36.
by scapp 5y ago
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. Som
37.
by scapp 6y ago
> 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