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.

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.

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.

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.

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.

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?

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?

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

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

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!

So, I would like to know if somebody has some convincing arguments against this point of view. — Mephist

Great essay and I've read some of his other stuff too. It's not the kind of thing one must vociferously disagree with. It's in the category of "Interesting even if wrong." Even if I believed that math is pure and must remain unsullied by practical concerns (an extreme version of formalism I suppose) I wouldn't disagree with Arnold about anything.

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.

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.

Hi all. I'm a frequent Trump explainer and/or defender, which can certainly appear like, and sometimes actually is, a measure of support. Nobody wonders more than I do where my own line is with the guy.

I've been following this Epstein story. First, Trump needs to fire Alex Acosta first thing in the morning. Acosta arranged Epstein's plea deal a few years ago. It was a corrupt deal to shield a very evil guy. Turns out that when they made the deal they failed to notify the victims as required by law. It's possible that the original case could be reopened. Either way there's going to be a lot of ugly stuff coming out about people in high places. Democrats and Republicans. Bill Clinton and Donald Trump are two names that will come up. Nancy Pelosi's daughter tweeted that "some of our faves" are going to be involved.

There's no evidence that Trump had sexual contact with underage girls. It's not his style. He likes beauty queens, showgirls, glamour girls. Look at his wives. I don't believe he directly did anything.

If he did, I will personally lead the impeachment parade. Whether it was last week or twenty years ago. He will not get a pass for acts committed before he took office. Nobody in the country will be able to defend him.

Short of that, if there is no credible evidence of Trump personally doing anything, he needs to get out in front of this and fire Acosta. If he doesn't the left will go wild. And I will not say a word in Trump's defense on this one.

Very ugly story, Epstein's crimes, convicted and alleged, along with the official corruption that enabled him, are beyond awful. I read an article that included the phrase, "hundreds of victims." Everyone involved needs to go down regardless of party affiliation. Let the chips fall where they may.

Here's a good backgrounder. Trigger warning this will turn your stomach. Both the sex crimes and the official corruption.

https://www.commondreams.org/news/2019/07/07/fresh-demands-labor-secretary-alex-acostas-resignation-mount-after-jeffrey-epstein

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.

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'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$!

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.

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.

\

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.

@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?

Would 1/0 = a vacuum/blackhole? -abstract thoughts — Pomme

No. Math is not physics. That seems to be a theme today.

In fact whenever mathematicians run into infinities, they do NOT say Aha here's an actual infinity in the real world. Some amateurs do that but professional physicists never do.

Rather, they say: "Our model has broken down. We don't know what happens below a certain scale, which is small but greater than zero."

There's an elementary example that most people should be familiar with. Consider classical Newtonian gravity,

$F = G \frac{m_1 m_2}{r^2}$

where $F$ is the gravitational force, $G$ is the gravitational constant (just some number that makes the units work out), $m_1$ and $m_2$ are the masses of the two bodies, and $r$ is the distance between their centers of mass.

Newton proved a theorem that if the bodies are spherical, you can just use the center of masses and it's the same as if you added up the gravitational attraction between all the respective pairs of points in the two spheres, a much harder calculation. Basically Newton did multivariable calculus before there was multivariable calculus.

Because of this theorem, it's common to think of massive bodies as point masses; that is, dimensionless points that nevertheless have mass.

Now if you have two point masses, they can get arbitrarily close together. As the distance between the two point masses gets close to zero, the gravitational energy between them gets arbitrarily large. It "goes to infinity" as they say.

Physicists do NOT say, "Wow a black hole with infinite energy results from two point masses getting too close together." We might think of it that way in a late night session at the dorm under the influence. But in the cool light of day we must say: "Newtonian gravity breaks down below a certain distance scale. When two sufficiently small masses are very close together, the gravitational energy is greater than all the energy in the universe. The equation may not be applied below a certain scale of distance.

You can see that even without quantum theory, we can show that there's a minimum distance, below which the theory breaks down. There's a sort of Planck length even in Newtonian gravity.

Here is a good explanation of what "contructive mathematic" means: https://www.iep.utm.edu/con-math/ — Mephist

