[cryvate1284]

You aren't very explicit what you mean, but I disagree I think.

The main thing is willing things into existence (like ZFC, the Axiom of Choice) is equally consistent with not having it (ZF + not AC) or not deciding it (ZF) as shown by forcing.

Russel's Paradox in particular was worked around by not allowing to "build sets" quantifying over all sets (see axiom schema of specification).

If you are talking about avoiding "unprovable statements" (i.e. Godel's incompleteness theorem), you have to strip things way back further: it applies to systems that only have e.g. Peano arithmetic. An actual practical statement that is unprovable in Peano arithmetic is Goodstein's theorem: - write out a number in its base 2, including its exponents (i.e. recursive) - replace all the 2s with 3s - subtract 1 - write out a number in base 3, including its exponents - replace all the 3s with 4s - subtract 1 - ... The question is whether for all starting numbers this sequence eventually ends at 1. The answer is yes, trivially if you use ordinals (and replace all your base numbers with omega: the +1 will basically do nothing and -1 means it must be finite because ordinals well-ordered), but this cannot be used in Peano arithmetic.

Fundamentally, like Paris-Harrington Theorem, I think the way to think about why this cannot be proved, is because these sequences get big before they end up at 1.

[lupire]

A better example is the "real" numbers, which do not physically exist but are a constant source of theorems that don't apply to physics, and this is taken as proof that real numbers are a fascinating complex object, instead of a poor foundation for analysis. Standard Mathematics does not use a good model for infinitesimals, which should not be allowed to be densely non-differentiable.

[raverbashing]

Yep, this is a good example. And maybe it helps illustrating my point

On N and Q we can come up with any number we want. Even though there are infinite numbers, we can come up with any number

On R we can do that as well. But at the same time we can come with "vapid" statements like "for each x in R exists x' < x" which are completely correct but don't really mean anything.

True, the R's are a good foundation, and in a way they do exist physically (after all, Pi exists in nature).

[raverbashing]

Thanks for your answer, I didn't know about Goodstein's theorem

> Russel's Paradox in particular was worked around by not allowing to "build sets" quantifying over all sets (see axiom schema of specification).

Ah I didn't know that by name but this is pretty much the gist of what I'm getting.

ZFC and AC, while Axioms, seem like a better foundation than something that allows "set of all sets" which sounds like a vague specification even for a mathematician. And in the end, Russel's paradox raises the exact issue of (pardon my non-mathematical language) "Set of all sets is BS"

Hence the axiom of specification which lets you build sets that exist.

I'm not talking about Gödel or unprovable statements, because even if something is not provable it might be constructable.

[yakubin]

> I'm not talking about Gödel or unprovable statements, because even if something is not provable it might be constructable.

What precisely do you mean by that statement? What is the thing that is not provable but constructible? A conjecture? If so, then what do you mean when you say that a conjecture is constructible? What does it mean to construct it?

As far as I know, "construction" in maths usually means a finite process. And proofs are finite sequences of strings, satisfying certain rules specified by a proof framework (such as sequent calculus). So I'm curious in what way something could be constructible, but not provable. To be honest, I don't understand how those words could apply to the same things, because proving usually applies to conjectures, statements, formulas etc. But constructing usually applies to definitions and proofs, which cannot said to be true or false at all.

[raverbashing]

> What is the thing that is not provable but constructible?

Just look at the grandparent message for an example: "An actual practical statement that is unprovable in Peano arithmetic is Goodstein's theorem"

Or proving the Collatz Conjecture. You need only basic algebra to build it, but something much more complex to prove it (if it is provable)

[guimplen]

>I'm not talking about Gödel or unprovable statements, because even if something is not provable it might be constructable. >Or proving the Collatz Conjecture. You need only basic algebra to build it, but something much more complex to prove it (if it is provable)

It seems like your first statement is about constructibility of the same object (that should be a proof). In your second statement you talk about constructibility of an object and provability of a certain statement about an object. I may be be judgemental, but being so imprecise is a big no-no in metamathematics.