2
$\begingroup$

I'm struggling with the notion of consistency, and a few cases :

I'm writing in the following $Con(T)$ to denote the arithmetic formula which expresses the consistency of $T$, for $T$ a consistent and recursive theory extending Peano (denoted $PA$).

Firstly, note that $PA$ isn't a complete theory, since Gödel's first incompleteness theorem states that a recursive extension of $Rob.$ cannot be both complete and consistent.

Now, my problem arises when I'm asking myself if this does hold : $$ PA \cup \{Con(PA) \} \vdash \neg Con(PA) $$

And how about $$ PA \cup \{\neg Con(PA) \} \vdash Con(PA) $$

Here are my thoughts : I know that from second incompleteness theorem, $PA \nvdash Con(PA) $, so it means that there is at least a model of $PA$ in which $\neg Con(PA) $ is true, for otherwise, it would be false in all models and so $Con(PA) $ would be true in the theory, which it cannot be.

And I would like to say that since the standard model is such that $PA$ is consistent, it is a model of $PA \cup \{Con(PA)\} $ too and it cannot proves $\neg Con(PA) $ otherwise, it would be inconsistent and so it may prove anything, including its own consistency, a blatant violation of Gödel's second theorem.

Hence to answer my first question, it doesn't hold.

Next, for my second problem, I know from above that there is a model of $PA$ in which there is $\neg Con(PA) $, so in this model, if I were to proves $Con(PA) $, I would have inconsistency, hence be able to prove anything, including the consistency of $PA \cup \{\neg Con(PA) \} $, which violates again the second theorem.

So answer to both my questions would be "No". Is that right?

On another note : is there any inconsistent and recursive theory extending Peano? I'd say that if there were one it would have to be complete by Gödel's first theorem, so I may just pick an axiom of Peano and add its negation to Peano and get such a monster, couldn't I? But now, if I were to consider a decidable and complete extension of Peano, I couldn't possibly have a recursive extension, but how should I build such an extension, how can I get Peano to "become" decidable?

Any other useful consideration to be sure to understand Gödel's theorem and implications is welcome.

$\endgroup$
3
$\begingroup$

Your arguments on the two entailments seem solid, except that it is not "a blatant violation of Gödel's second theorem" that an inconsistent theory can prove its own consistency. Gödel's theorems don't apply to inconsistent theories at all.

For the bonus question: Yes, there are plenty of inconsistent recursive theories that extend PA. One simple example would be PA${}\cup\{1=0\}$.

Your problem in the last paragraph seems to be that you have forgotten one of the premises of the incompleteness theorem. It says that no theory can be (a) an extension of PA (or Robinson arithmetic) and (b) recursive and (c) complete and (d) consistent. The case that troubles you does not satisfy the last of those conditions and is therefore not a problem for the theorem.

(Inconsistent theories are always decidable: The program that always prints "yes" will correctly decide whether any wff can be proved in them).

$\endgroup$
  • $\begingroup$ Hell, and I was so happy to be able to use the term "blatant"... About my last paragraph, I wasn't so clear, but I actually never thought it may be a problem for the theorem, I just didn't see how to build one. I didn't even think about this "always yes" decider. Thank you. $\endgroup$ – Lery Jun 5 '15 at 21:21
  • $\begingroup$ Wait. If it is no contradiction, then I don't have any argument about why it cannot prove $\neg Con(PA) $... So my arguments are empty. What am I missing? $\endgroup$ – Lery Jun 5 '15 at 22:21
  • $\begingroup$ @Lery: Well you already have "... PA would be inconsistent". That contradicts our knowledge that PA is consistent, due to the standard model. You have your contradiction there, you just don't need to appeal to Gödel to get it. $\endgroup$ – Henning Makholm Jun 5 '15 at 22:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.