Thanks man I'll get to this later. I am most definitely worn out for the day. What I did learn from all this is that the computable reals are NOT the constructive reals; and that the constructive reals can be Cauchy-complete. Now THAT I did not know, and it causes me to confront the depths of my ignorance. I'm really mystified on this point.

One article I'll definitely be rereading is Andrej Bauer's Five Stages of Accepting Constructive Mathematics.

http://math.andrej.com/2016/10/10/five-stages-of-accepting-constructive-mathematics/

That seems to be the common point of all your arguments about real numbers, so I wanted you to show you this: — Mephist

Yes but first, that in no way invalidates the fact that Cauchy-completeness uniquely characterizes the standard real numbers up to isomorphism; and secondly, that the comments and answers in that thread are "inside baseball" remarks from professional specialists in the field. I can understand the words but not the meaning. I have to assume the same is true for you, unless I'm wrong. I'm aware that Cauchy completeness is not the same as Dedekind completeness.

Example from one of the comments: "You won't find a model of ZF where they are different but there are models of IZF where they are different."

Now this is not something I'm prepared to say I understand even if I can parse the words. I assume the same must be true for you. This thread is very inside baseball, it's not for amateurs like us. IZF is evidently intuitionistic ZF. More mysteries beyond my pay grade.

But gee, I only meant to put in a good word for the standard reals. I'm not driving a stake in the ground and vowing to defend them to the death. Everyone knows they're murky.

The one thing I do put a stake in the ground about is that there aren't enough Turing machines to plug the holes in the computable reals. But apparently this is less clear when it comes to the constructive reals, which at least that one Italian paper seems to think are Cauchy complete. But how can that be? Apparently there are constructive approaches to Cauchy completeness. I confess great bafflement in this regard.

deleted

Formal logic (currently assumed as the foundation of mathematics) is only dependent on one very fundamental fact of physics (that usually is not regarded as physics at all): the fact that it's possible to build experiments that give the same result every time they are performed with the same initial conditions. — Mephist

Wow. I don't know where to start. That couldn't be more false.

Mathematics (what is called mathematics today) is the research of "models' factorizations" that are able to compress the information content of other models (physical or purely logical ones). A formal proof makes only use of the computational (or topological) part of the model. The part that remains not expressed in formal logic is usually expressed in words, and is often related to less fundamental parts of physics, such as, for example, the geometry of space. — Mephist

Not sure what you're getting at, but nothing I relate to.

Riemann understood that the concepts of "straight line", measure, and the topological structure of space are not derivable from logic, but should be considered as parts of physics. — Mephist

His work on non-Euclidean geometry was purely mathematical. But if you understand that Riemann knew that math wasn't physics; why won't you make that same distinction?

In te future, when mathematicians will start to use quantum computers to perform calculations, — Mephist

Mathematicians don't use computers to do calculations. This is a very naive point of view of what mathematicians do. It's often been remarked that of all the STEM fields, math departments don't use computers! The proof of the four-color theorem was an anomaly in 1976 and remains an anomaly today.

I believe that even the existence of repeatable experiments will not be considered "a priori", but as an even more fundamental part of physics. — Mephist

You've persistently claimed that mathematicians are doing physics, but this is an engineer's view of math. Mathematicians don't do physics. Just ask the physicists!

So, there will be quantum logic that is more powerful than standard (or even constructionistic) logic, at the price of not being able to be 100% sure that a proof is correct (but you will be able, for example, to say that we are sure about this theorem with 99% of probability). — Mephist

It's true that there are probabilistic proofs, but those are a subset of math, not all of math. Not even most of math. Mostly, a little bit of math.

