undefined

points

[-]

That is also not how it works. The theorem says that there exist some true statements for which there is no proof. This is assuming the axioms are consistent.

by skew-aberration8 hours ago|

parent|

[-]

I think you're right, I'm conflating two separate things.

EDIT: I am wrong (it's been a while) but there is nuance.

I said any computer program fails to prove some true statements. In fact, some 'true' statements cannot be proven by any program, as others have said.

But for those statements G, you can prove 'G is true if our system is consistent', just not 'G is true'.

So when we say G is 'true', we are really just asserting the consistency axiom that our computer program is denied.

by rcpt9 hours ago|

prev|

[-]

Godel says that there are statements that are true but have no proof within that system. It's not about algorithms.

I'm saying it'd be funny if Riemann were true but not proveable.

Though I guess it's actually funnier. If Riemann were false then there would be a counterexample, so it's clearly within existing axioms.

So if one can prove that Riemann isn't proveable in our current axioms then it has to be true.

by plagiarist8 hours ago|

parent|

[-]

Can something be both true and unprovable without being a self-referential Godel sentence? I assume most statements that aren't self-referential are independent, like the continuum hypothesis with ZFC.

by skew-aberration8 hours ago|

parent|

[-]

Godel sentences are only true if you assume consistency. And once you add that axiom, the computer can prove them too.

G is independent of your original system T (cannot be proven true or false).

If you create T+ with added consistency axiom, then G is true and provable.

But G is never true and unprovable in the same system.

It's a lot like is/ought or theology.