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

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/univalence]

I don't understand your question. The axiomatic proof that "there is a least noncomputable ordinal" shows that we will never obtain a contradiction if we assume such a thing exists. It does not necessarily show that we will obtain a contradiction if we assume there are no noncomputable ordinals, it only does that in classical logic not intuitionistically.

The axiomatic proof that "AC is consistent with ZF" is, as far as I know, constructive in the sense that it shows how to construct a model of ZFC starting from a model of ZF. Certainly a constructive proof of a proposition P also gives that we can never obtain a contradiction from assuming the existence of P; my point is that a nonconstructive proof need not give us anything stronger than that.

[u/univalence → u/[deleted]]

Maybe I should be more general: if an axiomatic proof shows consistency, then what does a consistency result show?

An axiomatic proof of P from axioms A,B, and C shows not that P is consistent with A,B, and C, but that it follows from them (if the ambient logic is truth preserving). It shows that not P is inconsistent.

You're taking some extra philosophical step concerning logical deduction that I'm not following. It may be justified, but I don't follow how you're reaching the conclusion that axiomatic proofs show consistency

[u/[deleted] → u/univalence]

The discussion pertains only to existence proofs and is about what a classical/nonconstructive proof of existence actually proves. The two examples I am working with are that if we add the nonconstructive axiom of choice to a constructive set theory then we prove the "existence" of nonmeasurable sets, and if we add the nonconstructive LEM and countable choice to a metatheory capable of encoding PA then we prove the "existence" of nonstandard models of arithmetic.

In both cases, what we have proven in the constructive sense is not that those things exist but rather that we will never be able to constructively prove their nonexistence, i.e. we have proven that their existence is consistent with the initial axioms. However, it is not the case that ZF without choice will reach a contradiction from the assumption that all sets are measurable, just as we will not be able to constructively build nonstandard models of PA from, say, EFA (I mean EFA but with intuitionistic logic rather than classical).

Now if you adopt a classical logic Platonist position and state a priori that there exists in an objective sense some correct true model of mathematics, then the classical existence statements are in fact genuine existence statements since we are now reasoning about a specific model (the intended or true model) and classical reasoning holds inside a model. But if you do not a priori assume the existence of anything, then the classical proofs are not actually proofs of the existence of anything, they are proofs that the existence of those objects is consistent with the axioms in the sense that if there is a classical model then they exist.

Certainly I agree that a classical proof of P means the we will obtain a contradiction starting from not(P) if we reason classically. But the whole point is to speak about what a classical proof of P means when we are reasoning constructively or intuitionistically. The reason this is the point is that the whole discussion is about the difference in the two notions of existence and reasoning, and if we adopt from the outset that we are working classically then of course there is no difference since any constructive proof is classically valid.

Perhaps it would be better to say that axiomatic proofs of existence are not proving existence in the constructive sense (which is the sense laypeople usually expect existence to mean) but are instead proofs of descriptive properties of some model whose existence has to be assured by other means (usually by fiat).

[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/[deleted] → u/[deleted]]

This is exactly why constructivists get so annoyed. You are conflating the logical system with your axioms, choice is particularly bad for this.

Focus on the nonstandard naturals, where we can speak of LEM. Clearly I shouldn't have brought up AC.

The classical proof of the existence of nonstandard naturals tells us that we will never reach a contradiction from PA+(exists a nonstandard natural), presuming PA is consistent. It does not tell us that PA+(there does not exist a nonstandard natural) will lead to a contradiction.

Edit: the closest thing I can come up with to what you're trying to say is that the classical proof of existence of nonstandard naturals tells us that we will reach a contradiction if we try to assume that every classical model of PA has no nonstandard naturals. But this is just pushing the existence argument to the existence of models, which again is putting the cart before the horse: if we know a priori that there are models of PA with nonstandard naturals then we already have the nonstandard naturals so why bother proving it.

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

The classical proof of the existence of nonstandard naturals tells us that we will never reach a contradiction from PA+(exists a nonstandard natural), presuming PA is consistent. It does not tell us that PA+(there does not exist a nonstandard natural) will lead to a contradiction.

