Completeness. Finally, the completeness property for the field of the real numbers is postulated asking the existence of the limit of any Cauchy sequence with an exponential convergency rate:
I promise that I'll answer very clearly to all your questions, but I am going to need some time (probably some days), even because I have a lot to do at work these days. — Mephist
By the way, just a quick note: as you said they have a completeness AXIOM. Not a completeness theorem. It means that completeness is not provable nor refutable! — Mephist
I'll rephrase it: if you remove the completeness axiom (consider the same exact theory without that axiom), Cauchy completeness is not provable nor refutable. — Mephist
Its an interesting piece of math, but it is wrong at the same time - its all based on Grandi's series evaluating to 1/2 which is wrong - Grandi's series does not converge and so it limit is undefined. — Devans99
That validates my earlier point that among all models of the real numbers, the standard (ZF) reals are privileged by virtue of being Cauchy complete. — fishfry
The constructivists agree! They are trying to develop a context in which they can say that the constructive reals are complete.
[From now on complete means Cauchy complete and not any other mathematical meaning of complete]. — fishfry
* How can the constructive reals be complete? If they are complete they must contain many noncomputable reals. How can that be regarded as constructive? — fishfry
* Does their formulation actually imply standard Cauchy completeness? — fishfry
* In what sense is their formulation constructive? I gather this may have something to do with the rate of convergence, in which case perhaps the theory of computational complexity may come into play. Big-O, P = NP and all that. I'm a big fan of Scott Aaronson's site. — fishfry
* And if the constructive reals are Cauchy complete, they must contain a lot of noncomputable real numbers. How can that be called constructive? — fishfry
OK, I'll stop it here because it's just become too long and I am only at the first question. — Mephist
The problem is that sets are defined axiomatically in ZFC. So, IF sets make sense (are not contradictory), then real numbers make sense. But IT'S NOT GUARANTEED THAT THE SETS DEFINED IN ZFC MAKE SENSE IN SOME CONCRETE MODEL. — Mephist
[ I know, I wanted to use formulas to be more precise and at the end I didn't do it (mostly for lack of time). — Mephist
What do you mean by "the standard (ZF) reals"? — Mephist
Maybe I am saying obvious things, but at risk of being pedantic, I prefer to make everything clear about some basic facts. (That's one of the reasons why I like computer-based formal systems: everything has to be declared. No implicit assumptions!) — Mephist
Fakt N.1. ZFC is NOT an axiomatic theory of real numbers. ZFC is an axiomatic theory of SETS. — Mephist
In fact, in first order logic all functions and relations can be applied to all variables, and there cannot be some functions (like addition and multiplication) applied only to numbers and other functions (like union and interception) applied only to sets. In ZFC, all variables are interpreted as SETS. — Mephist
Fakt N.2. The standard representation of real numbers in ZFC is the following: (https://www.quora.com/How-is-the-set-of-real-numbers-constructed-by-using-the-axiomatic-set-theory-ZFC-set-theory)
- Natural numbers are sets
- Integers are pairs of natural numbers (a pair is a function with two arguments)
- Rational numbers are pairs of integers
- Real numbers are sets of rational numbers — Mephist
Here's the definition of real numbers in ZFC in Bourbaki: https://math.stackexchange.com/questions/2210592/in-which-volume-chapter-does-bourbaki-define-the-real-numbers — Mephist
Fakt N.3. There is a more "usable" definition of real numbers given by Tarski (usable in the sense that the demonstrations are simpler): https://en.wikipedia.org/wiki/Tarski%27s_axiomatization_of_the_reals — Mephist
- Tarski's real numbers are defined axiomatically, — Mephist
and make use of set relations (similar to the ones of ZFC). But they are not based on first order logic. — Mephist
The difference is that it is allowed the quantification on all subsets of a given set (and not only on all elements of the universe), but the meaning of the subset relations is encoded in the rules of logic, and not given axiomatically.
The use of a second-order logic is essential to be able to express the property of being Dedekind-complete (Axiom 3) — Mephist
So, going back to what you wrote:
The constructivists agree! They are trying to develop a context in which they can say that the constructive reals are complete. — Mephist
[From now on complete means Cauchy complete and not any other mathematical meaning of complete].
— fishfry
OK, let's check the definition of being "Cauchy complete": — Mephist
"Cauchy completeness is the statement that every Cauchy sequence of real numbers converges." (https://en.wikipedia.org/wiki/Completeness_of_the_real_numbers) — Mephist
What's a Cauchy sequence? "a Cauchy sequence (French pronunciation: [koʃi]; English: /ˈkoʊʃiː/ KOH-shee), named after Augustin-Louis Cauchy, is a sequence whose elements become arbitrarily close to each other as the sequence progresses." (https://en.wikipedia.org/wiki/Cauchy_sequence) — Mephist
As you said, in the Coq formalization of real numbers there is this axiom:
completeness ∀f : N → R. ∃x ∈ R.(∀n ∈ N. near(f(n), f(n + 1), n + 1)) →(∀m ∈ N. near(f(m), x, m)) — Mephist
In the logic of Coq, "completeness" IS A FUNCTION, at the same way as "near" is a function and "+" is a function. — Mephist
The function "completeness" takes as input a sequence of real numbers "f" and returns two things:
1. a real number "x" -- let's call it "first_part"
2. a proof that IF "f" is a Cauchy sequence, THEN "x" is the limit of "f" -- let's call it "second_part" — Mephist
So, for every sequence of real numbers "f", the term "(completeness f).first_part" is a real number. If I have a proof that "f" is a Cauchy sequence, then I can use "(completeness f).second_part" (that is a proof) to obtain a proof that the Cauchy sequence "f" converges to the real number "completeness f". — Mephist
That's all I need to get a COMPLETE field of real numbers: for all sequences "f", if you have a proof that "f" is a Cauchy sequence, you can produce a proof that "f" is convergent to the real number "(completeness f).first_part". — Mephist
However, you can't explicitly compute it, because axioms are functions that cannot be reduced (https://stackoverflow.com/questions/34140819/lambda-calculus-reduction-steps) — Mephist
Then, IF you ASSUME that you can get a real number for every Cauchy sequence, THEN you can prove that there is a real number for every Cauchy sequence. Magic! :-) — Mephist
* How can the constructive reals be complete? If they are complete they must contain many noncomputable reals. How can that be regarded as constructive?
— fishfry
Yes, that's the same old question that I thought I just answered many times... :-) — Mephist
Here's the "computation" of pi:
Definition my_sequence := func n -> sum of 1/n bla bla...
Definition pi := "(completeness my_sequence).first_part"
Here's the proof that my_sequence converges to pi:
1. proof that my_sequence is a Cauchy sequence (let's call this proof my_proof)
2. from "(completeness my_sequence).second_part" (the proof that IF "f" is a Cauchy sequence, THEN "x" is the limit of "f") and "my_proof" (the proof that my_sequence is a Cauchy sequence) I get a proof that "x" is the limit of "f"
(by applying the rule of cut)
I "computed" the noncomputable real number pi, and the result is "(completeness "func n -> sum of 1/n bla bla...").first_part — Mephist
If "completeness" were a theorem instead of an axiom, I should have provided the implementation of the program that computes the function "completeness". But an axiom is treated as an "external function" of a programming language: — Mephist
I ASSUME to have some external machine that is able to compute the function "completeness", but I don't have to show how that machine works. That's cheating! :-) — Mephist
However, remember that this is an AXIOMATIC DEFINITION of what real numbers are, NOT A MODEL of real numbers. — Mephist
Axiomatic definitions, in whatever logic (intuitionistic or not), are not guaranteed to be consistent: you have to be careful on what axioms you assume to be true.
So, in principle it's not guaranteed that the real numbers that you defined make sense in some concrete model. — Mephist
And that is true even for Tarski's real numbers, that are described using classical (non intuitionistic) logic. — Mephist
Instead, this is not true for the description of real numbers in ZFC. In that case, real numbers are a model built from sets, and completeness is PROVED as a theorem, and not assumed as an axiom. Real numbers are concrete objects made of sets! — Mephist
The problem is that sets are defined axiomatically in ZFC. — Mephist
So, IF sets make sense (are not contradictory), then real numbers make sense. But IT'S NOT GUARANTEED THAT THE SETS DEFINED IN ZFC MAKE SENSE IN SOME CONCRETE MODEL. — Mephist
So, again, to be sure about the sets of ZFC you should define them as a model in some other axiomatic theory that you trust more than ZFC. Or you could use a FINITE MODEL: in a finite model you can verify a proposition "by hand" (as one of my favourite professors of analysis used to say) simply inspecting the model! — Mephist
But, obviously, there is no finite model that verifies all the axioms of ZFC. — Mephist
The best that you can do is to verify ZFC axioms on a model built from natural numbers. But natural numbers are NOT a finite model (you cannot check theorems on natural numbers "by hand"). And, as Godel proved, there is no axiomatic definition of natural numbers, in any formal logic, that is guaranteed to make sense. — Mephist
OK, I'll stop it here because it's just become too long and I am only at the first question. — Mephist
* Does their formulation actually imply standard Cauchy completeness?
— fishfry
Let me rephrase this question: "if a given Cauchy sequence has a limit in intuitionistic logic, does it have a limit even in ZFC?"
The answer is YES, because the axioms of intuitionistic logic correspond to theorems in ZFC, and the rules of intuitionistic logic are just a subset of the rules of classical logic. So, if you can prove that a given sequence is convergent in intuitionistic logic, you can use EXACTLY THE SAME PROOF in classical logic. — Mephist
You can map any proposition of one logic to a corresponding proposition of the other logic and every rule of one logic to a corresponding rule of the other logic. — Mephist
It doesn't matter what's the interpretation of the rules: if the rules are the same (or a subset of them), whatever you can prove in intuitionistic logic you can prove even in classical logic: just apply the same rules! — Mephist
* In what sense is their formulation constructive? I gather this may have something to do with the rate of convergence, in which case perhaps the theory of computational complexity may come into play. Big-O, P = NP and all that. I'm a big fan of Scott Aaronson's site.
— fishfry
Nothing to do with the rate of convergence! — Mephist
Constructive, in the particular interpretation of Coq, means that every object (every real number in this case) can be built using recursive functions ( except axioms... :-) ) — Mephist
* And if the constructive reals are Cauchy complete, they must contain a lot of noncomputable real numbers. How can that be called constructive?
— fishfry
This sentence has a hidden presupposition: that real numbers are a concrete set of objects and you can check if a given noncomputable real number is present or not. — Mephist
This is not true: any model of real numbers is ultimately based on an axiomatic theory that cannot be checked "by hand". — Mephist
[ I know, I wanted to use formulas to be more precise and at the end I didn't do it (mostly for lack of time). — Mephist
And probably I still wasn't able to be clear enough on what I meant. — Mephist
So, please repeat the questions that I wasn't able to be clear about, or where you thing that I am wrong. Maybe in that way will be easier to arrive at some conclusion — Mephist
Ok. Question: How can any model of the reals built on constructive principles be Cauchy complete? — fishfry
Yes that's the one direction. But it's the other direction that's harder. If a sequence is Cauchy in standard math, is it Cauchy in intuitionist math? That's a good question and I'm sure the constructivists have an answer, I just don't happen to know what it is. — fishfry
Here is where your post totally went off the rails. As I said? I said nothing of the sort! I quoted the definition in the Italian paper. — fishfry
OK! as you wish :smile:Read this first, don't waste time slogging through my other posts. This is the heart of the matter. — fishfry
* First, I must say that as much as I've been aggressively rejecting your remarks about Coq, that is only because I'm not yet ready to receive the information. First I need to grok the essence of this constructiveness business; and I have found that Cauchy completeness is a bridge from math that I know, to constructive math that I'm trying to understand. So I'm "On a Mission" and can't be distracted. — fishfry
* On the other hand, if and when the day comes that I am ready to learn about Coq -- which I confess I've been interested in from afar since I started watching Voevodsky videos -- I will start at the beginning of this thread and read every word you've written and follow every link! Because you are giving a master class in how someone can think about Coq in the framework of constructive math. — fishfry
OK, let's focus on Cauchy completeness.* And what is that thing? It's Cauchy completeness. — fishfry
The constructive reals are Dedekind complete but not Cauchy complete — fishfry
And so, here is a confession: I don't even know what Dedekind completeness is — fishfry
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
* 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
That's what all the mathematicians say. — tim wood
I believe there is constructivism - a minority view in maths - which rejects actual infinity.
I believe the vast majority of mathematicians accept actual infinity as a number - see the transfinite numbers from set theory. — Devans99
Transfinite numbers are not infinity. Infinity is not a transfinite number. — tim wood
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.