You should watch the youtube proof of $1+2+3+4+...= -1/12$.

The above series is called divergent meaning it tends towards infinity. Yet using the Grandi series we can prove it equals a finite value $-1/12$. In the youtube video (numberphile?) it's mentioned that some equations in physics involving $1+2+3+4+...$ can yield ''true'' results using $\frac{-1}{12}$. Does this agree with your views that infinity isn't actual or that there are no real infinities?

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. Once you start playing around with something that is undefined, you get all sorts of nonsense results coming out. Actual infinity is undefined IMO and playing around with it leads to nonsense results (Hilbert's Hotel etc).

I'm going to take a look at this to understand it better:

https://www.youtube.com/watch?v=YuIIjLr6vUA

@Mephist

I had an insight. A formula in the Italian paper is the link between what I know and what we're trying to understand.

That's this paper:

https://users.dimi.uniud.it/~pietro.digianantonio/papers/copy_pdf/RealsAxioms.pdf

It's written for specialists and I didn't relate to most of it. They're proposing axioms for the constructive reals that they claim have some benefits over other axiomitizations.

One thing caught my eye. They have a Completeness axiom.

Before this I had no idea constructivists were concerned with Cauchy completeness, but it turns out they are. 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.


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

Here's their axiom verbatim. Slight grammatical inaccuracies as in the original, as well as some mathematical ambiguity that's not important at the moment].

Completeness. Finally, the completeness property for the field of the real numbers is postulated asking the existence of the limit of any Cauchy sequence $\langle s_n \rangle_{n \in \mathbb N}$ with an exponential convergency rate:

$\forall n \in \mathbb N, | s_n - s_{n+1} |\lt 2^{-(n + 1)}$

After learning that constructivists care about completeness, my second surprise is that this axiom appears noticeably weaker than standard Cauchy completeness. Indeed in their very next paragraph they say:

" our axiom could appear weak at a first glance."

So we are on the same page. This is encouraging. Also encouraging is that that's the kind of math I understand! I can compare their definition to standard Cauchy completeness and try to figure out if they're the same or not.

Now, three points:

* How can the constructive reals be complete? If they are complete they must contain many noncomputable reals. How can that be regarded as constructive?

* Does their formulation actually imply standard Cauchy completeness? Or if not, are they reasoning in some kind of alternative context that allows them to claim Cauchy completeness in a way that standard math wouldn't?

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

So that's it. To sum up:

* Constructivists do care about Cauchy completeness.

* They have a funny way of expressing it that at first glance appears weaker than standard Cauchy completeness, but that they claim gets the job done.

* Even if it does, in what way does it count as constructive?

* And if the constructive reals are Cauchy complete, they must contain a lot of noncomputable real numbers. How can that be called constructive?

Hi @fishfry!

Sorry, but you have to give me some time to learn about how to write symbols on this site, and I have not much time for this right now. Otherwise we keep speaking using words without meaning, never reaching any conclusion.

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.

not trying to be rude but write out the formula on a piece of paper and take a picture of it with your phone and post it to this site that way. There are other ways too. Thought this might help. I assume everyone has a phone these days and i know you you have access to a computer.

\

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

No worries. Working out if their definition implies Cauchy is something I can take a run at. Math markup's not hard but it does have a bit of a learning curve. Lots of info online.

You can also copy/paste from a site like https://math.typeit.org/ but of course that's not as good as learning a little $\LaTeX$.

Also I like this site https://www.codecogs.com/latex/eqneditor.php which lets you enter a string of markup to see what it looks like.

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!

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

Not sure what you mean.

Suppose I have an axiom system that includes axiom X. Then X is a theorem with a one line proof: "X". Any axiom is a theorem with a one-line proof. The question is what their completeness axiom means, and in what context.

Note that Cauchy completeness, in the form of the least upper bound principle, is an axiom of the standard real numbers. It can't be proven without an axiom. The rationals are an ordered field that's not complete. We need an axiom to ensure completeness.

Of course Cauchy completeness is a provable theorem from ZF via the standard constructions like Dedekind cuts and equivalence classes of Cauchy sequences. But the article is an axiomitization and not a construction.

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

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

