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?

[pbrane.livejournal.com]

How about Cantor's Continuum Hypothesis: in ZFC, the statement: "There exists no set whose cardinality exceeds that of the integers, but is strictly less than that of the continuum". Is undecidable.

[gustavolacerda.livejournal.com]

Not concrete enough for me. Once your objects start getting infinite, I get skeptical of their "objective existence".

[pbrane.livejournal.com]

Hmm... I bet you it's not hard to prove that any undecidable statement in number theory will deal with the infinite. Math is *about* the infinite. Finitude is boring. :P I'm only be a little bit facetious.

And what does "objective existence" mean, in the realm of formal mathematics, pray tell?

[spoonless.livejournal.com]

Indeed... Godel's Incompleteness Theorem only applies to systems with "second order logic"... systems which can make statements not only about their elements, but also about sets of those elements.

It seems to me that any statement about a finite set can be expanded out as a finite sequence of statements about the elements of the set. In which case, a system is only irreducibly second order if it makes statements about infinite sets. (I'm inserting my own word "irriducibly" here just to mean, "not reducible to first order").

Then again, I've never actually seen this claimed anywhere, so maybe there are some pathological cases where my reasoning isn't right. But it seems like a reasonably solid argument.

[spoonless.livejournal.com]

uh... sorry about that. Guess I have no idea what I'm talking about here. :(

[gustavolacerda.livejournal.com]

hmm... I actually believe that the Godel sentence translates to a statement about finite mathematics. I think the encoding itself forces all those sentences to be about finite numbers... references anyone?

[bram.livejournal.com]

The Godel sentence has a "there exists" in it. In that sense it's not about finite mathematics.

[gustavolacerda.livejournal.com]

ok.
But in any case, I consider some existential statements, for example, the Goldbach conjecture as concrete enough: if there exists a counterexample, then a finite number theoretical fact holds. If there exists no counterexample, then the conjecture is true.

Whereas the existence of a set of intermediate cardinality sounds very abstract, and it's not the kind of result I would demand out of a theory arithmetic.

I feel like we should find a complete axiomatization for all statements like the Goldbach conjecture. Yet, I know it's likely that this is impossible.

[bram.livejournal.com]

The infinite has its share of paradoxes: Zeno's paradoxes (fallacies really), Russell's paradox.

So Hilbert dreamed that you could prove anything, even if it had to do with the infinite, even if it had a "there exists" that could only be verified by checking an infinite number of cases, by a finite proof.

If arithmetic could be proved to be consistent and complete, any proposition could be proved or its converse could be proved in a finite number of steps, and the infinite would not be needed.

That's what Godel demolished and that's why I think what he did is important.

"Statements like the Goldbach conjecture"-->what do you mean precisely? Simple statements? Statements shorter than a certain length in symbols?

[gustavolacerda.livejournal.com]

I mean concrete enough statements.

I consider Goldbach concrete because there either there exists a counterexample or there doesn't (even though there are an infinite number of cases), and if it does it's simple to check it. In other words, either it is true or it isn't, independent of which foundational system you choose. And I would expect any foundational system to decide all statements like this.

Statements like CH, though, talk about much more abstract objects, whose "existence" I consider doubtful, for example the set of the so-called "real" numbers.

By "existence", I don't mean actual existence, but rather "concreteness". My definitions are circular, since my ideas on this are still philosophical.

I guess what I want to find is a "decidable fragment" of arithmetic, which would include concrete things like Goldbach, but not necessarily things like CH.

Do you see what I'm getting at?

[bram.livejournal.com]

If I see correctly what you are getting at, what you really want is a retraction of Godel's Theorem! Which I don't think is going to happen.

[gustavolacerda.livejournal.com]

do you know Presburger Arithmetic? I wonder how far we extend it before being forced into undecidability.
My hope is that there exists a decidable arithmetic which can express statements of the form of the Goldbach Conjecture.

[gustavolacerda.livejournal.com]

here's the correct link: http://en.wikipedia.org/wiki/Presburger_arithmetic

[bram.livejournal.com]

Thanks. I had never heard of this before. By making your system weaker you get around Godel's theorem but, well, you make your system weaker.

[rdore.livejournal.com]

The Whitehead problem is independent of ZFC, to add one more thing to those already listed.

[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.