[FOM] Inconsistency of P

[Monroe Eskew]

On Tue, Oct 4, 2011 at 3:54 AM, Rempe, Lasse <L.Rempe at liverpool.ac.uk> wrote:
>
> (I am, however, not entirely sure which specific number c Monroe had in mind, given that the theorem obviously does not apply to inconsistent theories).
>

It seems wrong to say the theorem does not apply to inconsistent
theories, since it actually gives you a way to tell if a theory is
inconsistent.  It is a statement about all computable theories.

The constant c in my example is intended to share all the relevant
properties from the one in the general theorem.  Let me give a
slightly more general version.

Suppose T is an inconsistent extension of some true, Sigma_1-complete
theory, for example Q.  Fix a T-proof p of "0=1."  For any given c, a
proof of the statement "K(0)>c" is just a modus ponens away.   Make a
version of the Chaitin machine that enumerates the proofs in T such
that "K(0)>c" comes first.  The length of this program is a constant
plus log(c), so we can find c such that the program is shorter than c.
 In particular, exactly the same inconsistency argument from the
general case can be run here, even though we already have p.  There
exists n such that K(n)>c is true, so we then let S = Q + "K(n)>c".

This example is intended be similar enough to things in the proof of
Chaitin's theorem to show Panu's worry about subtheories was mistaken.

Best,
Monroe