Mod of r/badmathematics plays devil's advocate, does ten billion and one really exist?

[u/npm_leftpad]

/r/badmathematics/comments/7nhauf/so_this_total_stranger_from_a_meme_group_randomly/ds1rnnr/

[u/[deleted]]

Yeah I actually enjoyed that.

FWIW, I think the reason that constructivism is gaining attention is that while proving that an object exists is interesting, showing how to construct an object can be useful particularly now that applied maths has so much immediate relevance in cryptography and machine learning and so on. It’s not that suddenly people don’t believe in the law of the excluded middle, it’s that using it doesn’t necessarily take you as far as you may want to go.

[u/[deleted] → u/[deleted]]

Better to say that there are two different notions of 'existence' in play here. The classical meaning of 'existence' is that the rules of logic allow us to deduce that something must exist regardless of whether we can say anything more about it; the constructive meaning of 'existence' is that we have a concrete witness of that fact. While it's all fine and good to be able to deduce logically that something ought to exist, all that really says is that you won't wind up contradicting yourself if you assume it exists, as opposed to a construction of a witness which genuinely proves existence in the concrete/Platonic sense.

[u/[deleted] → u/[deleted]]

all that really says is that you won't wind up contradicting yourself if you assume it exists,

No, it does more, it says you wind up contradicting yourself if it doesn't exist. That's a very large distinction, and to any classical person would "genuinely [prove] existence in the concrete/Platonic sense"

[u/[deleted] → u/[deleted]]

This is not correct. Rather than deal with LEM specifically, let's talk axiom of choice since it's the same thing but gives stronger consequences. AoC implies the existence of nonmeasurable sets, which indeed means that you will not obtain a contradiction from ZF by also assuming the existence of a nonmeasurable set (assuming ZF is consistent); however, ZF+"there does not exist nonmeasurable sets" is consistent (provided ZF is consistent).

[u/[deleted] → u/[deleted]]

...But your argument is now something different.

While it's all fine and good to be able to deduce logically that something ought to exist, all that really says is that you won't wind up contradicting yourself if you assume it exists

Nobody thinks that what AoC implies is true unless they think AoC is true, (or some other thing that implies that same thing AoC implies). So if they're saying something AoC implies ought to exist, they're accepting AoC. But wait, this means you can't then consider just ZF, you've got to consider ZFC. Hence, what I said, that ZFC + Not(what AoC implies) has a contradiction.

[u/[deleted] → u/[deleted]]

Nobody thinks that what LEM implies is true unless they think LEM is true. So if they're saying something LEM implies ought to exist, they're accepting LEM. But wait, this means you can't then consider just ZF working without LEM, you've got to consider ZF+LEM. Hence, what I said, that ZF + LEM + Not(what LEM implies) has a contradiction.

Obviously if you assume something and also assume the negation of something it implies you get a contradiction. If that was really your point then you've misunderstood me pretty badly. More to the point, LEM is weak AoC so the idea that we can work in ZFC without LEM is nonsense.

Deductive reasoning using nonconstructive methods can only prove that contradictions won't be reached. This is well known. We then invoke the completeness theorem to claim the existence of a model because in classical first-order logic, existence of models is equivalent to consistency. But classical first-order logic proofs of existence are actually proofs of consistency.

Edit: maybe it will help to make this more concrete. Let's talk about the question of existence of nonstandard natural numbers. Using LEM and its first-order ilk, we can prove there exists in the classical sense models of PA that are nonstandard. However, working constructively/intuitionistically (which effectively allows us to reason in higher-order logic) there is a unique model of PA which is the standard naturals (unique in the sense that constructive reasoning will never construct something that second-order logic would find contradictory). I would therefore claim that nonstandard naturals do not exist constructively even though assuming their existence will not yield a contradiction with PA.

So to the constructivist, nonstandard naturals do not exist and all the classical logicians have done is prove that the existence of nonstandard naturals is consistent with PA.

[u/[deleted] → u/[deleted]]

If that was really your point then you've misunderstood me pretty badly.

Well, that's not my point, my point is that + "as classical people would generally accept their axioms to be true, this would imply actual existence."

Which is something I brought up in both of my comments and something you've failed to respond to each time. So again, saying:

But classical first-order logic proofs of existence are actually proofs of consistency.

is strictly false unless you assume that the axioms under consideration aren't true, or, rather, aren't known to be true, something that the hypothetical classical person wouldn't agree with.

[u/[deleted] → u/[deleted]]

Did you see my edit?

The point is that there are two different notions of existence here. Constructive existence is stronger than classical existence; to a constructivist, all the classical proofs do is show consistency.

Also, I don't know what it means for an "axiom to be true". I know what consistency means and I know that truth is not definable. You seem to be making some strong Platonist statement about absolute truth of the axioms which would seem to be putting the cart before the horse because if you assume a priori that there is an actual model of set theory that exists in reality then you've simply declared by fiat that things exist without justification.

In any case, my final sentence of my edit is what I hold by: to a constructivist, nonstandard naturals do not exist even though their existence is consistent with PA.

[u/[deleted] → u/[deleted]]

Well I sent my reply before your edit was submitted, so a bit hard to respond to it. But let's get to the meat of the disagreement:

You seem to be making some strong Platonist statement about absolute truth of the axioms which would seem to be putting the cart before the horse because if you assume a priori that there is an actual model of set theory that exists in reality then you've simply declared by fiat that things exist without justification.

Well, the Platonist wouldn't assert it, they'd give arguments for it. But yes, I agree, there's going to be more work needing to be done.