Sure, just like the ordered field axioms in ZF. If you omit completeness you get the rationals. If you toss in completeness you get the reals. I understand what you're saying but I'm missing your point. The paper gives an axiomitization. If completeness were provable without an axiom, they wouldn't need an axiom. That's clear.

In ZFC a Cauchy succession is a definition, and completeness is a theorem, not an axiom.

P.S. OK, sorry. They have Dedekind as an axiom, that is equivalent in ZFC, so it's the same thing. My mistake! Just ignore what I said... :confused:

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

How do you know it's wrong?

First of all the ''proof'' seems to have been reviewed and accepted by mathematicians. Second the result is useful in physics.

The series is not convergent according to the definition of convergent:

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

So the series has no sum. This article explains it quite well:

https://plus.maths.org/content/infinity-or-just-112

As far as the physics is concerned it is something called the Casimir effect that is associated with a finite sum of a divergent series. I don't know the maths or physics well enough, but from a layman's perspective, I think some of the maths in QM looks suspect. There is an alternative explanation for the Casimir effect that does not involve questionable maths:

https://en.wikipedia.org/wiki/Casimir_effect#Relativistic_van_der_Waals_force

Or it could be that the physicists have the precise maths wrong but it is close enough to being right that with some questionable manipulations, it gives results that agree with experiment. QM maybe is not quite the finished article.

Thanks for the info.

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

What do you mean by "the standard (ZF) reals"?
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!)

Fakt N.1. ZFC is NOT an axiomatic theory of real numbers. ZFC is an axiomatic theory of SETS.
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.

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

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

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

- Tarski's real numbers are defined axiomatically, and make use of set relations (similar to the ones of ZFC). But they are not based on first order logic.
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)


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.

[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":
"Cauchy completeness is the statement that every Cauchy sequence of real numbers converges." (https://en.wikipedia.org/wiki/Completeness_of_the_real_numbers)

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)

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

In the logic of Coq, "completeness" IS A FUNCTION, at the same way as "near" is a function and "+" is a function.

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"

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

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

However, you can't explicitly compute it, because axioms are functions that cannot be reduced (https://stackoverflow.com/questions/34140819/lambda-calculus-reduction-steps)

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! :-)

* 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... :-)

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

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:
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! :-)

However, remember that this is an AXIOMATIC DEFINITION of what real numbers are, NOT A MODEL of real numbers.
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.

And that is true even for Tarski's real numbers, that are described using classical (non intuitionistic) logic.

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!

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.

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!

But, obviously, there is no finite model that verifies all the axioms of ZFC. 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.

OK, I'll stop it here because it's just become too long and I am only at the first question.

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

* 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! 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... :-) )

* 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. This is not true: any model of real numbers is ultimately based on an axiomatic theory that cannot be checked "by hand".

[ 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). And probably I still wasn't able to be clear enough on what I meant. 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 ]

OK, I'll stop it here because it's just become too long and I am only at the first question. — Mephist

I just wanted to jump in quickly and tell you that your lengthy post (1) mostly consisted of things I already know; (2) completely failed to address anything I wrote; and (3) well I haven't time for all my other concerns. Honestly, and I say this in the context of finding most of our conversation very interesting and valuable, but this post said nothing at all to me as you completely ignored everything I wrote.

I'll get to a full reply later. For now please note that my early post specifically focuses on the Italian paper. So even your invocation of the constructive completeness axiom shows that you didn't read or understand a word I wrote. The axiom you gave is very different than the one in the Italian paper. The axiom in the Italian paper is very important to me because it's written in traditional math language and I can work with it mathematically.

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

Funny that the part you shouted in upper case directly contradicts ‎Gödel's completeness theorem. An axiomatic system is complete if and only if it has a model. So if there IS a concrete model, then the sets DO make sense.

https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem

Finally, you consistently misunderstand the relationship between axiomatic models and constructions. For example the axioms for the real numbers (ordered field plus least upper bound) completely characterize the real numbers. The Dedekind cut construction, on the other hand, explicitly constructs a model of these axioms within ZF.

