My knowledge of QM is very limited, but I think that the wave function collapses to a 'particle' when measured - at least for particles like the photon. A very small, collapsed, wave could be mistaken for a point particle? It would seem neat and tidy if all particle types had similar behaviour in this regard (string theory comes to mind). But probably we have to stick with uncollapsed waves from what you are saying. They could still be centred on a discrete grid point though.

I think that our theories use continuous variables as an excellent approximation for a reality that is discrete on such a fine level that it appears continuous to us (and thus continuous theories give results very close to reality). So continuous calculus gives good results but does not reflect the micro nature of reality correctly. This seems to be how classical physics works - the classical approximation of (what we now know to be) discrete matter are good enough because discreteness of matter only manifests its effects in the micro world.

I believe that if we ever hit on a ToE then it will be a discrete theory and utterly useless for predicting behaviours in the macro world - a quantum theory of gravity would never be used to try to predict the orbits of the planets for example - we would stick with Newton/Einstein for that. It would be useful in understanding the early moments of the Big Bang though.

My knowledge of QM is very limited, but I think that the wave function collapses to a 'particle' when measured - at least for particles like the photon. A very small, collapsed, wave could be mistaken for a point particle? It would seem neat and tidy if all particle types had similar behaviour in this regard (string theory comes to mind). But probably we have to stick with uncollapsed waves from what you are saying. They could still be centred on a discrete grid point though. — Devans99

If I had a reasonable explanation of what the collapse of the wave function means I would immediately publish it and I would become the most famous physicist of the world :grin:

