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
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
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
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
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
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
I can try to interpret it as "a sequence is Cauchy in the theory of real numbers of the Italian paper". — Mephist
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
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 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
[ 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
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
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
in the absence of evidence to the contrary — Mark Dennis
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
Because in ZFC you can define non computable functions by using the axiom of choice, that is not available in constructive mathematics. — Mephist
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
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
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
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
In fact, the proposition "Cauchy reals (...) are not Cauchy complete" cannot be proved with the constructive set theory that he considers. — Mephist
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
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
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
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
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
but if you build "Dedekind cuts" of real numbers you obtain again the same real numbers. — Mephist
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
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
Simply there are more possible "forms" for the object called "set of real numbers". — Mephist
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
* 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
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
* 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
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
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
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
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
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
I don't know...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
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
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
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
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
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
The simplest example is the set of natural numbers. You say the set of natural numbers is not computable. — Mephist
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
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
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
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
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
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
Real numbers are a concrete unique object, because there is only one model of real numbers. — 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! — Mephist
Get involved in philosophical discussions about knowledge, truth, language, consciousness, science, politics, religion, logic and mathematics, art, history, and lots more. No ads, no clutter, and very little agreement — just fascinating conversations.