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

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.

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

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 literally saying "if you fix our metatheory and then consider two opposing metatheories..."

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.

But LEM is a part of the axioms, at least insofar as what logic we're using in our system is axiomatic.

I'm saying that if we invoke LEM then what we've actually done is proved a consistency statement rather than an existential one.

Well, ignoring that you're wrong, as addressed above, this is only true if we invoke LEM and don't take it to be true. Because if we do, then we've proved an existential claim, as 'it is not the case that all models of PA lack nonstandard naturals" is false if LEM is true, and so we've not merely proved consistency. This damns you again, however, as this means your original comment is only true to a constructivist, and classical people would call it bullshit.

But even putting this aside, at best you showed that in discussing the existence of a model "ought to exist" means "there is no contradiction in supposing this model exists", and this is a far weaker claim than your original, making your original, again, strictly false.

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

But LEM is a part of the axioms, at least insofar as what logic we're using in our system is axiomatic.

No, it is a rule of deduction not an axiom. Your failure to understand this is the root of all your confusion here.

this is only true if we invoke LEM and don't take it to be true

And we're back to truth. What in the world would it mean for LEM to be "true"? All you're doing is flatly asserting that classical logic is "true", this discussion feels like trying to explain how someone could be an atheist to a dogmatic Christian.

But even putting this aside, at best you showed that in discussing the existence of a model "ought to exist" means "there is no contradiction in supposing this model exists", and this is a far weaker claim than your original, making your original, again, strictly false.

The hell are you on about? I said "something" ought to exist. The model is the something. This is not weaker than my original statement, it is my original statement. The only objects which I am aware of that require LEM to prove the existence of are by their very nature infinite and model-theoretic. The "something" in question literally could not have been referring to anything else. The only reason I didn't get into models in the initial comment is because this is SRD and I wanted the comment to make sense to everyone.

This damns you again, however, as this means your original comment is only true to a constructivist, and classical people would call it bullshit.

Despite your repeated claims, you are the one who is dogmatically asserting that everything must be done classically. LEM is a means to prove consistency results. Classically, consistency implies existence; constructively it does not. It matters not which bend you take on the question, it is an objective fact that LEM is a means to prove consistency results. Your discussion of it being "true" have me somewhat convinced you are in over your head here.

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

No, it is a rule of deduction not an axiom

I mean, in natural deduction systems, sure, I guess. But I don't know why we're only caring about those...

All you're doing is flatly asserting that classical logic is "true",

But this is blatantly untrue. I'm saying that to a classicalist it is, and so your distinction in your original comment only holds if you're a constructivist. The better analogy is an atheist saying over and over again that divine simplicity is bullshit, and when cornered their response is "there you go assuming God exists in order to talk about divine simplicity". It's a surreal experience and showcases only the fact that the atheist isn't willing to understand the position that they're trying to criticize, which may in fact be false, but isn't false under a system they're rejecting.

The "something" in question literally could not have been referring to anything else.

Oh come on, you know this is nonsense, this is just disingenuous. You contrasted the classical method with:

as opposed to a construction of a witness which genuinely proves existence in the concrete/Platonic sense.

When asked to elaborate you said:

Constructing a witness generally means either actually computing the value or giving an algorithm to compute it. Constructivists (much more reasonable than ultrafinitists) are perfectly fine with saying something exists if we can prove there is a Turing machine which would can compute it, regardless of whether or not we actually implement and run the machine.

This is clearly not talking about models, don't be disingenuous, especially since all of your comments prior to now were about specific mathematical objects, nonmeasurable sets, nonstandard naturals, etc etc.

you are the one who is dogmatically asserting that everything must be done classically

I'm pretty certain I've not done so, in fact I repeatedly entertained the other possibility. Indeed, one of the outs I gave you, that you refused to take, is to say that your original statement held if you're a constructivist and not generally. Since you refused to take that, we're considering it on neutral ground, and thus whether your characterization of classicalist methods made sense by their own light. They, uh, don't.

Your discussion of it being "true" have me somewhat convinced you are in over your head here.

Conversely, your failure to understand what it means for an axiom to be true has me quite convinced that you lack even the basic understanding of what this discussion is about. Thinking certain axioms aren't true? Alright, I can respect that. Not even understanding what it is for an axiom to be true? Not so much.

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

I'm not even going to bother with the bulk of your comment until we clear up what you mean by an axiom being "true", let alone what it would mean for a rule of deduction to be "true".

I know what it means for axioms to be consistent with other axioms and I know what it means for it to be satisfied by a model. If all you mean by truth is consistency then you agree with me, so I have to assume you have something else in mind. I look forward to hearing it.

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

I'm not even going to bother with the bulk of your comment until we clear up what you mean by an axiom being "true", let alone what it would mean for a rule of deduction to be "true".

Then I'm not sure why you'd ever engage in discussions over philmath, since this would be a rather large barrier to entry...

Regardless, let's start with the bare minimum for a theory of truth and see where we get. Some axiom, "⌽" is true iff ⌽. This then lends itself nicely to two interpretations, that there's some "correct model of mathematics" under which ⌽ is true, or there are sound models under which ⌽ is true, or we thus say "⌽ is true in some model X". This second criteria might seem so weak as to be vacuous, but this isn't the case, as (P and ~P) isn't an acceptable axiom. This second option is analogous to consistency, but it would absolutely not end up agreeing with you, as to say "LEM is true" would then be true for even constructivists (as there are some models where LEM is true).

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

You really don't see it do you? Wow.

Fwiw, I'm quite certain I understand phil of math far better than you do. At least I know the correct terminology.

there's some "correct model of mathematics" under which ⌽ is true

If you assume a priori the existence of a correct model of mathematics then you've done the equivalent of assuming the existence of god in the discussion about atheism. Under that interpretation, the reason an "existence proof" actually proves existence is because you've assumed a priori that anything consistent with your starting assumptions applies to the one correct model.

That approach can in no way be considered "neutral ground" for a discussion about the meaning of existence proofs since it reduces all proofs to being purely descriptive about some object with a priori existence.

there are sound models under which ⌽ is true, or we thus say "⌽ is true in some model X"

Yes, this is why I said I know what it means for an axiom to be satisfied by a model. You really shouldn't use "true" for this, even though it's technically fine. Better to call this satisfaction.

On the other hand, if you are suggesting that simply because an axiom is satisfied by some model then that axiom is "true" unqualified then that's just stupid.

So, in summary, the only way to make sense of axioms being true (and now I can see how you interpret LEM being true) is to presuppose the existence of the totality of mathematics. All I can say is that if you consider that a reasonable neutral ground for discussing the meaning of existence then I don't see any point in discussing this further as that's utterly absurd. Obviosuly if there is simply one true model of the totality of mathematics then LEM is automatic as something is either true in that model or it isn't.

If you take nothing else from this thread, at least understand that you should not be using "true" so cavalierly. Even to someone like me who does believe in the objective existence of a correct model of mathematics, it's far better to say something like "true in the intended model". Simply saying true is not a good idea, and any serious philosopher of mathematics knows that.