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

Let's look at Kolmogorov axioms here: (http://mathworld.wolfram.com/KolmogorovsAxioms.html)

Everything that is needed is a set $W$, some $Q_i$, that can be "anything", a function $Q_i$ from the $Q_i$ to real numbers, and a function "complement" on the $Q_i$.

Let's consider as our probability space the segment [0, 1].

I can take for $Q_i$ the closed sets included in [0, 1] made of countable number of non overlapping segments with non zero length, and for $W$ the set of all these sets. The complement of a $Q_i$ will be the closure of the remaining part of [a, b] when I remove the $Q_i$. There are no $Q_i$ of zero measure (and this is very reasonable for a probability theory: every event that can happen must have a non zero probability to happen).

The complement of a $Q_i$ overlaps with $Q_i$ only on the end points, and that is compatible with the axioms: the sum of measures adds up to 1.

The elements of $W$ are simply ordered pairs of real numbers instead of single real numbers, but everything works at the same way: from the point of view of set theory two segments are equal if and only if the extremes are equal: no mention of overlapping segments at all.

The definition of overlapping segments is the usual one: the higher number of the first pair is bigger than the lower number than the second pair.

There is no need to consider infinite sets of points, and for probability theory there is no need to speak about points at all: probability theory does not need zero-measure events, and no physical possible event has zero probability.

P.S. This is only a very simple example to show that it's not contradictory to define probability without points. Pointless topology is much more general than this and makes use of the concept of "locales" (https://en.wikipedia.org/wiki/Pointless_topology)

Is this the Curry-Howard correspondence? — 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

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.

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

OK, I see your point now!

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!

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. — fishfry

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.

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. 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.

About the Cauchy completeness problem, I don't know how to address it, 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.

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"!