The axiomatic definition is sufficient to do everything one needs to do with the real numbers. Its only drawback is that it suffers from the following refutation: "Oh yeah? How do we know there EVEN IS such a thing?" That's why once in one's life, one is shown a specific construction such as Dedekind cuts or equivalence classes of Cauchy sequences. Then one forgets the messy construction(s) and works forever after with the axiomatic definition.

When I have time later on I'll comment paragraph by paragraph, but frankly at least 2/3 of your exposition was just a recapitulation of what every undergrad math major knows; and the rest completely ignored my specific comments on the Italian paper, which is the ONLY thing I'm talking about at this point.

By the way I have proven to my own satisfaction that the the characterization of a Cauchy sequence in the Italian paper does imply standard Cauchy sequences. I still have to write up the proof, which has a number of interesting points regarding constructive thinking. The next step is to find a proof or counterexample of the other direction, that standard Cauchy implies Italian paper Cauchy.

Finally my tl;dr: At this point I am ONLY talking about the completeness axiom in the Italian paper, because it has the property of being written in standard math language (ie no undefined "near" function, no reference to Coq, etc.) Your pointedly ignoring my entire post is depressing to me. We can't have a conversation if I write, "Here is what the Italian paper says, I have the following questions," and you reply with a lengthy recapitulation of an undergrad class in real analysis followed by a discussion of Coq completely unrelated to what I wrote.

