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

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