There exists a concrete polynomial [math] P in mathbb{Z}[x_1,ldots...

There exists a concrete polynomial [math] P \in \mathbb{Z}[x_1,\ldots,x_9] [/math] (aka a polynomial of 9 variables with integer coefficients) such that the statement "There exist integers [math] m_1, \ldots, m_9 [/math] such that [math] P(m_1,\ldots,m_9) = 0 [/math]" is formally undecidable, i.e. neither provable nor disprovable in ZFC.

Furthermore, given any extension of ZFC, there will exist a polynomial with the same property with respect to it.

How does this make you feel? That something so concrete can be undecidable?

Other urls found in this thread:

projecteuclid.org/euclid.bams/1183547548
en.wikipedia.org/wiki/List_of_undecidable_problems#Problems_about_matrices
en.wikipedia.org/wiki/List_of_statements_independent_of_ZFC
twitter.com/NSFWRedditVideo

It makes me wonder why exactly 9. Is it the lowest dimensionality for which that is true? I also doubt it's truthfulness. Have any sources?

Prove your claim.

It doesn't make me feel anything without seeing how this claim arises. Not interested in being parroted results.

It's a consequence of the resolution to Hilbert's 10th problem.

It comes down to that one can write down a polynomial all of whose tuples of integer solutions together encode a formal proof of the consistency of ZFC.

projecteuclid.org/euclid.bams/1183547548

I don't think the 9 in particular is significant.

That also means that there aren't any roots, at least in the standard model of numbers.

Otherwise, it would be a very easy proof that the roots exist- just put them in the polynomial.

I call bullshit.

1. Plug in some arbitrary numbers for x_2, x_3, ..., x_9.
2. Now you got a polynomial in one variable. Use fundamental theorem of algebra to assert existence of roots.

There's a root, but it won't necessarily be an integer.

>a polynomial of 9 variables
(a+1)(b+1)(c+1)(d+1)(e+1)(f+1)(g+1)(h+1)(i+1)
abcdefghi+abcdefgh+abcdefgi+abcdefhi+abcdeghi+abcdfghi+abcefghi+abdefghi+acdefghi+bcdefghi+abcdefg+abcdefg+abcdefh+abcdegh+abcdfgh+abcefgh+abdefgh+acdefgh+bcdefgh+abcdefh+abcdefi+abcdefi+abcdegi+abcdfgi+abcefgi+abdefgi+acdefgi+bcdefgi+abcdegh+abcdegi+abcdehi+abcdehi+abcdfhi+abcefhi+abdefhi+acdefhi+bcdefhi+abcdfgh+abcdfgi+abcdfhi+abcdghi+abcdghi+abceghi+abdeghi+acdeghi+bcdeghi+abcefgh+abcefgi+abcefhi+abceghi+abcfghi+abcfghi+abdfghi+acdfghi+bcdfghi+abdefgh+abdefgi+abdefhi+abdeghi+abdfghi+abefghi+abefghi+acefghi+bcefghi+acdefgh+acdefgi+acdefhi+acdeghi+acdfghi+acefghi+adefghi+adefghi+bdefghi+bcdefgh+bcdefgi+bcdefhi+bcdeghi+bcdfghi+bcefghi+bdefghi+cdefghi+cdefghi+...+1

Oh, sorry. I didn't see the word "integers".

lmao

Any reason why it has to be 9 variables and not 8 or 7?

Yes, Con(ZF) implies there aren't any roots. But then there also exists a polynomial for ZF+Con(ZF); for that you need Con(Con(ZF)). And so forth, up the large cardinal hierarchy if you like. Who really knows what the true model of arithmetic looks like. Does it contain no proof of the inconsistency of a Berkeley cardinal? We don't even have intuition for this.

Just a matter of the encoding schema.

Well that's not really surprising at all.

A recurring theme with mathematics is that almost all solutions involving integers only are impossibly hard to deal with, just look at diophantines.

Yeah no, I like math, but not enough to go graph that

Im perhaps not a genius, like you all are on Veeky Forums (no sarcasm intended)

But thats greek to me. I was never any good in math :(

Read a book.

So what is this concrete polynomial? Why don't you tell us?

The integer coefficients are too big.

I suppose you could have just used
a*b*c*d*e*f*g*h*i
but it would have been less fun.

See the link posted
It has a very large degree, through the article has some fairly simple polynomials that do the job.

how big?
Is this related to the singular-ness of a 3x3 matrix with integer components? I seem to recall something like that.

Are you serious bro? I'm an undergrad CS dropout and I understand the premise. There exists a nine-variable polynomial P such that it is undecidable (it is formally impossible to compute if it is true or false) if there are solutions to P=0 using only integers as input.

What said, read a fucking book.

>with integer coefficients
He could have just used abcdefghi, but it wouldn't be representative of the number of terms of a polynomial that satisfies the given condition.

First of all, if you look at the article, it has degree [math]10^{45} [/math].

Although there also exists a diophantine equation in 58 unknowns, and of degree 4, with the desired property. The article doesn't say how big the coefficients are, but considering it's stipulating an encoding of a formal proof, the coefficients are almost certainly enormous (like Godel encodings, powers of powers of powers).

No need to be mean to him. You can tell someone to read a book as friendly advice without being derisive. Or maybe I've forgotten where I am.

Ok OP, suppose I take your concrete polynomial P, and stick in k for each m_k (for example), and find that P evaluates to zero. Then I have decided, no? I have proven such a collection m_k exists.

So if you are saying that this can't happen, no matter what choice I happen to make for the m_k, then you are telling me that there is no such collection. Thus we have again decided!

Checkmate athiests!

See: We CAN prove that no roots exist, but the proof is meta-mathematical. We can't prove it within the ZFC axioms.

These equations are so big that in addition to the nearly-zero probability of choosing correct coefficients, evaluating P with one combination of coefficients cannot be done in your lifetime.

Not exactly. You can prove that relative to Con(ZF), there is no solution. And Con(ZF) is almost certainly true, but is not a proven consequence of ZF (and assuming Con(ZF), of course, it is unprovable from ZF).

Mathematical theorems, even in set theory, are consequences of ZF or ZFC.

If you found integers like that, you would have proven that ZF is inconsistent. There goes mathematics.

en.wikipedia.org/wiki/List_of_undecidable_problems#Problems_about_matrices

That's undecidability in computability theory. Very different from OP, and relatively unremarkable.

OP is about the proof-theoretic independence of a single concrete proposition.

>and relatively unremarkable.
That's a weird thing to say.

It also struck me as odd that OPs issue would actually just be undecidable in ZFC.

There is, anyway, also a page of independence of ZFC. I'm of the opposite opinion of you, thought. ZFC is an "arbitrary" far too strong formal theory, so whatever happens there, whatev's

en.wikipedia.org/wiki/List_of_statements_independent_of_ZFC

Something is a mathematical theorem iff it is a consequence of ZF(C).

In almost any field of mathematics, every axiom is used except regularity, and regularity doesn't make the theory stronger.

A: You can't decide this problem!
B: What if I happen to find an integer root?
A: Aha! But there are no integer roots!!
B: Ok.... then I've decided.
A: But you haven't decided using these axioms!
B: ... and why the hell should I care?

>B: What if I happen to find an integer root?
Humanity would go extinct before managing to test your God-given solution for correctness.

>A: Aha! But there are no integer roots!!
Incorrect.

If ZFC is consistent there are no integer roots. Unless ZFC is inconsistent there is no proof of its consistency.

Because I believe ZFC is consistent, I believe there are no integer roots. But if you believe there are, you believe ZFC is inconsistent.

What is relation between computational undecidability and axiomatic undecidability. Is one subset of other.

>hurr muh axioms
literally who cares except autistic set theorists?

The axioms literally determine what is a mathematical theorem and not. They define provability.

Is there either a proof or disproof of the Whitehead problem from abstract algebra? No, because it's independent of ZFC.