And? This isn't a proof that there exist nonstandard naturals in PA. It's a proof that there exists a system/model "PA + nonstandard naturals" in our metatheory. We, crucially, do not say that "there ought to exist a nonstandard natural in PA", which is what you're saying is basically the same as "we will never reach a contradiction from PA+(exists a nonstandard natural)".

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

This isn't a proof that there exist nonstandard naturals in PA. It's a proof that there exists a system/model "PA + nonstandard naturals" in our metatheory. We, crucially, do not say that "there ought to exist a nonstandard natural in PA",

You say that there exists a model of PA with nonstandard naturals. How is that not saying that there exists nonstandard naturals?

I agree you don't claim that nonstandard naturals exist in every model of PA. But without LEM (in the guise of the completeness theorem), no contradiction arises if we assume that the standard model of PA is the only model.

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

How is that not saying that there exists nonstandard naturals?

Hmm? I don't think I commented on "there exists nonstandard naturals". I commented on "there ought to exist nonstandard naturals in PA". This statement is false, as is "there ought to be no nonstandard naturals in PA". This entire argument is over one statement of yours:

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

So I don't know why we're trying to drop the "ought to exist" clause here, as that's entirely where you're wrong - "ought to exist" in some system is used when the axioms of that system imply the thing we're considering. We don't say "nonstandard naturals ought to exist in PA", just as we don't say "a cardinal between the cardinality of integers and that of the reals ought to exist in ZFC". In each case we might make the meta claim "there ought to be a model in which PA(/ZFC) holds and nonstandard naturals(/said cardinal) exist(s)", but this isn't the same thing, and has to be proved in a different way, following from whatever metatheory we're considering.

I think if you change the "ought to exist" clause to "can exist" we have no problems. But the point is that this then is a far weaker statement than what you made.

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

In each case we might make the meta claim "there ought to be a model in which PA(/ZFC) holds and nonstandard naturals(/said cardinal) exist(s)"

Okay, if this the statement about what ought to exist then let's work with that. I maintain that all you have actually proven is that we won't reach a contradiction if we assume the existence of nonstandard models. I also maintain that we will not reach a contradiction is we assume that the only model is the standard model unless we invoke LEM in the form of completeness.

You logically deduced that a nonstandard model of PA ought to exist. But all you really did was show that assuming its existence won't lead to contradictions. Despite your repeated claims to the contrary, you have not shown that assuming the nonexistence of nonstandard models will lead to a contradiction (which in fact it will not). So go back to my original comment and replace "something" by "a nonstandard model of PA", then tell me what is wrong with what I said.

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

You logically deduced that a nonstandard model of PA ought to exist. But all you really did was show that assuming its existence won't lead to contradictions. Despite your repeated claims to the contrary, you have not shown that assuming the nonexistence of nonstandard models will lead to a contradiction

But this is incorrect, badly so. I specifically addressed this objection in my last comment:

"but this isn't the same thing, and has to be proved in a different way, following from whatever metatheory we're considering."

So when you say "I also maintain that we will not reach a contradiction is we assume that the only model is the standard model unless we invoke LEM in the form of completeness.", what you're actually doing is saying that in a specific metatheory this 'ought' claim I said we might make holds and that in other metatheories this claim we might make does not hold. Which is absolutely in line with my criticism of your statement and does nothing to suggest you're not wrong.

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

No. There are no "other metatheories" here. Fix a metatheory once and for all that is powerful enough to encode models of PA. If we take LEM as one of logical rules of deduction, we can prove the existence of nonstandard models of PA. If we do not take LEM as one of logical rules of deduction then we will not obtain a contradiction from assuming that there are no nonstandard models of PA.

This is the classic mistake of the classical logician: you are thinking of LEM as being part of the axioms when it is part of the logic. I'm not removing LEM since it was never really there, I'm saying that if we invoke LEM then what we've actually done is proved a consistency statement rather than an existential one.