In my opinion the most likely interpretation of quantum mechanics should be a somehow refined version of the many-world interpretation ( https://en.wikipedia.org/wiki/Many-worlds_interpretation ). But, as it is now, even this interpretation doesn't make sense. A collapsed wave is not smaller than an uncollapsed one: a collapsed wave is part of classical mechanics, and all experiments are part of classical mechanics. Quantum mechanics simply does not describe experiments. It describes the evolution of any physical system as the evolution of an abstract mathematical object (a vector in an infinite-dimensional vector space, called the state-vector) that does not correspond to any real physical object. And you can use that object to predict the probability of an experiment by the "trick" of making the state-vector (or wave-function) collapse, but the experiment itself must be described using classical mechanics, not quantum mechanics. So, practically, inside quantum mechanics there are not "collapsed wave functions". The collapsed wave function is the mathematical "trick" used to make in some way a state-vector (or wave -function) become "visible" from classical-physics observer.

I think that our theories use continuous variables as an excellent approximation for a reality that is discrete on such a fine level that it appears continuous to us (and thus continuous theories give results very close to reality). So continuous calculus gives good results but does not reflect the micro nature of reality correctly. This seems to be how classical physics works - the classical approximation of (what we now know to be) discrete matter are good enough because discreteness of matter only manifests its effects in the micro world. — Devans99

Yes, exactly. But I think that in any case, whatever theory you use, physical results will always be only approximations. You can say that if you measure quantities that are fundamentally discrete, you can measure them with exact precision. But in quantum mechanics there is the problem that for very high degrees of precision you cannot be sure that the measure is correct: results have only a statistical meaning.

However, even if it were possible to create a model that is fundamentally discrete in all variables and described reality with absolute precision, it probably would be so complex that would be impossible to use!

The advantage of using infinity and differential equations instead of finite-difference equations (https://en.wikipedia.org/wiki/Finite_difference) is that calculations become much, much simpler. Without infinities, there are no symmetries. And without symmetries the laws of physics become a complete mess, impossible to use (even if they were the most accurate possible description of the real world).

P.S. I have a very good example of this kind related to computer-science that probably is easier to understand: computers are not able to represent natural numbers exactly, because memory locations are finite. But when you use them, you treat them as if the memory locations were infinite. You don't take into account what happens if the digits don't fit into memory: simply you take a bigger memory location so that you don't have to worry about the size.
Why? Because finite-precision arithmetic is much more complex that regular arithmetic, and if you had to take into account the finite size of memory locations, it would become impossible to reason about programs. Well, a very similar thing happens with the use of infinities in physics.

Hi @Mephist, Thanks for your responses.

So, I'll try to change my style of writing: go straight to the answer of only one specific question and keep the post short and focused on one question at a time. — Mephist

Ok I've satisfied myself on the use of the rate of convergence in the Italian paper. The short answer is that by controlling the rate of convergence, the function that inputs $\epsilon$ and outputs a suitable $N$ in the Cauchy definition is a computable function. Now that makes sense and I see what they're doing.

But this necessarily leaves out all those Cauchy sequences whose convergence rates are not so constrained; and the limits of those sequences can not be Italian-Cauchy reals. But they are standard reals (being the limits of Cauchy sequences). So what the constructivists call Cauchy complete can not be actual Cauchy completeness. I am pretty sure about this. If the constructivists don't care, all fine and well. A lot of smart people are constructivists these days so I'm sure the fault is my own. But the Italian definition of a Cauchy sequence omits a lot of more slowly converging sequences unless I am mistaken (I haven't fully gotten to the bottom of this yet).

The Italian paper is about a formalization of real numbers in Coq:
"We have formalized and used our axioms inside the Logical Framework Coq" (from the first page).
That's why I was speaking about Coq — Mephist

Aha! Well that makes perfect sense. I didn't read the whole paper, just latched onto their completeness axiom.

Ok. Question: How can any model of the reals built on constructive principles be Cauchy complete?
— fishfry

Answer: because Cauchy completeness is assumed as an axiom of the theory (this is not a model of the reals because real numbers are described axiomatically). You can argue about the consistency of the theory, but you cannot argue about Cauchy completeness. Cauchy completeness is assumed as an hypothesis. — Mephist

Yes but what the Italian paper calls Cauchy completeness is not what I would call Cauchy completeness. They include only the limits of a small class of Cauchy sequences, namely those that converge at a particular rate. Again if this actually includes more than I think it does then I'll correct myself later, but as I understand it, they require the function that inputs epsilon and outputs N to be computable, and that must necessarily leave out a lot of Cauchy sequences. As I understand it.

Let me rephrase the question: "If a sequence is Cauchy in ZFC, is it Cauchy in intuitionist math?"
This question is too vague to have an yes/no answer:
"a sequence is Cauchy in ZFC" we know what it means.
"a sequence is Cauchy in intuitionist math" I don't know what you mean.

The adjective "intuitionist" is a property of a logic. You should say of what theory of real numbers (formulated in that logic) you are referring to. — Mephist

The Italian paper definition. Or in general, any theory that requires the epsilon-N mapping to be computable.

I can try to interpret it as "a sequence is Cauchy in the theory of real numbers of the Italian paper". — Mephist

That works. Or in general, in any constructive theory in which the "modulus" of the Cauchy sequence, which is their name for the epsilon-N mapping, must be a computable function.

Answer: If you take a Cauchy sequence in ZFC, you have a set of sets such that... (a proposition about that set of sets). Not all sets of sets that are expressible in the language of ZFC have a corresponding term of type R (the type of real numbers) in the language used in the theory of the Italian paper. So, you cannot really compare them. — Mephist

I don't know what your set of sets refers to. But if the modulus of a Cauchy sequence must be computable, that necessarily omits all those Cauchy sequences whose modulus isn't computable. That seems to be the entire point.

Put it in another way: which logic do you want to use to compare the two sequences? The first one is expressed in first order logic, the other one in Coq (If you don't want to speak about Coq, please choose another concrete intuitionistic logic and model of real numbers. There are too many of them to be able to speak in general). — Mephist

The meaning of a computable modulus is perfectly clear to me. It's a significan restriction, or at least seems like a significant restriction, in the definition of a Cauchy sequence. It seems that there must exist sequences (of rationals, say) such that the sequence is standard-Cauchy but not constructive Cauchy.

The definition of real numbers in the Italian paper is on the third page. The last axiom of that definition is this one:

completeness:∀f:N→R.∃x∈R.(∀n∈N.near(f(n),f(n+1),n+1))→(∀m∈N.near(f(m),x,m))completeness:∀f:N→R.∃x∈R.(∀n∈N.near(f(n),f(n+1),n+1))→(∀m∈N.near(f(m),x,m))

Is that what we are speaking about? ( finally I learned how to write symbols :-) ) — Mephist

Yay on the symbols!! Best thing since sliced bread. My handwriting always sucked. I wish they'd had that back in the day.

Sorry I didn't read that far in the paper but I'll review that part. But my main point stands. If the modulus must be computable then the constructive reals are missing a lot of limits of standard-Cauchy sequences.

[ I don't want to address too many points because I'll go off the road again. So, I'll wait for an answer about these ones for the moment ] — Mephist

Ok it's all good!

The constructive reals are Dedekind complete but not Cauchy complete
— fishfry

Hmm.. I am sorry that I have always to disagree with what you say, — Mephist

Ok I'll stop here because the next thing you wrote is lengthy and I have to digest it.

The simplest topology that corresponds to Euclidean geometry is that of flat, infinite space. So by Occam’s razor, we can conclude that in the absence of evidence to the contrary, the universe appears infinite. — Mark Dennis

I don't want to get sidetracked into all that but every time I take a look at these ideas, I come away thinking that the physicists have a very different concept of infinity than the mathematicians do. The "flat universe" argument leaves me ... flat. If I could only make one brief response to that idea it's that the supporting observations only apply to (by definition) the observable universe, which is a tiny part of the universe. So at best the observable universe appears to have a flat topology, which leaves a lot of options on the table. An infinite universe is by no means the Occam choice. The assumption of infinity is very strong and is not necessary. It can be replaced by, for example, a toroidal topology. Everybody knows this. The infinite universe is a weak argument.

in the absence of evidence to the contrary — Mark Dennis

And besides .. you can never observe the evidence to the contrary if it's outside the observable universe. So this is one of those self-fulfilling ideas that is popular but unprovable.

But this necessarily leaves out all those Cauchy sequences whose convergence rates are not so constrained; and the limits of those sequences can not be Italian-Cauchy reals. But they are standard reals (being the limits of Cauchy sequences). So what the constructivists call Cauchy complete can not be actual Cauchy completeness. I am pretty sure about this. If the constructivists don't care, all fine and well. A lot of smart people are constructivists these days so I'm sure the fault is my own. But the Italian definition of a Cauchy sequence omits a lot of more slowly converging sequences unless I am mistaken (I haven't fully gotten to the bottom of this yet). — fishfry

Yes, you are right. This leaves out all Cauchy sequences whose convergence rates are not computable. Because in ZFC you can define non computable functions by using the axiom of choice, that is not available in constructive mathematics. These (the ones left out) are the Cauchy sequences that are not expressible as an explicit formula (or algorithm), and then are not expressible at all in constructivist mathematics. Put it in another way: non constructive mathematics has more functions than constructive mathematics. The additional functions are the ones that you can define only by using the axiom of choice.
But I would like to stress an essential point that maybe you missed: the axiom of choice is not incompatible with constructivist mathematics: it's only an independent axiom (not refutable and not provable). So, if you add it to constructivist logic, you obtain... non constructivist logic! This is not a limitation, but it's only a choice to treat this axiom not as a "logical axiom" (that you are forced to use because it's built into the logic), but as an axiom of your theory (the theory of real numbers, for example). In this case the axiom can be seen as an "oracle function": a function that is not computable, that you assume to exist. In constructivist logic (at least the one used in Martin-Lof type theory, the one that I know) there are no logical axioms at all. Only logical rules! That, in my opinion, is an advantage, not a limitation: keep axioms out of logic and all logical symbols become mere definitions. The only primitive concept that remains as an integral part of logic is... computable functions!
Let me repeat it once again: you can get classical logic out of constructivist logic in a very simple way: just add an axiom to the theory! But if you want to reason about an universe where only computable functions exist using classical logic, the only way that I know is to use the internal language of topos theory (part of cathegory theory). Because you can easily add an axiom to a theory, but you are not allowed to take out an axiom from logic. It's just a much nicer "factorization" between what's part of the logic and what's part of the mathematical theory that you are building.

Is this that non Euclidean geometry? I’ve so far only read about this in reference but don’t quite understand it.

However, It would be a rather strange universe if it stops being flat outside of the observable universe. Unless you’re suggesting that it only appears to be Euclidean due to our observing of state/vectors?

I’m a pragmatist so I have a hard time really engaging with ideas until I know what purpose they serve to us now.

Because in ZFC you can define non computable functions by using the axiom of choice, that is not available in constructive mathematics. — Mephist

Still working on my response to the lengthy final part of your earlier post about whether the constructive reals are Cauchy complete. Such an interesting topic!

I just wanted to clarify one technical thing about what you wrote. This will be a standalone post so I can present a somewhat involved example at the end.

ZF is already nonconstructive. That is there are three levels of specifying a set: Computability, ZF, and ZFC. In other words we don't just jump from computability to the axiom of choice. ZF already gives noncomputable sets. You made that minor error in your earlier post then repeated it so I wanted to clarify this. The three levels of identifying the elements of a set (if you think of it that way) are:

* Computability. We have a Turing machine that generates all and only the elements of the set;

* ZF. We have statements of existence of sets we can't compute. The powerset axiom for example is very powerful. Cantor's theorem is a theorem of ZF so that the powerset of the naturals must be uncountable; yet there are only countably many Turing machines. So most of the subsets of the naturals are noncomputable sets. No axiom of choice is needed for ZF-noncomputability.

One little fact I know about this is that although there are only countably many Turing machines, there are not constructively countably many. Although in ZF we can enumerate the Turing machines, no such enumeration can be computable! That's because a computable enumeration of TMs would effectively solve the Halting problem, which Turing showed can't be done. So a constructivist could deny that the set of TMs is countable. That's kind of what they're doing with Cauchy sequences, subtly redefining a technical term then saying they still satisfy the definition.

* Then the axiom of choice gives you yet another level of incomputability. Have you seen the standard example? Let me just present it since this is a standalone post and perhaps some reader hasn't seen this.

Start with the real numbers $\mathbb R$. Define the following relation $\sim$ on them. For two reals $x$ and $y$ we say that $x \sim y$ if and only if it happens to be the case that $x - y \in \mathbb Q$; that is, the difference of $x$ and $y$ is a rational number.

We can verify that $\sim$ is an equivalence relation (proof by reader), so that it therefore partitions the reals into a collection of equivalence classes. In fact each equivalence class is countable, and there are uncountably many equivalence classes (again proof by reader).

The set of equivalence classes is usually denoted $\mathbb R / \mathbb Q$ and called "the reals mod the rationals."

Now by the axiom of choice there is a set, call it $V$, consisting of exactly one element from each equivalence class.

We know nothing about the elements of this set. Is 1/2 in it? We don't know, only that it contains exactly one rational (proof by reader). Is pi in it? I have no idea. The only thing I know about this set is that it exists. That's the classic example of pure mathematical existence. It exists, but not only can't its elements be computed, they can't even be identified by ZF. All we know is that the set exists.

$V$ by the way stands for the Vitali set, named after Guiseppe Vitali, who discovered this example in 1905.

It turns out that this set is nonmeasurable. There is no sensible way to assign it a length, as we can with intervals or complicated combinations of intervals of reals. Yet if we ban the axiom of choice, it's consistent that the real numbers are a countable union of countable sets. This would destroy the foundation of modern probability theory and everything that sits above it (statistical mechanics, quantum field theory, sociology, the state lottery, etc.)

I'm sure the constructivists have some workarounds but I gather they sometimes adopt weak forms of choice, because they need to. So the constructivists aren't so pure after all!


So to sum up, the next thing past computability is ZF, which already gives you sets that are arguably not computable (depending on who's arguing). Then AC gives you sets that are not only noncomputable, but beyond even the reach of ZF.

Then of course there are all the large cardinal axioms ... it's turtles all the way up!

This would destroy the foundation of modern probability theory and everything that sits above it (statistical mechanics, quantum field theory, sociology, the state lottery, etc.) — fishfry

Why???
What part of probability theory is inconsistent with the negation of axiom of choice?

Here's an extract from https://en.wikipedia.org/wiki/Probability_theory ( Idon't have time to fix formatting of formulas now)":

Modern definition: The modern definition starts with a finite or countable set called the sample space, which relates to the set of all possible outcomes in classical sense, denoted by {\displaystyle \Omega } \Omega . It is then assumed that for each element {\displaystyle x\in \Omega \,} x\in \Omega \,, an intrinsic "probability" value {\displaystyle f(x)\,} f(x)\, is attached, which satisfies the following properties:

{\displaystyle f(x)\in [0,1]{\mbox{ for all }}x\in \Omega \,;} f(x)\in [0,1]{\mbox{ for all }}x\in \Omega \,;
{\displaystyle \sum _{x\in \Omega }f(x)=1\,.} \sum _{x\in \Omega }f(x)=1\,.

The constructive reals are Dedekind complete but not Cauchy complete
— fishfry

Hmm.. I am sorry that I have always to disagree with what you say, but in my opinion this is not exactly what that paper says :sad: — Mephist

Ok let me pick up my reply to your earlier post here so I am one post behind you. I am paddling as fast as I can through these murky (to me) constructive waters.

Let's read the abstract: "It is consistent with constructive set theory (...) that the Cauchy reals (...) are not Cauchy complete".

That is exactly equivalent to say this: "It is not possible to prove with constructive set theory (...) that it is not true that the Cauchy reals (...) are not Cauchy complete.": — Mephist

Yes yes I misspoke myself a bit and I understood at the time what it's saying. However I must admit that I don't believe them, which is why I paraphrased them in a way you feel is unfair. I think that the only way they can have a model of the constructive reals that's Cauchy complete is by modifying the definition of a Cauchy sequence along computable lines, that is by constraining the rate of convergence. And that in so doing, they must necessarily omit some sequences that are Cauchy in ZF but not in their computable formulation. This is my strong belief but of course I may well be wrong and that's what I'm trying to figure out.

In other words: They define a Cauchy sequence constructively, that is with a convergence rate that allows them to deduce a computable modulus. Remember the modulus is just the function that inputs $\epsilon$ and outputs a suitable $N$ in the definition of a Cauchy sequence.

Then they define the constructive reals as the completion of all these computable Cauchy sequences; and then they can prove that their reals are Cauchy complete. But it's not the same Cauchy. This is my working thesis for what's going on. If it turns out to be more subtle then I'll learn something.

To say that a proposition is consistent with a theory means that it's not possible to prove that the proposition is false in that theory. It doesn't mean that it's possible to prove that the proposition is true. — Mephist

Yes I understand. Sorry I was deliberately imprecise so as to make my point, leading you to believe I didn't understand what they were saying.

In fact, the proposition "Cauchy reals (...) are not Cauchy complete" cannot be proved with the constructive set theory that he considers. — Mephist

I believe you but I feel that they must be using the restricited definition and not the standard one.

How do I know? Because the axioms of IZF_Ref (the constructive set theory that the paper is speaking about) are provable in ZFC, and the rules of IZF_Ref are the same rules of ZFC without Excluded Middle (here is a good reference for the axioms: https://plato.stanford.edu/entries/set-theory-constructive/axioms-CZF-IZF.html).
Then, all theorems that are provable in IZF_Ref are provable even in ZFC: just use ZFC axioms to prove IZF_Ref axioms, and then apply the same rules as the original theorem (ZFC has all rules of IZF_Ref, then it can be done). — Mephist

Ok. This is my next assignment then. I'll read the SEP article and try to grok IZF a little. I need to understand this point you are making. I don't understand it at the moment so I owe us both a response to this paragraph.

So, if "Cauchy reals (...) are not Cauchy complete" were provable in IZF_Ref, it would be provable even in ZFC. But, as we know, in ZFC this is provably false. — Mephist

Isn't that just because the constructive reals can't see all those ZF-Cauchy sequences that it's leaving out? This MUST be the case. Isn't it?

It's like, if I close my eyes I can prove there are no elephants in the room, even though if I were to open them, I'd see the elephant! The restricted definition of Cauchy sequences in the Italian paper bothers me greatly. It's missing a lot of ZF-Cauchy sequences. Sure it can prove that it doesn't see them. That doesn't prove they're not there, only that the constructivists need to open their eyes!

I must really be missing something deep and basic about constructivism. I hope you can take pity on the struggles of an old timer who had ZFC beaten into me by eminent mathematicians at some of our finest universities.

In fact, some models of IZF_Ref are not Cauchy complete (the two models that he considers) and some other models of IZF_Ref (the standard ZFC reals) are Cauchy complete. — Mephist

Ah ... you are saying that the standard reals are a model of IZF_Ref. That is a very enticing remark. I'll spend some time on this. That's a clue for me to hang some understanding on.

And so, here is a confession: I don't even know what Dedekind completeness is
— fishfry

Dedekind completeness is simpler than Cauchy completeness to formulate in set theory, but practically impossible to use in analysis. — Mephist

Yes I probably shouldn't have confessed to any ignorance, it's just that Dedekind completeness is too trivial to even think about in standard math. If you define the reals as the set of Dedekind cuts then every real is automatically a Dedekind cut. Having done that, they then prove the reals are Cauchy complete and have the least upper bound property. But nobody ever draws the implication chart among these properties because they're all trivially equivalent in ZF. I'd love to get more insight in this area.

Basically, this is the thing: if you build "Dedekind cuts" of rational numbers you obtain the real numbers (this is not part of the theorem, but the definition of real numbers in ZFC), — Mephist

Right, Dedekind completeness is baked in so there's no need to talk about it.

but if you build "Dedekind cuts" of real numbers you obtain again the same real numbers. — Mephist

Yes and a good thing too!

The same thing hapens with Cauchy: taking limits of rationals you obtain reals but taking limits of reals you obtain again reals (the set is closed under the operation of taking limits and forming Dedekind cuts).
A Dedekind cut is simply the partition of an ordered set in two non empty sets that respects the order relation (any element of the first set is smaller than any element of the second set). — Mephist

Yes yes.

and then start to attempt to grok what it means to be Dedekind complete but not Cauchy complete in an intuitionist setting (whatever that means!)
— fishfry

OK. In my opinion, intuitively it means that they can be the same thing as standard ZFC reals, but can even be something very different. — Mephist

Throwing a marshmallow to a drowning man! I still don't see the distinction between Cauchy and Dedekind in the constructive setting.

Simply there are more possible "forms" for the object called "set of real numbers". — Mephist

Ok perhaps this will be more clear when I dive into IZF, which I hadn't heard about till you mentioned it.

And there is even another problem with the definition of convergent Cauchy sequences defined in this article: they are not the sequences of rational numbers (as the standard definition) but sequences of pairs made of a real number plus a function (from page 2: "So a real is taken to be an equivalence class of pairs <X, f>, where X is a Cauchy sequence and f a modulus of convergence). — Mephist

Right. A constructive Cauchy sequence consistes of the sequence, along with a computer program that lets you prove that it is in fact a Cauchy sequence. I can see why a constructivist would care. I just need to understand how they can convince themselves that they're still ZF-Cauchy complete. That's the part that's bothering me.

Wait I think you said that wrong. It's not a sequence of pairs (rational number, modulus function). Rather it's a pair (entire sequence, single modulus function). It's the sequence, plus the function that inputs epsilon and outputs a suitable N.

* Finally I just want to say that with all the back and forth, and I do note that we both tend to the wordy side, this current post of mine represents my latest thinking about everything; and all prior comments are null and void.
— fishfry

OK, I'll not look at you previous posts any more :wink: — Mephist

Not that we haven't hit on a lot of interesting side topics, but we're making a lot of progress talking about Cauchy sequences so I'm happy to focus on that.

Constructivism is not about the rejection or acceptance of actual infinity, but it's about choosing computable functions as a fundamental logic concept (that is implemented the rules of logic), as opposed to the more abstract idea of functions that is implied by the classical axiom of choice.


I believe you responded this to someone else's post but it brings up a question.

You talk about computable functions. Every time I drill down, constructivism turns out to be about computability. But the constructivists seem to regard the computable reals as somewhat different than the constructive reals. One article referred to the constructive reals as the "realization" of the computable reals. Or the other way 'round? Either way the point is that computability is not exactly the same as constructivity. I'd like to understand this.

The other minor point is that you jumped from computability to the axiom of choice, but as I pointed out in my previous post there's an intermediate step. ZF is already noncomputable, even before we get to ZFC. — Mephist

Why???
What part of probability theory is inconsistent with the negation of axiom of choice? — Mephist

Your markup didn't render but no matter. I'm talking about the Kolmogorov axioms:

https://en.wikipedia.org/wiki/Probability_axioms

Here's the argument.

One of the axioms is countable additivity. It says that the measure of a countable disjoint union of sets is equal to the sum of their measures. For example suppose I throw a dart at the unit interval $(0,1)$. What's the probability of hitting a point in $(0, \frac{1}{2})$? It had better be $\frac{1}{2}$, right? Likewise the probability of hitting a point in $(\frac{1}{2}, \frac{3}{4})$ is $\frac{1}{4}$ and so forth.

Now what is the probability of hitting some point in $(0,1)$? It's 1. And we must be able to calculate this as the probability of $(0,\frac{1}{2}) \cup (\frac{1}{2}, \frac{3}{4}) \cup \dots = \frac{1}{2} + \frac{1}{4} + \dots = 1$.

[Endpoints don't matter in this discussion but to be more accurate I should fix up the intervals to be half-closed so I don't leave out any points].

So ok, countable additivity.

Now in the absence of the axiom of choice, there is a model of the reals that is a countable union of countable sets. Every countable set must have measure zero (proof by reader or just ask) and therefore the measure of the reals is zero. That's bad. No more probability theory. The axiom of choice is essential for probability. Of course I'm sure the specialists can work around this in various ways. And I'm sure they'd still run the state lottery.

https://mathoverflow.net/questions/100717/zf-the-reals-are-the-countable-union-of-countable-sets-consistent

But who said that the sets must made of points? Set theory does not say what is a set, only gives a list of axioms that are valid WHATEVER sets you consider.

If you take as sets the sets of finite segments, all sets have a measure and Kolmogorov axioms work perfectly well: zero-length segments will have zero measure and non zero segments will have a non zero measure. Where is the contradiction?

* ZF. We have statements of existence of sets we can't compute. The powerset axiom for example is very powerful. Cantor's theorem is a theorem of ZF so that the powerset of the naturals must be uncountable; yet there are only countably many Turing machines. So most of the subsets of the naturals are noncomputable sets. No axiom of choice is needed for ZF-noncomputability. — fishfry

Power Set in ZF:
∀x∃y∀z[z∈y↔∀w(w∈z→w∈x)]

Power Set in Coq:
Inductive Power_set (A:Ensemble U) : Ensemble (Ensemble U) :=
Definition_of_Power_set :
forall X:Ensemble U, Included U X A -> In (Ensemble U) (Power_set A) X.

The powerset of A is the set of all functions from A to a 2-element set (a subobject classifier in topos theory).

Coq uses inductive types (a generalization of recursive types, such as the one used to define integers in Peano arithmetic) to define infinite data types. In ML Type theory, that does not include inductive types,
it depends if you consider the predicative or impredicative version of the theory (https://ncatlab.org/nlab/show/predicative+mathematics)

In the predicative version of ML Type theory, this is true: to define the set of all subsets you have to use an axiom to define a "recursor function", that is assured to be consistent by the meta theory of the logic, but is still an axiom. So, in that case you are right: there are really 3 levels: finite, inductively definable and non-inductively definable.

This is the same as for the definition of integers: you have to use the induction principle, that is not provable in the predicative version of ML Type theory.

Although in ZF we can enumerate the Turing machines, no such enumeration can be computable! That's because a computable enumeration of TMs would effectively solve the Halting problem, which Turing showed can't be done. — fishfry

Are you sure about this? I think turing machines are simply strings that can be enumerated as integers. This is not the same thing as solving the halting problem.

We know nothing about the elements of this set. Is 1/2 in it? We don't know, only that it contains exactly one rational (proof by reader). — fishfry

If R/Q is the quotient class, 1/2 is contained in only one of it's subclasses: the one that contains all rational numbers.

So to sum up, the next thing past computability is ZF, which already gives you sets that are arguably not computable (depending on who's arguing). Then AC gives you sets that are not only noncomputable, but beyond even the reach of ZF. — fishfry

The sets that you say are not computable, but computable in ZF, are the ones that in type theory are called Inductive types, and correspond to initial algebras in category theory. The simplest example is the set of natural numbers. You say the set of natural numbers is not computable. It's not so simple: an inductive set is not a function, and the recursor on this inductive set is a computable function, because the recursion is done counting down to zero.

And there are even co-recursive sets, that correspond to co-initial algebras in category theory (not sure if the name is correct). Co-inductive functions are not required to terminate, but only to consume data at every step. However, you never get an infinite loop because there are restrictions on how co-inductive functions can be used. So, it's not so easy to define what is "computable" from the point of view of a constructive type theory.

You talk about computable functions. Every time I drill down, constructivism turns out to be about computability. But the constructivists seem to regard the computable reals as somewhat different than the constructive reals. — Mephist

There are too many points, and I have the impression that this discussion doesn't make sense if we don't agree on the definitions of the worlds. So, let me start from the most ambiguous one: what do you mean by "computable reals"? How do you "compute" a number that is not representable as a fraction? I'll wait for this answer before going ahead with the other points, because I really don't know what are the "computable reals".

You quoted yourself there.

Ops... thank you for pointing it out :yikes:

I'll try to answer only to what I think are the most relevant points only, OK?

Wait I think you said that wrong. It's not a sequence of pairs (rational number, modulus function). Rather it's a pair (entire sequence, single modulus function). It's the sequence, plus the function that inputs epsilon and outputs a suitable N. — fishfry

Yes, you are right.

Ah ... you are saying that the standard reals are a model of C. That is a very enticing remark. I'll spend some time on this. That's a clue for me to hang some understanding on. — fishfry

Yes, exactly!

But I have to tell you that in my opinion the road that you've chosen to learn about constructive mathematics is the most difficult that you could choose. I didn't know what IZF_Ref is, I had to look for the definition to understand the paper that you pointed out, and in my opinion IZF_Ref is not relevant at all, and the axiomatization of real numbers that he is speaking about is even less relevant: you can choose another slightly different axiomatization and you'll get different results. I'll tell you more: I don't think that Cauchy convergence is in some "objective" way weaker or stronger than Dedekind convergence (I can be wrong on this, I am not sure at all!), as you seem to deduce from this paper: I think that if you defined real numbers in ZFC using Cauchy convergence, then Dedekind convergence would become not provable in IZF_Ref.

In my opinion ZFC, or ZF, makes sense only in first order logic (of course!), and intuitionistic logic makes the most sense in the context of type theory. But of course you can choose whatever random combination of axioms and rules, and find their implications, but I doubt that in this way you can discover something meaningful about what the "real" real numbers are...

Isn't that just because the constructive reals can't see all those ZF-Cauchy sequences that it's leaving out? This MUST be the case. Isn't it? — fishfry

I don't know...
If you consider a weaker logic (taking out axioms) you get more possible models, but more abstract.
Consider this question: why modules don't have a base? Is it because they can't see all those inverse functions of multiplication that vector spaces see? Well, yes! But does it mean that modules are vector spaces when you close your eyes to not see the inverse of multiplication?
I know the objection to this argument: vector spaces and modules are abstract algebraic structures. Real numbers are a concrete unique object, because there is only one model of real numbers. Well, there is only one model in ZFC, but there are a lot of models of ZFC itself! Consider the Yoneda lemma in category theory built on top of ZFC: in every reach enough category (let's say in every topos) you can build a different real number object (https://ncatlab.org/nlab/show/real+numbers+object), and using the Yoneda lemma you can map them to different sub-categories of sets. All the theorems of real numbers will remain valid in all categories that have a real-number object, but if you consider a specific category there will be properties that are "visible" only in that category, and not in the standard real numbers.

You talk about computable functions. Every time I drill down, constructivism turns out to be about computability. But the constructivists seem to regard the computable reals as somewhat different than the constructive reals. — Mephist

Basically, the point is that building proofs in intuitionistic logic is equivalent (it's really the same thing) to building computable functions: there is a one-to one correspondence between intuitionistic proofs and terms of lambda calculus (sorry, lambda calculus again...). This is really a very simple and practical thing, but I don't know why all explanations that I am able to find on the web are extremely abstract and complicated!

If you take as sets the sets of finite segments, all sets have a measure and Kolmogorov axioms work perfectly well: zero-length segments will have zero measure and non zero segments will have a non zero measure. Where is the contradiction? — Mephist

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?

Power Set in ZF:
∀x∃y∀z[z∈y↔∀w(w∈z→w∈x)]

Power Set in Coq:
Inductive Power_set (A:Ensemble U) : Ensemble (Ensemble U) :=
Definition_of_Power_set : — Mephist

You totally missed or ignored my point. You said that (in ZF presumably) we have computable sets and then we can introduce the axiom of choice to get noncomputable sets. You said it twice in two different posts. I pointed out that there is an intermediate level, that of noncomputable sets in ZF. My remark was minor, just correcting a minor error. Yes?

Although in ZF we can enumerate the Turing machines, no such enumeration can be computable! That's because a computable enumeration of TMs would effectively solve the Halting problem, which Turing showed can't be done.
— fishfry

Are you sure about this? I think turing machines are simply strings that can be enumerated as integers. This is not the same thing as solving the halting problem. — Mephist

I see your point. I confused that with the fact that there is no computable enumeration of the computable numbers. To enumerate the computable numbers you have to be able to enumerate the TMs that halt. That you can't (computably) do.

I believe that preserves my larger point, which is that a constructivist might say that I can't constructively prove that there are only countably many computable numbers, because I can't computably enumerate them.

The sets that you say are not computable, but computable in ZF, are the ones that in type theory are called Inductive types, and correspond to initial algebras in category theory. — Mephist

I did not say there are any sets that are not computable but computable in ZF.

The simplest example is the set of natural numbers. You say the set of natural numbers is not computable. — Mephist

I neither said nor believe such a thing. Are you saying that's true?

It's not so simple: an inductive set is not a function, and the recursor on this inductive set is a computable function, because the recursion is done counting down to zero. — Mephist

You lost me a while back in this post.

And there are even co-recursive sets, that correspond to co-initial algebras in category theory (not sure if the name is correct). Co-inductive functions are not required to terminate, but only to consume data at every step. However, you never get an infinite loop because there are restrictions on how co-inductive functions can be used. So, it's not so easy to define what is "computable" from the point of view of a constructive type theory. — Mephist

This does not seem to bear on the extremely trivial point I made in correcting an error you made twice. I reiterate my original remarks and don't understand your two off-point responses. I'm sure I must be missing something vital but I thought I made a very trivial point whose importance was only that you committed the same minor error twice and I wanted to clarify the issue. Which clearly I didn't.

There are too many points, and I have the impression that this discussion doesn't make sense if we don't agree on the definitions of the worlds. So, let me start from the most ambiguous one: what do you mean by "computable reals"? How do you "compute" a number that is not representable as a fraction? I'll wait for this answer before going ahead with the other points, because I really don't know what are the "computable reals". — Mephist

Ah you don't know what are the computable reals! Why didn't you say so about ten or twenty posts ago when I first mentioned them?

The definition is due to Turing, whose famous 1936 paper is called, ON COMPUTABLE NUMBERS, WITH AN APPLICATION TO THE ENTSCHEIDUNGSPROBLEM

(caps in original).

https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf

A computable real is a real number with the property that there is a TM that inputs a positive integer n and halts, outputting the n-th decimal digit of the number (or binary, same thing). With this definition I hope you will agree that pi is computable (earlier you thought it wasn't) and that Chaitin's Omega isn't (since its computability would amount to solving the halting problem).

An equivalent definition is that given epsilon there is a TM that cranks out a rational approximation to the number within epsilon.

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.

I have made or referenced this argument probably a dozen times already, so if you didn't know what I meant, I can certainly see why you don't take my point about the constructive Cauchy sequences.

But I have to tell you that in my opinion the road that you've chosen to learn about constructive mathematics is the most difficult that you could choose. — Mephist

But I m not choosing to learn constructive math. How we got onto this was that I made the rather trivial point that the standard reals are the Goldilocks model of the reals with respect to Cauchy completeness. 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.

I thought this was a very harmless, lighthearted observation. You replied by claiming that the constructive reals are Cauchy complete. You can only prove that (as far as I can tell) by changing the definition of a Cauchy sequence to include only the computably Cauchy sequences, then defining the constructive reals as the limits of all the computably Cauchy sequences. This is what we've been discussing for the last many posts.

But my intention was not to learn constructive math. There's too much standard math I'm interested in and that keeps me busy. My point was to challenge your claim that the constructive reals could ever legitimately be called Cauchy complete. That's what we've been talking about.

I had to look for the definition to understand the paper that you pointed out, — Mephist

You are the one who pointed out that paper to me! Didn't you? I really thought so.

In my opinion ZFC, or ZF, makes sense only in first order logic (of course!), and intuitionistic logic makes the most sense in the context of type theory. But of course you can choose whatever random combination of axioms and rules, and find their implications, but I doubt that in this way you can discover something meaningful about what the "real" real numbers are... — Mephist

I can't comment on this. But if you haven't understood all along what a computable real is, and that there are only countably many of them, and that the standard reals are not countable, then you have not understood, let alone challenged, my argument.

Which is: The constructive reals can not legitimately be called Cauchy complete. There aren't enough of them to do the job.

Consider this question: why modules don't have a base? Is it because they can't see all those inverse functions of multiplication that vector spaces see? Well, yes! But does it mean that modules are vector spaces when you close your eyes to not the inverse of multiplication? — Mephist

Pretty funny. The statement "Every vector space has a basis" is logically equivalent to the full axiom of choice. So every time I give you a vector space and you say, "Well of course it has a basis," you are asserting AC.

To answer your question directly, I suppose that if someone asked me, why don't modules always have a basis, I suppose I'd say, "Some modules aren't free." Which doesn't answer the question, since a free module is just a module that has a basis. But even a module with a basis is not necessarily a vector space, so I think your analogy is a little off. The integers are a free module over the integers, with a basis, but are not a vector space.

But why do all vector spaces have a basis? It's because of the axiom of choice! Without choice, there's a vector space that has no basis. Consider how strange such a thing must be, before you casually abandon choice.

Real numbers are a concrete unique object, because there is only one model of real numbers. — Mephist

I said no such thing and of course believe no such thing.

Basically, the point is that building proofs in intuitionistic logic is equivalent (it's really the same thing) to building computable functions: there is a one-to one correspondence between intuitionistic proofs and terms of lambda calculus (sorry, lambda calculus again...). This is really a very simple and practical thing, but I don't know why all explanations that I am able to find on the web are extremely abstract and complicated! — Mephist

Is this the Curry-Howard correspondence?

Ok I believe I've caught up to your series of posts replying to my most recent of the other day. I still owe you a response to the second long post you replied to me a few days ago.

But wait let's stop here for a moment. If you didn't know what I meant by a computable real, then let's go back to the basic argument. The computable reals can't be Cauchy complete because there are far too few of them to plug all the holes with only computably Cauchy sequences as defined in the Italian paper.

And again, I only mentioned it to kind of wrap up our original discussion. Saying in effect that, "Ok constructivism is all the rage and there's a ton of stuff I'll never know, but the standard reals are the only Cauchy complete model of the reals." That was my original point. If you haven't known what I meant by a computable real all along, this has been a vacuous discussion with an empty intersection.

Also of course there are many (many!) exotic models of ZFC, each with their own version of the reals. That doesn't bear on my simple and basic point.

Wow!!! I knew there was something that missed! :starstruck:

Sorry, but I was thinking that you used the term "computable reals" in an intuitive way, without a concrete definition!
Yes, now I think a lot of what you said starts to make more sense! :smile:

I did study Turing machines a long time ago, but I didn't remember about this definition at all!

OK, well, I am at work now.. :razz:

I'll read again what you write later, but now I think it's going to be much easier to agree!

In the end, math is not an opinion, right? :smile: :smile: :smile: