more ignorant logic speculation

[gusl]

So, I've been thinking, how significan't should Gödel's Incompleteness be anyway? It seems those example sentences are always pretty contrived, whereas I only really care about "concrete" statements.

Give me an example of a concrete-looking undecidable statement in number theory.

Should we replace the ideal of static axiomatization with a dynamic one? Can there be an algorithmic way of picking new axioms? Would this create a logic on its own, which also suffers from Gödel's Incompleteness?

Chaitin views Gödel's incompleteness as an information-theoretic necessity.


Does the undecidability of FOL imply that there are no bounds on proof size?

Comments

[bram.livejournal.com]

There are ways of generating the undecidable propositions without the self-reference.

I learned one neat new thing a couple of years ago: Rosser's Theorem. It's a version of Godel's theorem that does away with the "omega-incompleteness." That is, Godel's theorem says there are undeciable propositions of the form "there does not exist such a number" where that number codes via Godel-numbering for the proof of the proposition itself (i.e. "I can't be proved.")

BUT is the proposition TRUE?

IF it is, you can still CONSISTENTLY add its converse. There DOES exist such a number satisfying such a relation. And yet you can prove 1, 2, 3, etc. individually do NOT satisfy the relation. So the converse basically introduces an "ideal element" separate from the normal integers.

However, this violates "omega consistency". If you care about omega consistency, the Godel proposition is better than its converse.

Rosser's theorem has an undeciable proposition WITHOUT such a form. Basically the Godel's numbered translation of the proposition is "For every proof of me there is a shorter proof of my negation".

I think Godel's theorem is vastly important whether or not simple propositions are undecidable, but who knows? The Goldbach conjecture or the twin primes conjecture could be undecidable.