Surely your ( and most of other peoples' ) reply to what I just said is that "this is no more mathematics". — Mephist

Not the first time you've put words in my mouth that I didn't say, wouldn't say, and don't agree with. But nobody would disagree that probabalistic proofs exist. But even the guy who wrote the famous Death of Proof article in Scientific American had to backpedal.

Well, at the time of Euler topology was not mathematics either. — Mephist

You seem to be grinding an ax but I'm not sure about what. That future math will be different than current math which is different than past math? Ok. Why would anyone disagree?

I hope going forward that you'll write less but with more focus. You really wore me out and in the end you yourself agree that you're not sure what the constructive reals are. As Gauss said: Few, but ripe.

Can you show me a physical theory, or a result of a physical theory, that is somehow derived from the fact that a continuous line is made of an uncountable set of points? — Mephist

You mean besides relativity and quantum physics? The 't' in the Schrödinger equation is a continuous parameter over the real numbers. What math do you think the physicists are using?

Of course I'm not saying that the physicists MUST use continuous math; only that to date, they do.

HOTT is not a constructivist theory (with my definition of constructivism) because it uses a non computable axiom: the univalence axiom — Mephist

I didn't know that. But ok. If HOTT is not constructive, what are we talking about?

And now after all this: What ARE we talking about? I no longer know what we're discussing. You lost me somewhere and you've refused to throw me a lifeline.

It's been interesting as hell, but the last two of your 4-part post really lost me.

This was considered by Voevodsky as the main "problem" of the theory, and there are currently several attempts to buid a constructive version of HOTT. One of them is cubical type theory (https://ncatlab.org/nlab/show/cubical+type+theory), but I don't know anything about it. — Mephist

Ok that's very interesting. Poor Voevodsky.

[ THIS WAS THE LAST PART :-) ] — Mephist

Yay! I made it!!!! Not sure what I accomplished, but at least I got caught up in this thread.

Yes, and this clarifies a lot o things about infinity: — Mephist

Ok, herewith my reply to Part 3.

"In first-order logic, only theories with a finite model can be categorical." (form https://en.wikipedia.org/wiki/Categorical_theory). ZFC is a first-order theory and it has no finite model (obviously), than it cannot be categorical. Ergo, you cannot use ZFC to decide the cardinality of real numbers: "if a first-order theory in a countable language is categorical in some uncountable cardinality, then it is categorical in all uncountable cardinalities." (from the same page of wikipedia). — Mephist

Ok fine. But now you're spinning off into new topics. I can't keep up with this. I've learned a lot from this thread but once again I urge you to focus your concerns so that I can address them. Who the hell is arguing that first-order logic can determine the cardinlity of the reals? Who is claiming that????

Then, you can say, the problem is in the language: let's use a second or higher order language, and you can discover the "real" cardinality of real numbers. — Mephist

But I haven't said that!!!! You are arguing with strawmen. We already know that ZFC does not determine the cardinality of the reals. Who the hell is saying any different?

Well, in my opinion this is only a way of "hiding" the problem: it is true that if you assume the induction principle as part of the rules of logic, you get a limit on the cardinality of possible models (the induction principle quantifies over all propositions, so it's not expressible in first-order logic), but this is exactly the same thing as adding an axiom (in second order logic) and not assuming the induction principle as a rule. Ultimately, the problem is that the induction principle is not provable by using a finite (recursively computable) model: it's not "physically" provable. — Mephist

I have no idea what you are talking about. Honestly. I can't relate this to anything we've been discussing.

That's exactly the same situation as for the parallels postulate in euclidean geometry: you cannot prove it with a physical geometric construction (finite model), because it speaks about something that happens at the infinite, and the fact of being true or not depends on the physical model that you use: — Mephist

Once again I fail to relate this to anything we've been discussing.

Physical model? Physics has nothing at all to do with the independence of the parallel postulate.

if computers that have an illimited amount of memory do not exist, or, equivalently, if infinite topological structures do not exist, then the induction principle is false, and infinitesimals are real! — Mephist

My friend @Mephist, that is word salad and nonsense. We've come this far, but you're losing me. What you said is just false, to the extent that it has any meaning at all.

So, the sentence "if you use uncomputable (non constructive) axioms in logic, you can decide the cardinality of real numbers", for me it sounds like "if you use euclidean geometry, you can prove the parallel postulate". — Mephist

Well at least Part 3 was easy. It's incoherent. I don't mean to be provocative. Only that your other posts to me have been insightful and interesting; and Part 3 was nonsense.

But now I'm ready for Part 4 and my catching up to your posts will be a great accomplishment for me. I urge you, I beg you, to try to be concise. You're burying your own points in words.

I think in that in an ideal mathematical language, Chaitin's Omega wouldn't be stateable. To say 'Omega is definable but non-computable' is surely not a statement about a number, but a statement about the syntactical inadequacy of our mathematical language for permitting the expression of Omega. — sime

You'll have to take that up with Chaitin and the mathematical logicians. As it happens, the class of real numbers definable in first-order logic is slightly larger than the class of real numbers computable by Turing machines. This is indisputable. I have no idea what an ideal mathematical language is. But in fact I only used Chaitin's Omega because it's a noncomputable real that we can visualize. The proof would go through with any noncomputable number. The n-th trunctions of any noncomputable number form a Cauchy sequence of computable numbers that fail to converge to a computable number. proving that the computable reals are not Cauchy-complete.

Let's take as reference the most complete proof of the theorem that I was able to find: — Mephist

I have to defer this for now. You already said you're not interested in the proof of B-T and now you've written a lengthy post about it. The proof in ZFC is unassailable, there is no point in your trying to find fault with it. And no point in my trying to explain it, since you shook my confidence in our conversation by claiming a translation in Euclidean space can't be continuous. I wish you'd keep your posts simple.

Right now my plan is:

* Catch up to parts 3 and 4 of your earlier replies;

* Catch up my mentions on the political threads;

* Try to get you to state a simple thesis so that I know what you're talking about. As it is you have given me definition of constructive reals that contradicts itself, along with a badly translated paper that defines the constructive reals as isomorphic to the standard reals. I can not keep up with all this as much as I'd like to.

* Urge you to split out a SEPARATE THREAD on Banach-Tarski. And start with a study of the paradoxical decomposition of the free group on two letters. That's the heart of the paradox and it doesn't require any set theory. It would be true in anyone's universe.

OK, this is the end. I think I cannot explain better than this my argument about BT. — Mephist

There's little point in your trying to find fault with an 80 or so year old theorem that's been checked and rechecked. But I would love for you to split out your B-T concerns into a separate thread so we can focus on them. Your claim that isometries aren't continuous or don't preserve topology is just terribly wrong, I honestly don't follow your reasoning at all. You also confuse measure 0 with nonmeasurable.

By the way I truly commend you for diving into the proof. You seem to understand most of it. That's impressive. I'm not sure what you mean about your objection but I'll try to understand it.

I tried to google for "constructive real numbers are not complete", or something similar. — Mephist

Ok herewith my response to your Part 2. I'm buried in mentions again. Working hard to catch up.

I think this is what you refer to by "constructive reals". Is it?
Can you give me a link where is written that they are not complete? — Mephist

I posted earlier a proof that the computable reals are not complete. That's indisputable.

But it turns out that you are right, the constructive reals are not quite the computable reals, and I found many points of inconsistency in the literature.

First:

"The concept of a real number used in constructive mathematics. In the wider sense it is a real number constructible with respect to some collection of constructive methods. The term "computable real number" has approximately the same meaning."

https://www.encyclopediaofmath.org/index.php/Constructive_real_number

Ok, the constructive reals are sort of like the computable reals. Then this:

"The main message of the notes is that computable mathematics is the realizability interpretation of constructive mathematics."

http://math.andrej.com/2005/08/23/realizability-as-the-connection-between-computable-and-constructive-mathematics/

Ok, the computable reals are the "realizability interpretation" of the constructive reals. I'm not familiar with that technical phrase but it seems to indicate once again that the computable reals aren't too far off from the constructive reals.

But then there's this link you gave me:

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

That paper (badly written and/or badly translated, and confusing) give a completeness axiom that they claim makes the constructive reals complete. But if that's true, then this is nothing more than an alternative axiomitization of the standard reals. Good for Coq, fine; but devoid of philosophical interest since all complete totally ordered fields are isomorphic to the standard reals.

By this paper, which you asked me to look at, the constructive reals ARE the standard reals and contain uncountaby many noncomputable reals.

So I admit I have no idea what the constructive reals are and I can't find two explanations that are consistent with each other.

Perhaps the problem is with the underlying murkiness of intuitionism. Or perhaps I haven't seen the right article.

But I'll conceded that evidently the constructive reals are different than the computable reals; but how, I can't say and don't know.

I am convinced that my definition of "constructivism" is not the same thing that your definition. — Mephist

After a day's research, I agree. I have no idea what the constructive reals are.

Well, here's a simple definition of what I mean by constructive logic:
=== A logic is called constructive if every time that you write "exists t" it means that you can compute the value of t. === — Mephist

Well than that is inconsistent with the article you asked me to read. Because that article's constructive reals are Cauchy-complete, and therefore must include many noncomputable real numbers. So your definition is not consistent with the definition in that article.

But if YOU are falling back on the requirement that constructive reals must be computable, then I already proved (twice) that they are not Cauchy complete.

I believe that you can define real numbers that are complete in a constructive logic. I think the example that I gave you using Coq is one of these. But I could be wrong: I am not completely sure about this. — Mephist

Yes, that's the problem. The link you gave me did do this. But then the constructive reals in that article must (a) contain lots of noncomputable reals, and (b) must be isomorphic to the standard reals, depriving them of any philosophical interest regardless of how Coq-compatible they may be.

I googled this: "non archimedean fields are not complete" and the first link that come out is this one:
https://math.stackexchange.com/questions/17687/example-of-a-complete-non-archimedean-ordered-field — Mephist

Yes, I agree I was wrong about my claim. However the hyperreals do happen to fail to be Cauchy-complete, so my Goldilocks remark stands.

Probably, as they say, "The devil is in the detail". I read several times in the past about Abraham Robinson's hyperreal numbers, and I believe that I read somewhere that non archimedean fields are not complete. So I believe that, under appropriate assumptions, this is true. But why is this a problem? — Mephist

Why is not being Cauchy complete a problem? Because then they fail to satisfy the ancient intuition of the continuum. I thought I explained all that.

Hmmm... I understand what you mean:
- "constructive" reals are computable functions. Then there is a countable number of them — Mephist

Yes. But there's even another wrinkle. The computable real numbers are countable; but they are not effectively countable. That's because any enumeration of the noncomputable reals must be noncomputable itself. Else you'd solve the Halting problem. So a strict computabilist can claim that the computable reals are NOT countable, because there's no computable enumeration of them! I've seen this argument in print.

- standard reals are the set of all convergent successions of rationals then their cardinality is aleph-1
- nonstandard reals are much more than this (not sure about cardinality), since for each standard real there is an entire real line of non-standard ones. — Mephist

Not a real line, a "cloud." Let's please not go off talking about the hyperreals. I only used them to point out that of the three famous models of the reals, only the standard reals are Cauchy complete.

Well, here's how I see it:
- "constructive" reals (with my definition) can be put in one-to-one correspondence with standard reals, only with a different representation — Mephist

If that's true then they necessarily contain many noncomputable reals, contradicting your own definition.

(but I don't know a proof of this) and do not correspond to computable functions. It is true that if you can write "Exists x such that ... " then you can compute that x, But for the most part of real numbers x there is no corresponding formula to describe them (and this is exactly the same thing that happens for non constructive reals). — Mephist

You're already contradicting your own definition. The constructive reals, whatever they are, are quite murky.

- Robinson's nonstandard reals are more than the standard reals because you exclude induction principle as an axiom (so that "P(0)" and "P(n) -> P(n+1)" does not imply "forall n, P(n)"). But there are objects used in mathematics that are treated as if they were real numbers, but DO NOT have the right cardinality to be standard real numbers: for example the random variables used in statistics: — Mephist

At this point I have to decline to go off in yet another direction. I actually wish you would make a brief, simple, clear point that I can work with.

https://en.wikipedia.org/wiki/Random_variable . So, they are more similar to nonstandard reals. — Mephist

I'll pass on this remark but I don't agree with it.

- The real numbers of smooth infinitesimal analysis are less then standard real numbers, and even the set of functions from reals to reals is countable: basically, every function from reals to reals is continuous and expandable as a Fourier series. And there are infinitesimals.
What for such a strange thing? Well, for example, they correspond exactly to what is needed for the wave-functions and linear operators of quantum mechanics: there are as many functions as real numbers, and a real numbers correspond to experiments (then, there are a numerable quantity of "real" numbers). And what's more important, a wave function contains a definite quantity of information, that is preserved by the laws of quantum mechanics. — Mephist

Fine, whatever. I would prefer at this point to constrain the discussion, not widen it. I was greatly disheartened after reading your own link and finding out that their model of the constructive reals is isomorphic to the standard reals. That undercuts everything I know about the constructive reals.

So, from my point of view, there is not one "good" model of real numbers, at the same way as there is not one "good" model of geometric space. — Mephist

There's exactly one model (up to isomorphism) that is Cauchy complete; and that is the standard reals.

[ END OF PART TWO :-) ] — Mephist

Ok. Next up, parts 3 and 4, and a big stack of mentions in the politics forum, which I'm afraid to read.

But can you do us both a favor and write a short, clear, and consise thesis that we can discuss? Part 2 was terrible for me because it contradicted itself in so many ways, giving multiple characterizations of the constructive numbers, at least one of which is isomorphic to the standard reals modulo an awful translation from the original Italian.

I think this is what you refer to by "constructive reals". Is it?
Can you give me a link where is written that they are not complete? — Mephist

I have a lot more to say about this second of your posts (of the four that I'm working through) but I wanted to just catch this up first because I already proved this earlier but with so much verbiage back and forth it was easy to miss.

You know Chaitin's Omega? Very cool number, because it's actually a specific example of a noncomputable real number, or rather any one of a specific class of noncomputable reals. We can define it because it's a definable real even though it's not computable. It's not computable because if it were, it would solve the Halting problem, which Turing showed we can't do.

Now, consider a sequence whose n-th term is simply the n-th truncation of Omega's decimal expression. In other words if we take pi, we can form the sequence 3, 3.1, 3.14, 3.141, ... This is a Cauchy sequence that converges to pi. This is an example of a Cauchy sequence of rationals that fails to converge to a rational, showing that the rational numbers are not Cauchy complete.

Likewise we can form the Cauchy sequence of rational numbers that are the n-th truncations of the decimal digits of Omega. This is a Cauchy sequence of computable numbers, because it's easy to see that a rational number is computable. The algorithm that cranks out the decimal digits is just grade school long division.

But this is a Cauchy sequence of computable numbers that fails to converge to a computable number! So the computable real numbers are not Cauchy-complete. QED.

Now the big problem IMO with the computable reals is that you can do this for every noncomputable real. Every noncomputable real represents the limit of a sequence of rational hence computable numbers that fail to converge to a computable real number. The computable real line has only countably many points and uncountably many holes. It's the swiss cheese of number lines and a terrible model of the ancient idea of the continuum. I confess that I do not understand why Brouwer and Weyl were not greatly troubled by this.

The other thing I wanted to mention about your post is that you found an example of a non-Archimedean ordered field that's Cauchy complete. I stand corrected!! I'm apparently wrong on this point. But I thought otherwise and now I have to try to understand why I've seen a proof that a non-Archimedean field can't be complete. This is a mystery but thank you for digging up this example, I have to study it.

Either way it's not too critical. In fact the Robinson hyperrreals are NOT Cauchy-complete so my Goldilocks remark still stands even if I am wrong about the general case.

Yes, I really wasn't interested in speaking about Banach-Tarski. I took it only as an example, maybe the wrong one. But on the other hand I am convinced that what I wrote is correct, so I am a little upset to not being able to convince you (and it's not about you: probably I didn't convince anybody...). I could start a separate discussion and try to use formal proofs instead of explanations, but I am afraid it's not appropriate for a philosophy forum (I still didn't read how to write symbols on this site). Maybe I'll make a last attempt tomorrow, and than stop talking about BT. But I have not time now. However, thank you for replying to my posts. — Mephist

Well I'm three of your posts behind I think so I'm planning to get to them soon.

But I'm not sure what you mean that " I am convinced that what I wrote is correct, so I am a little upset to not being able to convince you ...' About what? There are two things going on:

1) The business about ZFC and point-sets being "wrong" in some way; and

2) Your misunderstanding of isometries, which preserve measure of all measurable sets.

I don't know which one you want to talk about. I don't know what you think you didn't convince me of. I see foundations as historically contingent and not all that important to what working mathematicians do anyway. And you certainly didn't convince me that foundations are for the purpose of modeling physics, that's not mathematically true at all, it's something only a physicists or an engineer would believe :-)

So maybe you can concisely tell me exactly what thesis you are trying to convince me of. No, formal proofs would be the wrong way to go without a simple one or two sentence description of the thesis being put forth.

But if I understood you, you believe that the rightness of a foundation can be measured by how well it lets us model physics. And that's 100% opposed to what I think foundations are. Math is not held to the standard of physics, hasn't been since Riemann.

So just tell me as clearly as you can what it is you're trying to convince me of. That will be helpful to me because you covered a lot of different topics in the post I replied to and I spent a lot of time trying to explain that rigid motions are continuous and preserve measure, and if you don't care about those things we shouldn't lengthen our posts with them.

One can imagine measuring the time it takes a kettle to boil by the heartbeat of the person watching it, — fdrake

Yes Galileo used his heartbeat as a timer.

the clock measuring both factors out. In that regard time's an instrumental variable for any bijective continuously differentiable function of it. — fdrake

Ah but no. The continuity of the real numbers are the mathematical model of time. But we don't know for sure if time itself is continuous. That was my point. I don't necessarily take differential equations for reality. It's the map/territory thing.

In any case, unlike genuine fake news (!), the NYT at least publishes corrections, listens to criticism, and tries to correct the record. — Wayfarer

Little late for that. Thanks for your thoughtful comments. I was against the Iraq war at the time and clearly that's colored my take on current events ever since. Once Hillary gave cover to the Dems to support the war, my connection with modern liberalism started to slip. Obama's continuation of the wars and his institutionalization of the torture finished me off.

Which, by the way, is how we got Trump. He called out Jeb! on W's war. Hillary was the opponent. Sure the deplorables are HALF of Trump's supporters, as Hillary correctly noted. Who are the other half? Those who remember that Hillary Clinton could have stopped the war with a word, and chose not to. That, and the lying New York Times. Look at the trillions wasted since then. Look at our foreign policy.

Fake news is lying the country into war. Everything else is just someone's little website. When the NYT lies they cause real damage.

The NYT is considered liberal. — Coben

Ah. Good point. They are liberal on social issues. On matters of war, they take the establishment line. That's the whole point. The NYT helped Bush lie the country into war. Sure they're social liberals. Their support for the Iraq war and their suppressing the story about Bush's illegal domestic surveillance until after the 2004 election gives the lie to the claim that they are any kind of peacemongers.

And today? They are leading the charge toward a war with Russia. The NYT is not for peace. Nor are most liberals anymore. It's been a long time since Vietnam.

What's left of the anti-war movement, anyway? Me and Tulsi, that's about it.

The problem with your example that you make the judgment "in the fullness of time". — Number2018

A million people marched against the Iraq war. I didn't believe the bullshit about the WMDs. And if Saddam had WMDs it's because we sold them to him when he was our ally during the 1980's Iraq-Iran war. I knew that at the time and so did millions of others.

I'm disappointed there are so many apologists for the Iraq war in this thread. I was not fooled at the time nor were millions of other Americans. Americans were angry about 9/11 which Saddam had NOTHING to do with. Bush's neocons used that anger and fear as an excuse to invade countries that they had already been planning to invade. That was perfectly well known at the time.

Do you know the PNAC document? The Project for a New American Century? The perpetrators of the attack on Iraq knew exactly what they wanted to do -- to depose the governments of Iraq, Iran, Syria, and several other Middle Eastern countries.

I am sorry, I am not buying the level of naivety I'm seeing here. The Iraq war was a lie and it was perfectly clear at the time. If any Middle Eastern country was up to its eyeballs in 9/11 it was our "good friend" Saudi Arabia. You know that, right?

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

Am I telling people things they've never heard before? You know what? If you don't know that Cneney and Wolfie and Feith and the rest of the neocons were already planning multiple invasions of multiple Middle East countries BEFORE 9/11, and used Americans' fear and anger to whip up war fervor, then YOU are the victim of fake news. That's EXACTLY what fake news is.

You think the invasion of Iraq was an honest policy decision? Even at the time? That's fake news.

By your logic every news outlet that covered what George W. Bush claimed, what Dick Cheney claimed, what Colin Powell claimed, what Condoleezza Rice claimed, what Donald Rumsfeld claimed, and what others in the government, military, and intelligence claimed about weapons of mass destruction are complicit as purveyors of Fake News. — Fooloso4

Yes, thanks for mentioning it. That's exactly what fake news is. When the establishment lies the country into war. Cheney, Powell, Condi, Rummy, Doug Feith, and Paul Wolfowitz should be in prison along with Bush. That's Obama's greatest failing. Instead of holding the Bush regime accountable for the war and for turning the US into a torture regime, he institutionalized those things. So that we're STILL at war, several of them, and the torture camps are still open. You just don't hear about them because we've all become numb to it.

That is exactly what fake news is. Fake news is not when some little alt-right or alt-left website prints something that questions the establishment narrative. That definition of fake news is itself fake news.

Fake news is when the establishment lies the country into war. Fake news is the Reichstag fire, the Gulf of Tonkin, the WMDs. Fake news is Assad "gassing his own people," which he never did. Fake news is last week's Iranian shootdown of a US surveillance drone that was most likely in Iranian airspace. The Japanese government doesn't believe the US's story. Neither do I.

So yeah thanks for bringing this up and helping me to bring focus to my thoughts.

Fake news is when the establishment sells big lies to the public. It's NOT when little alt-websites question the establishment. Fake news is the Big Lie that the government sells to the people. That's the point, which in retrospect I should have just said right up front several posts ago. Fake news is how the powers that be keep everyone frightened and compliant. That's what fake news is.

I Googled "Judith Miller lies. Iinterestingly, when I Googled "Judith Miller," Google autocompleted "lies" as the first suggestion.
— fishfry

Apparently you do not know how google works via algorithms based on what is on your computer. — Fooloso4

You're right, it's possible that I may have googled that phrase at some time in the past. Still, the larger point remains. Anyone who thinks Judith Miller made an honest mistake, as opposed to being a deliberate lying propagandist for the war, is either a fool or a neocon maniac. That's my sincere belief. You disagree ok. Your examples didn't convince me. Chris Matthews? Another suckup to power. You may recall he liked Bush's "swagger." Salon? Give me a break. When did the liberals become such a bloodthirsty bunch of warmongers?

A million people marched in the streets against that war, but Hillary and the New York Times joined up with Bush. And now, 17 years later, we're still there. You really want to defend the NYT's role in this awful thing?

What the NYT published was fake news. That's why I brought it up. The single most consequential piece of fake news we've seen in 20 years, one whose consequences aren't done yet. But I didn't even mention the fact that the NYT chose to NOT report Bush's illegal domestic spying until AFTER the 2004 election. That revelation would have made Kerry president.

So you can have your moon hoax videos and your $200k worth of Russian troll farm Facebook ads. But they're nothing. By reach and influence and deadly consequences, the New York Times is the biggest purveyor of fake news on the planet.

I'm not mentioning that to make a right-wing attack on the NYT. I'm pointing this out because when we label the alt-left or the alt-right as fake news and whatever the NYT publishes as the Shining Truth, we deeply misunderstand what fake news is. Fake news is when the government and the "paper of record" lie the country into war. That's what fake news is.

But ok, Judith Miller is just misunderstood. If you say so. I'll take you at your word that you sincerely believe Judith Miller was not a deliberate neocon propagandist. The depth of my passionate disagreement with that viewpoint precludes me from engaging in rational discussion of the point. Chris Matthews. Perfect example of everything wrong with the left these days. I remember a long time ago when he used to be relatively sane. But he preferred Bush's swagger to peace. You'll forgive me if I don't cheer.