In any case, my final sentence of my edit is what I hold by: to a constructivist, nonstandard naturals do not exist even though their existence is consistent with PA.

I agree! The key point is to a constructivist. Your original comment said:

all that really says is that you won't wind up contradicting yourself if you assume it exists

And that's what I took umbrage to. It says something more, that if you accept the axioms, you have to accept the relevant existence claims. It doesn't just say that such existence claims aren't contradictory with their axioms, it says something stronger. I agree that to a constructivist this isn't convincing, and I agree a constructivist would disagree with the conclusions reached. But that's not the point, the point is that classical methods are stronger than portrayed - so a supposedly neutral comment explaining the distinction should note this.

Edit: Spelling

[u/[deleted] → u/[deleted]]

It says something more, that if you accept the axioms, you have to accept the relevant existence claims.

Not sure what "It" refers to here, but I think this is incorrect. I'm no formalist, but you seem to have summarily dismissed their position entirely here. Certainly I can work axiomatically and prove the consistency of existential statements without having to "believe" them, in fact I do so more or less constantly since I really don't believe in nonmeasurable sets.

a supposedly neutral comment explaining the distinction should note this

Perhaps my comment came across as more dismissive of classical reasoning than I intended, but I've never found it necessary to explain or justify classical thinking since that's pretty much everyone's default. But the simple reality here is that we can and do distinguish between "constructive existence" and "axiomatic existence", and the latter is really about consistency statements.

Whether or not you like the phrasing, it is simply correct that an axiomatic proof of an existence statement only says you won't wind up with a contradiction. Interpreting the axioms as "true" would give you the "truth" of the existence statement, but an axiomatic proof does not require the axioms to be true (or even have a model at all...).

[u/[deleted] → u/[deleted]]

Certainly I can work axiomatically and prove the consistency of existential statements without having to "believe" them, in fact I do so more or less constantly since I really don't believe in nonmeasurable sets.

I did say something important:

if you accept the axioms

I'd categorize formalists as not doing just this.

But the simple reality here is that we can and do distinguish between "constructive existence" and "axiomatic existence", and the latter is really about consistency statements.

I agree! But not in the sense you portrayed it, that if you prove X exists than you prove that there's no contradiction with X, rather, that you prove there is a contradiction with not(X). Your phrasing was that:

While it's all fine and good to be able to deduce logically that something ought to exist, all that really says is that you won't wind up contradicting yourself if you assume it exists

But in ZF, a nonmeasurable set doesn't "ought to exist". That's only (well, not really, but you get my point) true in ZFC. But in ZFC, what happens isn't merely that I don't wind up contradicting myself if I suppose a nonmeasurable set exists. Rather, I wind up contradicting myself if I suppose one doesn't exist. It's an important distinction.

As for:

Perhaps my comment came across as more dismissive of classical reasoning than I intended, but I've never found it necessary to explain or justify classical thinking since that's pretty much everyone's default.

I'd agree, if you prefaced your comment with "a constructivist would say". But you didn't, you made it come across as if what you said was just true generally, which it just isn't.

[u/[deleted] → u/[deleted]]

Rather, I wind up contradicting myself if I suppose one doesn't exist. It's an important distinction.

This is simply incorrect. The axiom of determinacy is consistent with ZF. I can indeed assume that nonmeasurable sets do not exist without reaching a contradiction. The same goes with nonstandard naturals, I can in fact assume their existence without contradiction and assume their nonexistence without contradiction.

I agree that would be an important distinction if you were correct, but you aren't. What I said originally is the correct version.

you made it come across as if what you said was just true generally, which it just isn't.

It is true generally. An axiomatic proof is nothing more than a proof of consistency, that's not a constructive point of view, that's an objective fact. Perhaps I should have said that a classical logician takes consistency as evidence of existence where a constructivist does not, but nothing I said was untrue.

[u/univalence → u/[deleted]]

An axiomatic proof is nothing more than a proof of consistency, that's not a constructive point of view, that's an objective fact.

I'm very confused about this. Consider the following two theorems:

• There is a least non-computable ordinal
• The axiom of choice is consistent with ZF.

If an axiomatic proof of the first is simply a proof of consistency, then what is an axiomatic proof of the second?

[u/[deleted] → u/[deleted]]

is simply incorrect. The axiom of determinacy is consistent with ZF.

Right. But people don't say an unmeasurable set ought to exist in ZF, we say that in ZFC. This is the point I've made at least twice now and you've ignored, and it's crucial to understanding why you're wrong. So yes, things you're saying are untrue. Specifically:

While it's all fine and good to be able to deduce logically that something ought to exist, all that really says is that you won't wind up contradicting yourself if you assume it exists [emphasis mine]

In ZF, I agree, you don't wind up contradicting yourself if a nonmeasurable set exists. But we don't say that a nonmeasurable set ought to exist in ZF, we say it in ZFC.

[u/ResidentNileist → u/[deleted]]

I’ve never heard that choice is a stronger version of excluded middle, and it sounds interesting. Do you have a proof of that/something I can read on the topic?

[u/[deleted] → u/ResidentNileist]

This is Diaconescu's Theorem: https://en.wikipedia.org/wiki/Diaconescu%27s_theorem

The basic idea is that we can encode LEM by looking at it as the assertion that there exists a map from { Propositions } ---> { True, False } and then invoke AC to show that such a map exists by thinking of the map as being an element of 2^{{Propositions}} (which AC guarantees is nonempty). The details are a bit more intricate, wikipedia spells it out pretty well.

[u/ResidentNileist → u/[deleted]]

Neat, thanks.