Skip to main content
MathOverflow

Return to Question

added 78 characters in body
Source Link
siam
siam
  • 11
  • 2

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

If we have a proof that a given recursively axiomatizable 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 recursively axiomatizable first order logic containing Peano arithmetic such that the shortest known proof of its inconsistency is of the form above?

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?

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

If we have a proof that a given recursively axiomatizable 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 recursively axiomatizable first order logic containing Peano arithmetic such that the shortest known proof of its inconsistency is of the form above?

Source Link
siam
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?