Homotopy Type Theory
en.wikipedia.org
en.wikipedia.org
https://www.youtube.com/watch?v=u92V0OMgvhM&list=PL1-2D_rCQB...
HOT is an interesting development. You can fit all existing mathematics within it, in addition to mathematics we have not explored, such as systems where you do not accept the axiom of choice or, more interestingly, disregard it entirely.
It is constructive. This is interesting because it means real numbers "do not exist" as you can not write them down. Specific transcendental constants can be written down because you hold them by their relationship to other numbers.
I had hoped to study it and its application to number theory and computation but it is nearly impossible to get back into school.
...
> It is constructive. This is interesting because it means real numbers "do not exist" as you can not write them down.
Didn't you just contradict yourself? If real numbers do not exist within HTT, then you cannot fit all of existing mathematics in HTT.
You can express the idea that a sequence converges to a limit in constructive mathematics (if not, I'd like to know why) and you can prove that that limit is not rational, nor is it algebraic. That is to say, real analysis works in a constructive setting. At least that's my math-enthusiast understanding of it.
Traditional mathematics even asserts the existence of numbers whose concrete properties we can't even possibly know, such as Chaitin's constant: https://en.wikipedia.org/wiki/Chaitin%27s_constant
My understanding is that these are the kinds of numbers you lose out on when you switch to being a constructivist. I guess you could say that means you can't fit "all of existing mathematics" in it, but to me that feels a bit vacuous.
> In the constructive sense, we don't know the real numbers except the ones that can be talked about using concepts that are more intrinsic to our reality such as rational numbers or circles.
I accept that as being true.
But then, to say that you can fit "all of existing mathematics" feels like you're saying that you can fit everything that fits, and everything that doesn't fit is defined to not be "real" in some sense. That is, it feels circular - like you're so far down the rabbit hole that you can't remember that there's a world above ground that also exists and has validity.
The way I choose to see it, however, is constructivism is the activity of seeing how far you can go with the least possible axiomatic foundation. If, at some point, you need something like the Law of Excluded Middle, you just assert the specific instance that you need as an axiom (and not as a structural rule).
In this sense, then all of mathematics is valid from a constructivist viewpoint, what changes is that now you care about where you assert certain axioms.
A number whose only classification is that it is real is a nonphysical entity. In constructive systems it can not be reasoned about because it can not exist. Something very close to real numbers exists, but situationally. Pi exists because I can describe a procedure to construct it, same for Euler's number.
It is a standard theorem that all constructive results are classical, and that all classical results are either constructively true or not-false. A not-false theorem can't be proven true, but it definitely would lead to a contradiction if it were false.
To get a taste of what's constructive, imagine taking a subset of the finite set {0,1}. We construct the subset by enumerating its elements; a computer program might print out elements one-by-one. So, if we start a program and it prints 0, 1, ...; we know that the subset contains all of the elements and we're done. But if we start a program and it prints 0, 0, 0, ...; only printing zeros, then we have to prove that it halts in order to prove that the subset is finite. Constructively, subsets of finite sets aren't necessarily finite.
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).
I'm sure Mr Hilbert would approve.
"and the formalization of each of these in computer proof assistants."
Aah, loosely IT related (hence the post) and surely Lean and co can't be far away from the discussion.
"As such, this article may not represent the views of all researchers in the fields equally. This kind of variability is unavoidable when a field is in rapid flux."
The WP article is quite dense for a civilian to get through so I hope something cool is on the horizon.
Is a result on the way or has Lean blue screened?
Lean?
WP = Wikipedia
Lean -> https://leanprover.github.io
Coq: https://github.com/HoTT/HoTT
Lean: https://github.com/gebner/hott3
idk what you mean by "blue screened", or results being on the way. afaict most of the non-foundational work present (what I assume you mean by "results") in these libraries are basic properties of basic mathematical concepts being rebuilt on HoTT.