[ 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

Well worth your time to learn. The SINGLE most important and magic development in math from the time I was in grad school to today, is LaTeX math markup and its web cousin MathJax. Back in my time the math departments had staffs of secretaries to type up the professors' papers, and the students were stuck with writing longhand. The true impact of computers on math isn't just Coq, it's $\LaTeX$!

What do you mean by "the standard (ZF) reals"? — Mephist

Ok, here's my detailed response to your post. But I fear we're diverging, since right now I'm 100% focused on understanding the completeness axiom from the Italian paper. The reason being that it's written in standard mathematical style so I can work with it.

The standard (ZF) reals are the real numbers as understood in mainstream math, say at the level of an undergrad math major. Either axiomatically, as a Cauchy complete ordered field; or by construction as equivalence classes of Cauchy sequences or Dedekind cuts. There are other equivalent constructions as well.

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

There are no implicit assumptions in ZFC. I don't understand why you think there are.

Fakt N.1. ZFC is NOT an axiomatic theory of real numbers. ZFC is an axiomatic theory of SETS. — Mephist

You're right. You're stating the obvious. But ok.

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

Yes ok. Why are you spelling fact as fakt?

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

Perfectly familiar to undergrad math majors. It's a nice theory in fact, served the 20th century well.

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

Not sure what is the point of this link.

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

All of modern math as well as physics and all other physical sciences find the standard definition perfectly serviceable, to the extent they care about it at all. Not following your point.

- Tarski's real numbers are defined axiomatically, — Mephist

As are the standard reals, as a complete ordered field.

and make use of set relations (similar to the ones of ZFC). But they are not based on first order logic. — Mephist

Nor are the standard reals, as the least upper bound property is second order.

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

We're in perfect agreement on all this. Except for my puzzlement as why you're mentioning it.

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

Yes. This was my great recent revelation. I always thought the constructive reals were the computable reals, but as this is only vaguely true (very murky area here), apparently the constructive reals are claimed to be complete in some sense.

[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

I only mentioned that since I don't want to keep writing Cauchy complete.

"Cauchy completeness is the statement that every Cauchy sequence of real numbers converges." (https://en.wikipedia.org/wiki/Completeness_of_the_real_numbers) — Mephist

Perfectly well agreed.

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

That's a vague handwavy statement. The precise statement is that the sequence of real numbers $\langle s_n \rangle$ is Cauchy if:

$\forall \epsilon \gt 0 \ \exists N \text{ such that } n, m \gt N \implies |s_n - s_m | \lt \epsilon$

If you want to be pedantic that's the official definition. It says (informally) that A sequence is Cauchy if the tails get arbitrary close together. The intuitive idea is this. Suppose that we live in the open unit interval (0,1). We know about the sequence 1/2. 1/3, 1/4, 1/5, 1/6, ... But we can't say it "converges" because zero is not in our universe. Nevertheless there is SOMETHING about this sequence that "morally" converges, even if the point of convergence doesn't exist. That something is the property of being Cauchy. It defines a sequence that "should" converge if only there were something in our universe that it could converge to. That's why the standard reals are the Cauchy completion of the rationals. The reals contain the limits of sequences of rationals like 3, 3.1, 3.14, ... that "should" converge but don't, because pi isn't rational.

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

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. I have no idea what your formulation means since I have no idea what near() means. The entire point of the Italian formulation is that it's written in standard math language and makes perfect sense in the context of standard math.

When you say, "As you said ..." and then quote something I NEVER SAID, I despair. Why did you do that?

In the logic of Coq, "completeness" IS A FUNCTION, at the same way as "near" is a function and "+" is a function. — Mephist

Yes but I'm not talking about Coq.

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

Yes but I didn't ask about Coq.

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

Yes but I didn't ask about Coq, nor does what you wrote help me because it's written in a nonstandard language.

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

I'll take your word for it, but I didn't ask about Coq and this verbiage doesn't help me understand the constructive reals.

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

All well and good, but nothing I asked about or talked about.

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

Doesn't help me understand anything, doesn't respond to any of the questions and points I raised earlier.

* 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

No you haven't.

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

Pi is computable, so this is all completely beside the point. It's computed by the famous Leibniz formula, for example, which can be coded up by a beginning student of programming.

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

You completely misunderstand the relation between axiomatic definitions and constructions. Completeness is a theorem about Dedekind cuts and an axiom of the axiomatic definition of the reals as a complete ordered field.

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

I have no idea what you're talking about. Is an external machine like an oracle? What do you mean? Why is this relevant?

In any event all of this has NOTHING AT ALL to do with the specific points I raised about the completeness axiom in the Italian paper that you asked me to read.

However, remember that this is an AXIOMATIC DEFINITION of what real numbers are, NOT A MODEL of real numbers. — Mephist

Ok whatever. Same remarks as all along. Even if true, it's seriously off course relative to the concerns I raised.

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

As Gödel pointed, out, if there's a model then the axioms are consistent. That's the purpose of the Dedekind and Cauchy models: To show that the real number axioms are not vacuous.

And that is true even for Tarski's real numbers, that are described using classical (non intuitionistic) logic. — Mephist

Ok fine, but it would be far better if you'd try to respond to the specific points I made.

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

Not news to me but if it seems worth an exclamation point to you, ok.

The problem is that sets are defined axiomatically in ZFC. — Mephist

This is a problem?

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

As I pointed out earlier, if there's a model of the reals then the axioms for the reals are consistent.

I perfectly well agree that nobody can prove within ZFC that ZFC is consistent. What of it? That's an 88 year old result and everyone's made their peace with it long ago.

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

You're just complaining about incompleteness. Like I said, 88 years and counting. You'll just have to get over it. I honestly don't know what to say.

But, obviously, there is no finite model that verifies all the axioms of ZFC. — Mephist

Ok, for a moment there I thought you had one in your back pocket that you were going to throw at me. But no, there isn't any such thing.

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

Right.

OK, I'll stop it here because it's just become too long and I am only at the first question. — Mephist

You haven't answered any of my questions. You've gone backward by changing the subject. I am ONLY interested at the moment in the completeness axiom in the Italian paper, because it is written in the language of standard math and I can work with it technically.

I've already convinced myself that their axiom implies standard Cauchy completeness, but not yet the converse.

* 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

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.

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

We agree on one direction but I haven't seen a proof of the other direction.

Intutionistic convergense implies standard convergence, but is the converse true?

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

My understanding is that intuitiionist logic doesn't have enough rules to do standard math. That's my question.

* 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

Tell it to the authors of the Italian paper, which specifically references the rate of convergence. Their axiom is explicitly phrased as a claim about the rate of convergence.

Didn't you even read my post that you claim to be replying to? I"m really baffled here. Please go back and read what I wrote.

They explicitly talk about the rate of convergence as being significant. That's one of my questions.

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

Surely this is patently false; the noncomputable numbers serving as witnesses.

* 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

They're implied by Cauchy completeness. I can check. I have checked. I could check here in public. There are only countably many Turing machines and uncountably many reals. That's the proof of the existence of noncomputable reals.

This is not true: any model of real numbers is ultimately based on an axiomatic theory that cannot be checked "by hand". — Mephist

I don't know what that means. I can prove there are infinitely many primes and I don't have to check them all by hand. I can prove that every even number is divisible by 2 without checking them all by hand. Wiles can prove Fermat's last theorem without checking every quadruple (a,b,c,n) of positive integers by hand. So what?

[ 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

Completely separate topic, but math markup is the best thing ever and anyone studying math should take the time to learn it. The basics are very simple.

$e^{i \pi} + 1 = 0$

On some websites you can Quote that and see how it's done; but this particular website quotes the marked up form and not the original markup, unfortunately.

The markup for the above is: e^{i \pi} + 1 = 0, enclosed in "math"begin and end tags enclosed in brackets.

And probably I still wasn't able to be clear enough on what I meant. — Mephist

I know you're passionate about your point of view, but I don't know what your point of view is. I've asked you repeatedly to state a clear and concise thesis so that I can understand where you're coming from.

I gather that your point is that ZF is not constructive and that Coq is. That's fine. But my understanding is that the constructive reals can't contain all of the standard reals and that therefore they can't be Cauchy complete. That's the point I'm trying to understand. You're claiming the constructive reals are Cauchy complete and I most certainly have not seen a proof of that fact nor do I believe any proof could exist. I'm happy to be shown the error of my thinking.

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?

I have made progress on the Italian completeness axiom and that's the focus of my efforts at the moment.

ps -- I found a paper of interest:

https://arxiv.org/abs/1510.00639

On the Cauchy Completeness of the Constructive Cauchy Reals

Abstract: "It is consistent with constructive set theory (without Countable Choice, clearly) that the Cauchy reals (equivalence classes of Cauchy sequences of rationals) are not Cauchy complete. Related results are also shown, such as that a Cauchy sequence of rationals may not have a modulus of convergence, and that a Cauchy sequence of Cauchy sequences may not converge to a Cauchy sequence, among others."

I think I may find some clues here.

OK. I see what I am doing wrong: I am making very long premises to be able to refer to them in the following argumentation. But if you start reading the beginning without looking at the following part you find what I wrote completely unrelated to the point you are asking.
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.

Yes but I'm not talking about Coq. — fishfry

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

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.

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

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.

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

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

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

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

$completeness: \forall f: N \to R. \exists x \in R. (\forall n \in N. near(f(n), f(n+1), n+1)) \to (\forall m \in N. near(f(m), x, m))$

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

[ 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 ]

Read this first, don't waste time slogging through my other posts. This is the heart of the matter.

Hi @Mephist. I didn't read your latest posts but I had another little insight.

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

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

So I didn't want to give you the idea that I think your Coq material is anything less than awesome. It's just that I'm on a Mission right now and must focus on one thing.

* And what is that thing? It's Cauchy completeness.

* And I figured something out tonight. Just from eyeballing that paper I linked earlier about Cauchy completeness in the constructive reals. This paper.

https://arxiv.org/abs/1510.00639

And this is what I'm getting, if I am getting this right. You know how these days it's so easy to learn "about" things, without learning the things. One reads a Wiki page, one gets the gist; but without putting in the years it takes to actually own the material. But we can still make connections among or "knowing about" facts and ideas. This is kind of epistemological. Knowing stuff (years of study) versus knowing about stuff, as in eyeballing Wiki for five minutes.

So with that disclaimer, this is what I think I understand:

The constructive reals are Dedekind complete but not Cauchy complete.

Now this is something I can sink my teeth into because it's math I can investigate. That's why I have to find my own learning path through this material. When people start talking about Martin-Löf type theory and lambda calculus, it does me no good because I never learned those things. But I know a lot of other things.

For example, in the standard real numbers, Cauchy and Dedekind completeness are equivalent. You have one if and only if you have the other. And so, here is a confession: I don't even know what Dedekind completeness is. That's because I know what Cauchy completeness is and Dedekind completeness is just another equivalent form. So I never bothered to pick it up.

But now it turns out that (if I'm reading that latest paper correctly, and this is all from a very cursory read) that in the intuitionist setting, they are not the same. That was a direct quote I think from the paper.

So now I need to look up Dedekind completeness, get warmed up by proving its equivalence to Cauchy completeness, 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!)

* I hope you can see that I'm on a very focused path right now. I want to grok the "meaning" of constructivism. If it's subtly different then computability, I want to at least understand the difference.

So someday I will read all the Coq stuff; but from now on you should just be aware that you're writing it for yourself and others that may now or someday be interested. But it's going right over my head.

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

* This is it: The constructive reals are Dedekind complete but not Cauchy complete. When I understand that I will be enlightened.

Hi @fishfry!

Read this first, don't waste time slogging through my other posts. This is the heart of the matter. — fishfry

OK! as you wish :smile:

* 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

No problem!

* 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

Actually, I find Coq is much easier then the paper that you found! But everything depends on your background, I guess.

* And what is that thing? It's Cauchy completeness. — fishfry

OK, let's focus on Cauchy completeness.

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:

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

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

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

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.

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. 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), but if you build "Dedekind cuts" of real numbers you obtain again the same real numbers. 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).

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. Simply there are more possible "forms" for the object called "set of real numbers". 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).

* 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:

A thought experiment:

1. Imagine a backwards travelling, counting, eternal, time traveller
2. Assume that past time is infinite (I do not think it is, but for the sake of argument)
3. Then the traveller, will from our perspective, have counted every number
4. Seems unbelievable (no greatest number), but thats the nature of infinity
5. If this is not an actually infinite process, I’m not sure what would qualify?
6. Every number has been counted and no number corresponding to 'actual infinity' has been encountered
7. So it seems we can conclude that actual infinity is not a number?

So it seems we can conclude that actual infinity is not a number? — Devans99

That's what all the mathematicians say.

That's what all the mathematicians say. — tim wood

You will have to explain that.

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.

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

Yes. I know. You believe what you believe, never mind anyone or anything else. But look. Even here, just this simple, you mistake your topic. Transfinite numbers are not infinity. Infinity is not a transfinite number.

And what does "a minority view" mean in mathematics? There's an opinion, a minority view, on whether 2+2=4?

From online on Constructivism:
"Much constructive mathematics uses intuitionistic logic, which is essentially classical logic without the law of the excluded middle. This law states that, for any proposition, either that proposition is true or its negation is. This is not to say that the law of the excluded middle is denied entirely; special cases of the law will be provable. It is just that the general law is not assumed as an axiom. The law of non-contradiction (which states that contradictory statements cannot both at the same time be true) is still valid."

Whatever comes of this may be interesting, the way two-headed newts are interesting. But you seem to confuse the freakish with mainstream understanding. The great flaw in your arguments is your great If. Grant your if and you prove whatever you like. But without the If, like Cinderella's carriage, it reveals itself as just another pumpkin.

By the way, Constructivists deny the validity of many transfinite cardinals - because they're unconstructible.

Transfinite numbers are not infinity. Infinity is not a transfinite number. — tim wood

"Transfinite numbers are numbers that are "infinite" in the sense that they are larger than all finite numbers, yet not necessarily absolutely infinite. The term transfinite was coined by Georg Cantor, who wished to avoid some of the implications of the word infinite in connection with these objects, which were, nevertheless, not finite. Few contemporary writers share these qualms;it is now accepted usage to refer to transfinite cardinals and ordinals as "infinite". However, the term "transfinite" also remains in use."

- https://en.wikipedia.org/wiki/Transfinite_number

???

The definition of Aleph-naught is contradictory:

1. Aleph-naught is the size of the set of naturals
2. Sets contain a positive number of whole items only
3. So Aleph-naught must be a natural number
4. But there is no largest natural number
5. So Aleph-naught cannot exist (or be larger than all the natural numbers)