Skip to main content
1 of 2
siam
  • 11
  • 2

Shortest proof of inconsistency of first order theory

Suppose we are studying first order theories in some metatheory (e.g. PA or ZF).

If we have a proof that a given first order theory is complete and contains PA then we also get a proof that it is inconsistent by Gödel. Not all proofs of inconsistency are of this form.

Is there a complete first order logic containing Peano arithmetic such that the shortest known proof of its inconsistency is of the form above?

siam
  • 11
  • 2