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