1
$\begingroup$

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?

$\endgroup$
4
  • 1
    $\begingroup$ You seem to be tacitly assuming that the theory in question is computably enumerable. Without such an assumption, there are plenty ($2^{\aleph_0}$) of complete, consistent theories extending PA or ZF. $\endgroup$ Commented Aug 18, 2021 at 17:49
  • 2
    $\begingroup$ This looks like an improved version of some questions that I commented on recently, that others downvoted, and that someone deleted -- so if the same person who asked those downvoted questions is asking a similar question here from a new account, I think that would be an abuse of the site, and asking improved questions from the same account would be more appropriate. $\endgroup$
    – user44143
    Commented Aug 18, 2021 at 21:26
  • 1
    $\begingroup$ The time gap between the questions was more than 48 hours. I lost access to the old account. $\endgroup$
    – siam
    Commented Aug 19, 2021 at 8:05
  • 3
    $\begingroup$ Well, if there is a proof that $T$ is complete of length $n$, there is a proof that $T$ is inconsistent of length at most $n+c$, where $c$ is a constant (the length of the proof of Gödel’s theorem, basically). So it’s effectively almost the same. Thus, while it’s perfectly possible the answer to the question is yes, this might depend on some minute details of the definition of the proof system, and it might be quite difficult to prove, as usual speed-up theorems work with much bigger gaps than just an additive constant. $\endgroup$ Commented Aug 19, 2021 at 8:37

0

You must log in to answer this question.

Browse other questions tagged .