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

"concrete"

[jozefpronek.livejournal.com]

The Paris-Harrington theorem displays a quite concrete sentence that is independent of PA, yet true in the standard model of arithmetic. The sentence is a fact in combinatorics. What could be more concrete?

There is also a similar (much more difficult to prove) theorem for ZF, due to Harvey Friedman.

Re: "concrete"

[gustavolacerda.livejournal.com]

This "standard model" is what I'm interested in!
It will certainly have its undecidable sentences. Why do we extend PA in this way, as opposed to other possible consistent ways? Just because it corresponds to existing mathematics and/or our intuition?

I've once read that writing a grammar for a natural language is a neverending project: you're always making little adjustments to fit the language as it's really used.

Is this analogous to extending theories of arithmetic? Always more closely approximating what's "really true"? But in math, how do we know what's really true?