I can't speak to non-pointed set-theoretic probability theory. I know about ETCS (elementary theory of the category of sets) so I understand that sets don't require points. But as to probability, I can't say. However if you take finite line segments as sets, you seem to lose intersections. Are these closed or open segments? You have a reference for this interpretation of probability theory? — fishfry
Is this the Curry-Howard correspondence? — fishfry
All of the familiar mathematical constants such as pi, e, sqrt(2), etc. are computable. However there are only countably many computable numbers (since there are only countably many TMs in the first place). But Cantor's theorem shows that there are uncountably many reals. Hence there are uncountably many noncomputable reals.
Point being that there are only countably many constructive Cauchy sequences (if we require that the modulus must be a computable function) hence the constructive real line is full of holes. It cannot be Cauchy complete. — fishfry
The constructive (ie computable) reals are too small, there are only countably many of them. The hyperreals are too big, they're not Archimedean. Only the standard reals are Cauchy complete. — fishfry
I had an idea to solve the question about Cauchy completeness, that I should have had a long time ago: just look at the book that proposes constructive mathematics as the "new foundations"! — Mephist
In the end, math is not an opinion, right? — Mephist
Everything that is needed is a set W, some Qi, that can be "anything", a function Qi from the Qi to real numbers, and a function "complement" on the Qi. — Mephist
I believe the main source of confusion here is the concept of a model. If you take ZFC and remove some axioms (the axiom of choice and the logical axiom of excluded middle) the set of theorems that you can prove will be smaller, but the set of models of the theory will be bigger.
All models that were valid in ZFC will be still valid in the "reduced" ZFC, because all valid proofs in the reduced ZFC are still valid proofs of ZFC: you can't prove propositions that are not true in the model if you couldn't do it with the full ZFC. — Mephist
The standard reals are the model of time in the Schrödinger equation. Everyone thinks of them the same way. The high school analytic geometry reals. Those are the morally correct reals. — fishfry
Yes... well, half of it: the "proofs-as-programs" interpretation is valid even in the standard first order natural deduction logic, if you don't use excluded middle (the intuitionistic part). Here is a summary of all the rules of first order intuitionistic logic with the associated expressions in lambda calculus: https://en.wikipedia.org/wiki/Natural_deduction#/media/File:First_order_natural_deduction.png — Mephist
The only rule that doesn't fit with this interpretation is excluded middle. You can take a look at the paragraph "Classical and modal logics" in https://en.wikipedia.org/wiki/Natural_deduction for an explanation of why this happens. — Mephist
OK, I see your point now! — Mephist
But consider this (taken from https://en.wikipedia.org/wiki/Real_number under "Advanced properties"):
"It is not possible to characterize the reals with first-order logic alone: the Löwenheim–Skolem theorem implies that there exists a countable dense subset of the real numbers satisfying exactly the same sentences in first-order logic as the real numbers themselves."
Even ZFC can't distinguish between countable and uncountable reals! — Mephist
You often used this argument:
The constructive (ie computable) reals are too small, there are only countably many of them. The hyperreals are too big, they're not Archimedean. Only the standard reals are Cauchy complete. — Mephist
And my answer is: you can assume without contradiction that constructive reals are uncountable, exactly as you do in ZFC! The fact that you can build only a countable set of real numbers only means that you can only consider a countable set of real numbers in the propositions of logic (the same as in ZFC), not that the logic does not allow the existence of an uncountable set of real numbers. — Mephist
Now, let's consider "computable reals". Computable reals are functions from natural numbers to natural numbers (you know better than me: take as input the position of the digit and produce as output the digit). Well, not all of these computable functions are valid terms in Martin-Lof type theory. — Mephist
The set of functions from Nat to Nat that are allowed as valid expressions depends on the details of the rules, and in Coq sometimes it even changes from one version to the other of the of the software. The reason is that the rules of the language must allow to build only total recursive functions (functions that always terminate), otherwise the logic becomes inconsistent.
So, the functions that you can actually build using the rules of the logic correspond only to the Turing machines that are provably guaranteed to terminate (by using the meta-logic of the language, not the language itself), and that of course is a strict subset of all the Turing machines. But this IS NOT the entire set of functions from Nat to Nat that is assumed to exist, at the same way as the set of real numbers of which you can speak about in ZFC is not the set of real numbers that is assumed to exist. — Mephist
About the Cauchy completeness problem, I don't know how to address it, — Mephist
because in constructivist logic there are different axiomatizations of real numbers that are not equivalent between each other, and even not equivalent to ZFC reals. You can consider it a defect of the logic, but you can even consider it an advantage, because the thing that all these the axiomatizations have in common (well, not sure if all, but at least the two or three that I have seen..) is the set of theorems that is sufficient for doing analysis. So, the degree of freedom that is left out and makes the difference between the various constructivist axiomatizations corresponds to the aspects of ZFC reals that are not so "intuitive", such as for example the difference between point-based or pointless topology. This, in my opinion, means that there is not only one intuitively correct definition of what are real numbers. — Mephist
I had an idea to solve the question about Cauchy completeness, that I should have had a long time ago: just look at the book that proposes constructive mathematics as the "new foundations"! — Mephist
Here's the book: https://homotopytypetheory.org/book/ — Mephist
Chapter 11.3 Cauchy reals:
"""
There are three
common ways out of the conundrum in constructive mathematics:
(i) Pretend that the reals are a setoid (C, ≈), i.e., the type of Cauchy sequences C with a coincidence relation attached to it by administrative decree. A sequence of reals then simply is
a sequence of Cauchy sequences representing them. — Mephist
(ii) Give in to temptation and accept the axiom of countable choice. After all, the axiom is valid
in most models of constructive mathematics based on a computational viewpoint, such as
realizability models. — Mephist
(iii) Declare the Cauchy reals unworthy and construct the Dedekind reals instead. — Mephist
Such a verdict is perfectly valid in certain contexts, such as in sheaf-theoretic models of constructive
mathematics. However, as we saw in §11.2, the constructive Dedekind reals have their own
problems. — Mephist
Using higher inductive types, however, there is a fourth solution, which we believe to be
preferable to any of the above, and interesting even to a classical mathematician. The idea is
that the Cauchy real numbers should be the free complete metric space generated by Q.
""" — Mephist
Well, I see that the problem is much more complex than I thought... — Mephist
However, solution (i) is the one used in Coq standard library (the one that I knew). And, as I said, in that case Cauchy completeness is an axiom, so.. no problem! :smile:
However, I don't know how to prove that for each ZFC real there exists only one constructive real that verifies all possible propositions expressible in ZFC, and maybe you are right that this cannot be done. — Mephist
He proposes a fourth solution, based on the hierarchy of infinite sets typical of Homotopy Type Theory, and in 11.3.4 he proves Cauchy completeness. But I don't know HOTT enough to prove anything in it.. — Mephist
So, well, in the end I don't have a definitive answer :sad: (but maybe somebody on https://mathoverflow.net/ could have it) — Mephist
P.S. I found an answer about countability of constructivist real numbers here: https://stackoverflow.com/questions/51933107/why-are-the-real-numbers-axiomatized-in-coq — Mephist
"""
As for your second question, it is true that there can be only countably many Coq terms of type R -> Prop. However, the same is true of ZFC: there are only countably many formulas for defining subsets of the real numbers. This is connected to the Löwenheim-Skolem paradox, which implies that if ZFC is consistent it has a countable model -- which, in particular, would have only countably many real numbers. Both in ZFC and in Coq, however, it is impossible to define a function that enumerates all real numbers: they are countable from our own external perspective on the theory, but uncountable from the theory's point of view.
""" — Mephist
OK, so I have a question: what is this morally correct model of real numbers? The set of all infinitely long decimal representations? — Mephist
That is: If you now claim that the constructive reals are the computable reals plus the noncomputable reals, you've completely conceded my point; and, I imagine, horrified all the constructivists who don't believe that at all. — fishfry
That's an awful lot of handwaving IMO. But there IS an intuitively correct definition of the real numbers: A Cauchy-complete totally ordered field. That's a second-order, categorical axiomitization. It was familiar to Newton and to every high school student.
I can believe that constructivists prefer a different model or models. I can NOT believe that anyone trained in math claims to not have an intuition of the standard reals. That is, I can imagine a constructivist saying, "The standard reals can't be right because you can't explicitly construct most of them." Of course that's true. But I can't believe anyone saying they have no mental picture of the standard reals as locations on the real line. — fishfry
In other words Coq is all well and good, but if it's just to verify proofs, must we abandon standard math to use it? Perhaps I'm missing the subtleties here. — fishfry
I find it fascinating that constructivists claim to be able to prove the Cauchy completeness of a set, namely the real numbers, whose elements manifestly can not all be computed. But at least I've learned that people are making the effort. — fishfry
The intuition of a line being made of points and having no gaps is VERY unintuitive, and it's NOT used in standard mathematics: integrals and derivatives are defined as limits of sequences: no sets of points at all. But I am sure I can't convince you about this and I don't see the point of going in circles repeating the same things...They have intuitions about what these things are; and just because there is a funny model with some property, they do NOT stop there. If the model doesn't match the intuition, the model becomes a handy formal device but the search for mathematical truth continues unabated. — fishfry
NO! A constructive real DOES NOT REQUIRE a computable Cauchy sequence!
ALL Cauchy sequences of rational numbers (computable AND INCOMPUTABLE) are PERFECTLY VALID real numbers in constructive logic. — Mephist
NO! A constructive real DOES NOT REQUIRE a computable Cauchy sequence!
ALL Cauchy sequences of rational numbers (computable AND INCOMPUTABLE) are PERFECTLY VALID real numbers in constructive logic. — Mephist
If you read my posts I have always said the same thing: constructivist logic DOES NOT MEAN assuming that only computable functions exist! — Mephist
If somebody that is reading this knows about constructivist logic and thinks that this is not true, PLEASE reply to this post and say that it's not true! — Mephist
P.S. Now I know what computable reals are, but I still don't have a definition of non computable reals: I imagine that you mean functions from naturals to naturals that are not computable — Mephist
P.S. Maybe I'll try to explain the difference between assumptions and definitions (I know that it's an elementary concept, but maybe it's not so clear).
In constructive logic I can write "Let FF be a function from natural numbers to natural numbers." This is an assumption.
I know nothing about FF: it can even be non computable.
Then I can write "Definition: GG is the function that takes a number xx and returns the number x2+F(x)x2+F(x)".
Now, if FF is not computable, even GG will be not computable, but I don't need to know how FF is defined in order to define GG. I can compute 2∗G(x)−F(x)2∗G(x)−F(x) and obtain 2x2+F(x)2x2+F(x).
F(x)F(x) will never be expanded or computed, because is treated as a "black box" that I assume to exist but can't be used to calculate actual natural numbers. — Mephist
So, the point is that I can assume the existence of non computable functions, but I must use computable functions in my definitions (in this case the square and the addition functions). — Mephist
In standard logic this is not true, because I can use the axiom of choice even in my definitions. — Mephist
In constructivist logic instead you shoud add the axiom of choice as an assumption (or axiom), and then you can use it as an "oracle function" ( a black box, such as F(x) ) inside your definitions. — Mephist
At the end, using constructivist logic you can even do exactly the same proofs that you do in standard logic, but you have to add the appropriate axioms explicitly as assumptions, because they are not built into the logic itself. — Mephist
You can use exactly the same definition of Cauchy-complete totally ordered field in constructivist logic. Even rational numbers are locations on the real line. The problem is with continuity: points are not "attached" to each-other, right? — Mephist
It's not about verifying proofs. In every formal logic proofs can be verified mechanically, otherwise it wouldn't be called "formal" logic. It's about the complexity of rigorously written proofs. In ZFC complete formal proofs become so long that nobody uses them in practice. In Coq the situation is much better. In HOTT is even better.
You don't have to abandon standard math to use Coq or HOTT. You can use HOTT to do perfectly standard math with a much simpler formalism for proofs: that's why it's proposed a new foundation of ALL mathematics. — Mephist
I
I think I'll give up with this discussion because I see that is leading nowhere! — Mephist
I
The intuition of a line being made of points and having no gaps is VERY unintuitive, and it's NOT used in standard mathematics: integrals and derivatives are defined as limits of sequences: no sets of points at all. But I am sure I can't convince you about this and I don't see the point of going in circles repeating the same things... — Mephist
A line is made of points with no gaps? Now I don’t know any theory, but what I intuitively grasp from taking calculus is that a point has zero dimensions. A line is not made of points. A point just divides a line into two segments. — Noah Te Stroete
Forgive my elementary level knowledge on the subject. — Noah Te Stroete
Well, thank you for trying to explain it to me. I guess I’m really not interested enough to do further studying. It seems like a meta question or concern whose answer may have little consequence... but it may just seem that way to me because of my ignorance.
I apologize for the intrusion. — Noah Te Stroete
Get involved in philosophical discussions about knowledge, truth, language, consciousness, science, politics, religion, logic and mathematics, art, history, and lots more. No ads, no clutter, and very little agreement — just fascinating conversations.