[FOM] Inconsistency of P

[Daniel Mehkeri]

 > This case just is not very interesting, because *all* consistent
 > theories (in the language of T) are subsystems of T; and trivially,
 > some of these prove  K(n) > c (let c be however large and complex).

Yeah, I imagine other FOM readers are also wondering why we care at all.

One place where it would matter, even if T is consistent, is when T is 
reasoning about its own subtheories. The fact that T is consistent is 
not available within T. As I understand it, this was relevant to the 
proof attempt:

If S proves K(n) > c, then S is inconsistent.
  [BUT we can only say T is inconsistent]
Now T proves S is consistent.
So T proves S does not prove K(n) > c(T).
...
So T is inconsistent [by something like Kritchman-Raz's unexpected 
hanging argument].
But the computation of this inconsistency is superexponential.
Now PRA proves superexponential functions terminate.
But PRA also proves T is consistent.
So PRA is inconsistent.

This is also a possible answer to Taylor's question about what it might 
mean to find an infeasible inconsistency.

Daniel Mehkeri