Here's the book: https://homotopytypetheory.org/book/

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.
(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.
(iii) Declare the Cauchy reals unworthy and construct the Dedekind reals instead. 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.
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.
"""

Well, I see that the problem is much more complex than I thought...

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.

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..

So, well, in the end I don't have a definitive answer :sad: (but maybe somebody on https://mathoverflow.net/ could have it)


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

"""
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.
"""

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

Hi @Mephist

I've been percolating on all this a few days. The insight I'm taking away is that constructivists care about Cauchy completeness. I hadn't formerly realized that. And I have a bridge from what I know, the detailed bits and bytes of Cauchy sequences (ie "epsilonics") and the corresponding notions in constructive math.

I've learned about as much as I'm going to about constructivism at the moment; and much more than I ever knew in the past.

I still don't see how constructivists can claim (if they do) that they have a model of constructive reals that are Cauchy complete. If that is true, to me it seems that it cannot also be "morally" Cauchy complete. I'm wearing my Platonist hat now, also called realism. And in particular, how constructivists deal with the holes that I claim must be present in the real line absent noncomputable reals. I will most likely need to defer learning more about this till a future time.

But you did point me at a reference that you say sheds some light, so I'll read that at least.

I will now dive into the thread since I was last here and see what there is to see. My intention is to answer any questions that I can, but not make too many assertions that I would have to defend.

Hi,

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.

In the end, math is not an opinion, right? — Mephist

But yes, it is. It's opinion. What math is, how mathematicians think about and practice math, is under constant change.

In a trivial sense a proposition, once proved, is proved forever. But which proofs and which proof frameworks are considered meaningful, changes over time.

Techniques of proof vary over the years, as do standards of rigor. Gauss was the first person credited, in his doctoral thesis of 1799, with a fully correct proof of the fundamental theorem of algebra (FTA), which says that a polynomial in one variable with complex coefficients has a root in the complex plane; and as a corollary, that every n-degree polynomial has n roots, counted to multiplicity. (ie $x^2$ has one root but it's counted twice).

But by today's standards, Gauss's proof wouldn't be acceptable from an undergrad. It is no longer seen as rigorous. In fact the final subtlety in this theorem was nailed down as recently as 1920.

Likewise the categorical revolution started by MacLane in the 1940's has already caused set theory to lose its foundational status in many parts of math. Brouwer's intuitionistic dreams failed to become mainstream in the 1930's, but may end up doing so in the near future. I think of HOTT and constructivism as "Brouwer's revenge."

Likewise type theory, which Russell proposed in order to solve Russell's paradox; but instead, the axiom schema of specification won the 20th century (that's the axiom that says that you can form a set from a predicate only if you have an existing set to quantify the predicate over. And now type theory's a big deal again.

Math is not about the theorems. It's about how mathematicians think about mathematical objects. And in that respect math is constantly changing. Math is a historically contingent human endeavor. It's social and it can be political, just like anything else.

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

At the moment I haven't bandwidth to engage with the probability topic. So to roll this back, I made the following claim:

Claim: Without the axiom of choice you can't do modern probability theory.

I'll now retreat to saying that this is my belief, but if you have refuted my point then so be it. However skimming your argument I see that you refer to pointless topology and locales. These are modern concepts and somewhat specialized. So at worst, my Claim is operable up to a certain level of math, which is still relatively high up the chain in the scheme of things.

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

Ok I read the next two of your posts, and they contain a lot of meat. I want to respond to them but not tonight, it's late here. I will just say ahead of time that I reject all Lowenheim-Skolem arguments for the following meta-reason. The theorem dates from the 1920's or whatever and can always be used to trump any argument. "Oh yeah, well for all you know the reals are countable because L-S."

Now, here is the thing. For a hundred years, mainstream math hasn't cared. L-S is regarded as a curiosity and of course it's technically true, but nobody thinks that way.

So you now have to be making the claim that the constructivists are making the following argument: "For a hundred years we didn't take L-S all that seriously; but now we do." So I'm not convinced.

Also looking ahead to my more detailed comments to come, I believe that there IS a canonical intuitively correct model of the real numbers, and it's the standard reals. The second order standard reals. With the least upper bound axiom, the axioms for the reals become second order (I've always been a little bit shaky on this point so correct me if I'm wrong) and therefore are not subject to L-S.

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. All other models are not. I believe that even a constructivist must be able to conceive of the standard reals (and is thinking of the same structure as the rest of us) and must recognize it at some level as the "real" reals. The only way to avoid this is to fall back on formalism. This is my belief. It may well be that I'm nothing but a product of my education, but I have a very strong intuition of the standard reals and I refuse to believe that others don't.

Anyway those are two points I wanted to make after a quick read of your two lengthy posts, but there is a lot of stuff in there and I'll get to it tomorrow.

Well, I agree with you that mathematical ideas are much more variable and arbitrary then what it seems to be when you learn it at school.
However, as I wrote here (https://thephilosophyforum.com/discussion/5792/is-mathematics-discovered-or-invented/p1), I am convinced that what are now considered the most relevant parts of math are in reality fundamental facts of nature that are not invented by us but only discovered, and that would be discovered in an equivalent form even by an alien civilization.

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

OK, so I have a question: what is this morally correct model of real numbers? The set of all infinitely long decimal representations?

the morally correct model of real numbers is the model most resembling our use of real numbers, i.e. the model that treats the real numbers as being subcountable, wherein the absence of a bijection between the natural numbers and the real numbers is interpreted to imply the following profundity:

There is an absence of a bijection between the natural numbers and the real numbers.

But our use of real numbers (at least for the most part) is in integrals and derivatives, right?
So the "dx" infinitesimals in integrals and derivatives should be the morally correct model? This is how real numbers are intuitively used since the XVII century.

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

Ok, first of two responses to your lengthy posts of page 9.

I didn't understand this para but you said your point was half of Curry-Howard so I'll trust you.

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

I'll have to stipulate that I didn't follow any of this. I can't detour into modal logic right now.

OK, I see your point now! — Mephist

Ok!! This was regarding the fact that there aren't enough computable numbers to plug the holes in the leaky boat of the constructive real line.

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

First, that's not true. Cantor's theorem is a theorem of ZF and it shows that the powerset of the naturals is uncountable. And it's easy to prove the powerset of the naturals is bijectively equivalent to the set of all infinite binary sequences, which can be coded as the reals. So your point appears wrong.

Second, but really first, all Lowenheim-Skolem objections are suspect, because nobody seems to care. So why do constructivists suddenly care? Skolem as I understand it used his theorem to claim that sets are not sufficiently clear from the axioms. Perhaps so. But nobody in a hundred years has ever said, "Oh noes, set theory is destroyed, we have to start over!" Except the constructivists I guess. But I don't see why L-S is suddenly relevant.

Third, the standard reals are (as I understand it but I confess confusion on this point) a second-order theory because of the least upper bound property.

The second order reals are (again, as I understand it, and I am not an expert on these logical matters) categorical, meaning that any two models are isomorphic.

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

Yes and no. Yes, I do make that point. But I am not making a detailed technical argument. Just stating a curiosity that the standard reals have the Goldilocks property with respect to Cauchy completeness.

I mentioned that as a curiosity, not as an argument. I never imagined anyone would disagree.

Still, what I say is true, and you have not convinced me that the constructive reals are Cauchy complete unless you change the definition of a Cauchy sequence in such a way as to change its essential meaning. This is my working thesis and you have not convinced me otherwise.

Of course there are funny models but funny models are not arguments, they're just funny models.

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

If a constructive real requires a computable Cauchy sequence, there can't be enough of them to make up an uncountable set except in the "funny model" sense. I'm rejecting funny models in favor of the standard models.

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

Martin-Lof is a buzzword I hear a lot in these discussions but it doesn't mean anything to me. But of course there are far more functions on the naturals than there are computable numbers. You agree with that.

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

Well you are claiming that constructivists now regard noncomputable reals as existing. That's certainly contrary to my understanding. But if you allow noncomputable numbers in your ontology you have the standard real numbers and not something else.

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.

About the Cauchy completeness problem, I don't know how to address it, — Mephist

I can see that!! (lol)

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

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.

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

Ok second my replies to your two longer posts of 6 days ago.

Here's the book: https://homotopytypetheory.org/book/ — Mephist

Ok true confession I haven't had a chance to look at that yet but it's on my reading list.

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

Setoid. Buzzword of the day. From Wiki:

"In mathematics, a setoid (X, ~) is a set (or type) X equipped with an equivalence relation ~."

Well that tells me nothing at all. Given a set there are lots of equivalence relations on it. I assume they must mean some particular equiv rel of interest to someone. Type theorsist or constructivists or such. But what you quoted didn't explain much I'm afraid, it seems to be missing details. What's a coincidence relation? There's a key detail missing. But ok, onward.

(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

Ok this relates to something I ran across, that Cauchy and Dedekind completeness are equivalent if you accept countable choice. I haven't understood yet why that is but I gather it's not too difficult. And if you accept countable choice, which a lot of constructivists do, then things are not so bad. Countable choice (or sometimes dependent choice) is often enough for the theorems we care about.

(iii) Declare the Cauchy reals unworthy and construct the Dedekind reals instead. — Mephist

Unworthy! LOL. "We're not worthy!!"

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

As far as I can see, the constructivists acknowledge the problems I'm mentioning and are trying to work their way out, but without complete success. Literally: Without "complete" success!

No version of constructively-defined real numbers can possibly be Cauchy complete unless you change the definition.

As far as I can see, I'm not wrong about that even though I'm ignorant of the mighty constructivist struggles to finesse their way out of the problem.

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

Oh what a cool buzzphrase.

I know what a free group is, and a free Abelian group, and a free module over a commutive ring. I can believe that one can define a free complete metric space over Q and I would love to see that definition, since I would probably understand it. Perhaps that's the answer, or at least an answer, to this dilemma.

Well, I see that the problem is much more complex than I thought... — Mephist

We have a meeting of the minds on this. It's certainly more complex than I thought.

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

Don't know. Haven't ever looked at Coq. It seems to me that the desire to be able to mechanically verify proofs (Voevodsky's original motivation) is not exaclty the same as Brouwer's desire to constrain mathematical objects to the realm of the constructible.

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.

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

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.

So, well, in the end I don't have a definitive answer :sad: (but maybe somebody on https://mathoverflow.net/ could have it) — Mephist

It's worth a shot on math.stackexchange since Andrej Bauer hangs out there I believe. Maybe I'll ask one of these days.

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

I read that but I don't know Coq so had to skip the details. But the checked answer invoked Lowenheim-Skolem and adding extra axioms; and also made the point you did (which I completely agree with) that even in ZFC we can only define or compute countably many subsets of the naturals. I'll take away that these points are regarded as valid by constructivists and that if I knew more about all these things I'd be enlightened. But then I'd lose my apparenly naive faith in the standard real numbers. I'd hate to lose that!!

"""
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

Yes yes, perfectly well agreed. Nevertheless the noncomputable (or nondefinable, which is a slightly different notion) reals have a purpose, which is to plug the holes. But clearly my argument hasn't gotten any more sophisticated than that, and in the end I'm probably just not appreciating constructivism.

OK, so I have a question: what is this morally correct model of real numbers? The set of all infinitely long decimal representations? — Mephist

I can live with that. In fact I've read something along those lines in some of the constructivist references. The decimal representations (modulo dual-representations, of which there are only countably many) are a perfectly good model of the reals. They have the least upper bound property so they are in fact the standard reals.

I wanted to comment on the concept of moral correctness. In 1940 ‎Gödel developed the constructible universe, denoted $L$, which is a model of ZF in which both the continuum hypothesis and the axiom of choice are true. In so doing, he showed that these two propositions are at the very least consistent with ZF. [In 1963 Cohen proved that their negations are consistent as well, showing their full independence].

[Note: The constructible universe is a proper class and not a set, therefore it is not actually a model of anything. I've always been confused on this point].

Now everyone could just go, well, we have a nice model, it's a nice universe of sets that decides the truth of these two propositions. Why don't we just assume that $L$ is the true universe of sets and be done with it?

That is, if we denote by $V$ the von Neumann universe, why don't we just adopt the axiom $V = L$, the axiom of constructibility?

The fact of the matter is that we don't do that. Mathematicians feel that $L$ is not the "morally correct" universe of sets. For one thing it doesn't have enough sets.

This is a good example of the concept of moral correctness: That although mathematicians may act like formalists when they're writing proofs (or computerized proof verification systems), deep down inside they are all raging Platonists. Nobody does math because they truly believe it's a meaningless formal game like chess. Mathematicians believe that their work is about something. 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.

If a constructive real requires a computable Cauchy sequence — 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.

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

If you read my posts I have always said the same thing: constructivist logic DOES NOT MEAN assuming that only computable functions exist!
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!

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

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 $F$ be a function from natural numbers to natural numbers." This is an assumption.
I know nothing about $F$: it can even be non computable.
Then I can write "Definition: $G$ is the function that takes a number $x$ and returns the number $x^2 + F(x)$".
Now, if $F$ is not computable, even $G$ will be not computable, but I don't need to know how $F$ is defined in order to define $G$. I can compute $2*G(x) - F(x)$ and obtain $2 x^2 + 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.

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).
In standard logic this is not true, because I can use the axiom of choice even in my definitions.
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. 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.

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

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?

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

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.

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

I think I'll give up with this discussion because I see that is leading nowhere!

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

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...

I think infinity breaks down and becomes impossible when you are dealing with numbers, or any kind of symbol which represents something else. Maths can't work with it but it can still be represented. O

Something like a perfectly balanced, circular orbit with zero friction on the other hand. That's where infinity is. You can't write it down or spell it out but you also have to accept it will theoretically go on forevermore.

The universe is infinite in all directions. If you try to think of infinity as linear, it will always hit a wall.

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

Ok, I see that I said something that induced you to write in caps. Before responding to the interesting technical points in your following posts, let me just go meta for a moment.

I'm trying to wind down my involvement in this thread.

* I have not said anything new for quite some time. *

* My next move, if I were interested enough to make it a priority, would be to dive into the wonderful references you've been giving me all along.

So if it happens that I'm totally wrong about constructivism, totally wrong about everything for that matter, it's ok with me. I've learned more than I ever knew about constructivism and it still baffles me. I understand Coq and the desire to mechanize the checking of published proofs so as to avoid error. That was Voevodsky's original motivation.

I DON'T necessary understand the mathematical metaphysics that seems to accompany neo-intuitionism. I've looked into Brouwer a little bit over the years and I confess I just don't get it. Why tie your hands with constructibility? Much less computability, which is even more restrictive. Computability is trendy right now. After all we mastered the technology only in the past 50 years, and it wasn't tell ten years ago that everyone started walking around with a supercomputer in their pocket named after a fruit. So I'll forgive a certain amount of computational metaphysics. "We're a simulation," "We can upload our minds to a computer," etc. It's nonsense but it's perfectly understandable. Just as everyone thought the world was a machine in the century after Newton. It will pass. Turing showed that there are naturally expressed problems that can't be solved by computer. This lesson hasn't been internalized in our zeal to reinterpret reality in terms of the computable.

Hence neo-intuitionism. The revenge of Brouwer. I'm all for it.

But I just haven't got any level of advocacy or passion in this thread at the moment, since I'm perfectly well out of things to say. So I'm startled to see that anything I said induced a response involving a lot of upper case typing. I assure you that eliciting such a response was not my intention. I'm not dogmatic about anything, I've pretty much said my piece and learned some things.

I'll try to comment on your posts but I'm most definitely not wanting to engage in any disagreements that involve a lot of capitalization.

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

Ok that said. This is different from what I understood from the Italian paper, which is that a real number is characterized by (or identified with) a funny-Cauchy sequence defined by a particular rate of convergence that allows us to show that the modulus of the sequence is computable. If there's anything technical I got from this thread it was exactly that.

But I understand as you've explained to me that there are many different approaches to constructivism; and that in some of them, all Cauchy sequences of rationals represent real numbers, not just the computable ones.

I believe you if you tell me this. But the collection of all [equivalence classes of] Cauchy sequence of rationals is exactly the standard real numbers.

So I believe you if you tell me, but actually, I don't believe you. Because you've just constructed the standard real numbers. So I'm confused again.

If you read my posts I have always said the same thing: constructivist logic DOES NOT MEAN assuming that only computable functions exist! — Mephist

Ok. I will stipulate to being thoroughly confused on this point. But that's ok.

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

I'll stipulate you are correct on this point. I just don't understand the mechanism of construction. Perhaps that's what I'm missing.

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

A computable real is a real number that is computable in the sense of Turing 1936. A noncomputable real is a real that isn't. This is perfectly sensible, isn't it?

And of course you can identify noncomputable reals with noncomputable maps from the naturals to themselves, just as you can identify all the reals with that set.

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

Is a black box like an oracle, a device that can solve a noncomputable problem?

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

Ok, you can refer to noncomputable functions and then computable expressions involving them. That makes sense.

In standard logic this is not true, because I can use the axiom of choice even in my definitions. — Mephist

You haven't related anything to the axiom of choice, I totally didn't get this reference here. It doesn't seem to apply to anything you said. You don't need the axiom of choice to have noncomputable functions.

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

I think you are using AC in a funny way. I tried to correct a couple of instances of this earlier. Nothing we're talking about has anything to do with the axiom of choice.

I do not believe that an oracle in computer science is in any way analogous to the axiom of choice. If you know of a connection perhaps you could explain it. An oracle allows you to compute something that was formerly noncomputable. The axiom of choice doesn't let you compute anything. In fact the elements of the sets given by the axiom of choice have no properties at all and could never be computed by any stretch of the word.

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

I believe you but there's a kernel I'm missing. If the constructive reals let you prove all the same theorems, what is the point? What's wrong with the original proofs? And by "built into the logic," you have a lot of meaning for that phrase in your mind but I don't know what you mean.

Perhaps you need to make your point more simply because I'm not seeing it at all.

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

Right. The real numbers are a continuum. The rational numbers aren't because they're not Cauchy complete. The computable reals are not because they are not Cauchy complete. (I proved this earlier). And the constructive reals ... well I can't say, because I still don't understand the difference between the computable reals and the constructive reals. That's another point of mystery for me.

But even in the standard reals the points are not attached to each other like bowling balls. It's more like infinitely stretchy taffy. You can take any two points, no matter how close together, and stretch the line between them to any length you like.

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

Yes yes this is the part I understand. Coq is a tool for helping to avoid errors in published math. That was Voevodsky's idea.

It's the mystical mathematical metaphysics of Brouwer I don't understand. The claim that every mathematical object should come with a recipe for building it. I've never been excited by that idea. It seems unnecessarily restrictive. After all there is no reason to believe the world is a computer, no matter how many TED talkers assert the proposition.

I
I think I'll give up with this discussion because I see that is leading nowhere! — Mephist

On the contrary. It's been very valuable to me. It's just that I have no more points to make. And you've tried to explain things to me that I haven't understood. The fault is mine.

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

You're right. You could never convince me of that since you're wrong. What if there were a sequence that morally should converge, but there was no limit there? That's the point of Cauchy completeness. You need it to ensure the existence of the limits you need for your integrals and derivatives.

But I sense that you are unhappy or frustrated. At my end I've found this very enlightening and helpful. I appreciate the conversation. If we're done that's good. I may peruse your links from time to time.

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.

Forgive my elementary level knowledge on the subject.

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

In the standard set-theoretic account of the real numbers, the real line is made of points. That is, the line is the union of all the sets that each contain one point, if you think of it that way.

That doesn't mean there's a point and then a "next" point. They're not lined up like bowling balls. Between any two real numbers there's another. In fact between any two real numbers, the points between can be stretched into a new copy of the entire real line. So it's like maple syrup, not bowling balls if that helps.

There are no gaps. "Every Cauchy sequence converges." That's the technical condition that ensures there are no gaps. It means that every sequence that should converge, does converge.

As a helpful example, consider the rational numbers. Between every two rational number there is another. But there are still gaps! For example the sequence of rational numbers 3, 3.1, 3.14, ... that converges to pi, doesn't converge in the rationals. There are gaps in the rationals at every irrational.

But the reals have no gaps. That's their defining property. All the gaps in the rationals are filled in.

I can't speak to constructivist or intuitionist conceptions of the real line. And there's also the hyperreal line, in which every real number is surrounded by a cloud of infinitesimals.

Forgive my elementary level knowledge on the subject. — Noah Te Stroete

It's a deep question, the nature of the mathematical continuum. People have been arguing about it forever.

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.

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

No intrusion at all, I love to talk about the standard real numbers! I'm not sure which part of your question I didn't clarify, I'd be glad to try again if you have more questions. As I understand it you asked how the real numbers can be made of points. You take all the real numbers and collect them into a set. That's the set-theoretic viewpoint. So the real numbers are made of points just as the set of natural numbers {0, 1, 2, 3, ...} is made up of the individual numbers 0, 1, 2, 3, ...

There are no gaps in the real numbers, but i'm not sure which part of this you are asking about.

I guess I got confused because you guys were talking about numbers as points, where I was thinking about zero-dimension points on a two-dimensional line. This stuff to me right now is very esoteric, as I don’t remember the terminology for the different kinds of numbers. I was always better at calculations like an engineer than I was so much interested in or ever had any exposure to theory.