3 ms·

OK, the way I'd figure it out is: for such a polynomial, you definitely can't find those integers. There isn't any concrete m1...m9 satisfying the condition. Th

OK, the way I'd figure it out is: for such a polynomial, you definitely can't find those integers. There isn't any concrete m1...m9 satisfying the condition. The stumbling block is you can't find a proof for this fact in ZFC. But this seems to go against the idea that for any proposition independent from an axiom system, there is a model of the axiom system where that proposition is true and another where it is false. Someone enlighten me (not sarcastic).

dodobirdlord 7y ago
> OK, the way I'd figure it out is: for such a polynomial, you definitely can't find those integers. There isn't any concrete m1...m9 satisfying the condition. The stumbling block is you can't find a proof for this fact in ZFC. If this were formalizable it would be a proof. I encourage you to read through the excellent piece on the busy beaver function and computability. It's not entirely related, but it's fun! And it touches on the same theme as your question here, that human intuition about mathematics is weak. The writeup describes and proves the non-computability of a particular function of positive integers with definite (but non-computable!) value. https://www.scottaaronson.com/writings/bignumbers.html https://www.scottaaronson.com/writings/bignumbers.html
- Dylan16807 7y ago
  > If this were formalizable it would be a proof. A proof, but not a proof that can be expressed inside ZFC.
  - dodobirdlord 7y ago
    Obviously, the original statement has been proved to be independent from ZFC.
OscarCunningham 7y ago
You're right that if ZFC is consistent then it has a model in which this polynomial has an integer root. The issue is that the "integers" in the model are different from the actual integers. So you can't take the root out of the model and use it to prove ZFC inconsistent.
- joe_the_user 7y ago
  That is certainly how I would understand the situation. However, it seems intuitively you construct the notion of finite, could engage in the ordinary computation and have a way of distinguishing these "weird roots" from regular roots. I suppose if you make the position of (something like) "every polynomial whose root cannot be found by finite calculation does not, in fact, have one" an axiom but then you would have discarded the notion of finite axioms (you'd have a second order system). Still, might actually have a way to specify "truth", something I'd thought was a bit beyond logic at this point.
  - OscarCunningham 7y ago
    You might be interested in https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theo....

dodobirdlord 7y ago

> OK, the way I'd figure it out is: for such a polynomial, you definitely can't find those integers. There isn't any concrete m1...m9 satisfying the condition. The stumbling block is you can't find a proof for this fact in ZFC. If this were formalizable it would be a proof. I encourage you to read through the excellent piece on the busy beaver function and computability. It's not entirely related, but it's fun! And it touches on the same theme as your question here, that human intuition about mathematics is weak. The writeup describes and proves the non-computability of a particular function of positive integers with definite (but non-computable!) value. https://www.scottaaronson.com/writings/bignumbers.html https://www.scottaaronson.com/writings/bignumbers.html

Dylan16807 7y ago
> If this were formalizable it would be a proof. A proof, but not a proof that can be expressed inside ZFC.
- dodobirdlord 7y ago
  Obviously, the original statement has been proved to be independent from ZFC.

OscarCunningham 7y ago

You're right that if ZFC is consistent then it has a model in which this polynomial has an integer root. The issue is that the "integers" in the model are different from the actual integers. So you can't take the root out of the model and use it to prove ZFC inconsistent.

joe_the_user 7y ago
That is certainly how I would understand the situation. However, it seems intuitively you construct the notion of finite, could engage in the ordinary computation and have a way of distinguishing these "weird roots" from regular roots. I suppose if you make the position of (something like) "every polynomial whose root cannot be found by finite calculation does not, in fact, have one" an axiom but then you would have discarded the notion of finite axioms (you'd have a second order system). Still, might actually have a way to specify "truth", something I'd thought was a bit beyond logic at this point.
- OscarCunningham 7y ago
  You might be interested in https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theo....