Re: proving that a statement is undecidable


"Bennett Haselton" <bennett@xxxxxxxxxxxxx> wrote in message news:b5f030f8-674b-4249-99c0-0706d39242b4@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
I'm confused by statements that a given proposition has been proven
undecidable within a given set of axioms, and wondered if there are
some types of statements that we know, from looking at them, can never
be "proven undecidable", and other types of statements that could
potentially be proven undecidable.

For example, it seems like you could never use Zermelo-Frankel axioms
to prove that the Goldback Conjecture is undecidable within ZF.
Because if you do, then you would have this contradiction:
1) ZF can be used to prove that GC is undecidable in ZF.
2) Therefore, ZF can be used to prove that you can never find a proof
of GC in ZF but you can never find a counterexample either.
3) In particular, ZF can be used to prove that you can never find a
counterexample of GC.
4) Therefore, ZF can be used to prove that GC is true, i.e. you can
never find a counterexample.
5) This contradicts statement #1 that ZF can't prove or disprove GC.

The conclusion seems to be that, while you don't know if GC is true,
false, or undecidable in ZF, you know that certainly can't *prove* in
ZF that it's undecidable. (Is this correct? If it's wrong, where?)

On the other hand, Paul Cohen proved that the Continuum Hypothesis is
undecidable within ZF. What is it about CH that makes it the kind of
statement that can be proven undecidable, while GH is not?

Bennett

I am not an expert in this at all, but I will have a go.

Undecidable in reality means independent of the other axioms.

A statement is undecidable if you can produce models in which it is both true and false.

Here is a simple set of axioms:

1. There exists an element zero.
2. Every element has a successor.

From this, can we prove that there is no number that has zero as a
successor?

Short answer, no. If we take the numbers 0,1,2,3 ... as the model, then no number has zero as a successor. If we take the numbers -2,-1,0,1,2 ... as the model, then -1 has zero as a successor.

The question of whether 0 is a successor to any number is undecidable in this system, because models exist in which it is true and false.

As I understand it, that is how the independence proof of CH proceeds, but constructions of models in which it is true and false.

It is quite possible that the Goldbach conjecture is true but not provable. There might even be a proof in a slightly stronger environment that it is undecidable in standard arithmetic, which would of course mean it is true. You might like to try Googling Goodstein sequences, if you don't know about them already.

.

Relevant Pages

  • Re: Set Theory: Should you believe?
    ... with a successor function, and with a successor relationship where ... one assumes in the axioms that the successor relationship is a function ... formulate the Peano Axioms which are non-equivalent. ... Bringing in these other treatments where "number" ...
    (sci.logic)
  • Re: Set Theory: Should you believe?
    ... with a successor function, and with a successor relationship where ... of formulating the Peano Axioms are essentially the same. ... logicians commonly refer to as Peano Arithmetic, is the "first order projection" ... infinitely many naturals and others are not. ...
    (sci.logic)
  • Re: Weniger als alef
    ... Zero is not the successor of a number. ... >> Peano's axioms are the basis for the version of number theory known as ... Andernfalls hätte man eben irgend eine Menge wie IR, die ...
    (de.sci.mathematik)
  • Re: Weniger als alef
    ... Ja, in diesem Kontext schon. ... Zero is not the successor of a number. ... Peano's axioms are the basis for the version of number theory known as ...
    (de.sci.mathematik)
  • Re: infinity
    ... Not while discussing the consequences of the axioms as they actually are! ... > You never commented on my adjustment of the Peano axioms, ... IF you claim to have generated an infinite set with your ... I am applying only finitely many successor operations at ...
    (sci.math)