3

By Godel's incompleteness theorem, no consistent r.e. theories $T$ that can encode PA can prove $Con(T)$. But is there is consistent r.e. theories $T$ that can encode PA that can actually prove $\neg Con(T)$?

Perhaps there is already a name for it, but I don't know, so I'm calling it self-defeating theories. Note that it still have to be consistent.

snaketail
  • 33
  • Unfortunately, I'm not sure I understand your question, "is there is consistent" sounds a bit vague. If you mean inconsistent theories, the answer is clear: in an inconsistent theory, you can prove anything, including the contrary, that's why they're called inconsistent. And if a theory can prove its own inconsistency, it is inconsistent. –  May 17 '17 at 18:23
  • 2
    @ProfessorVector "And if a theory can prove its own inconsistency, it is inconsistent." No, that's completely false. See my answer. – Noah Schweber May 17 '17 at 18:27
  • @ProfessorVector: $\operatorname{Con}(T)$ is not the metaproposition that $T$ is consistent: it is the proposition that the theory described by $T$ does not have an integer that encodes the derivation of a contradiction from $T$. –  May 17 '17 at 20:12
  • @ProfessorVector: And to digest the difference between a "proof" and a "proof in $T$", note that in a nonstandard model of $PA$ there are transfinite integers. Consequently, the length of a "proof in (the model of) $PA$" can be transfinite -- such a thing cannot be converted into a proof in the ordinary sense. Thus, a theory $T$ having a proof of $\neg \operatorname{Con}(T)$ does not necessarily yield a proof that $T$ is inconsistent. –  May 17 '17 at 20:18

1 Answers1

7

Everything below assumes that PA is consistent.

Sure, there are lots of these (although I don't know a name for them) - by Goedel's incompleteness theorem, the theory PA + "PA is inconsistent" is consistent, assuming PA is! And clearly it proves its own inconsistency.

The issue here is one of soundness: PA can't convert a proof of "I prove $0=1$" to a proof of "$0=1$." In fact, this sort of conversion is very rare, in a precise sense: by Lob's theorem, PA proves "If I prove $\varphi$, then $\varphi$ is true" exactly when PA already proves $\varphi$! So there is actually very little new information PA can extract from a proof of "PA proves $\varphi$."

Let me say a little more about the details here, to address the worries of the commenter below.

First of all, note that if you believe the incompleteness theorem, you had better believe the statement I wrote above. If PA+"PA is inconsistent" proved "$0=1$", then by the deduction theorem we'd have that PA proves "If PA is inconsistent, the $0=1$." But PA proves "$0\not=1$," so by contrapositive PA would prove "PA is consistent" and so be inconsistent.

Alright, so what's the heart of the confusion expressed below? Note the sentence

"Starting from false statements, you can prove anything."

This is a common phrasing of the principle of explosion; however, it is not actually correct! There are plenty of false-but-consistent sets of axioms out there.

Incidentally, there's already a nascent version of this conflation in the following two definitions of inconsistency used in the comment: "you can prove anything, and that's called inconsistency" (correct) and "theories that prove false statements are called inconsistent" (incorrect). Inconsistency is a purely syntactic property (do you prove every sentence?) whereas correctness is a semantic property (do you prove any sentences which are not true about the natural numbers?).

Accurately stating explosion is a bit subtle. One version is:

If $T$ proves $\neg\varphi$, then $T$ proves "$\varphi\implies \psi$" for every sentence $\psi$.

This is absolutely true. But note the hypothesis "$T$ proves $\neg\varphi$," not "$\varphi$ is false." That is, the principle of explosion is properly understood internally to a theory. Note that if this were not the case, then the true theory of arithmetic would be decidable: for every sentence $\varphi$ in the language of arithmetic, exactly one of PA+$\varphi$ or PA+$\neg\varphi$ would have to be inconsistent, and we would be able to search through possible proofs to determine which it was. But the true theory of arithmetic is extremely undecidable.

The takeaway is this: a theory which proves false statements need not be inconsistent; the principle of explosion is not as strong as it is often stated. While it is true that any theory proving its own inconsistency must have false axioms, it need not be able to prove every sentence, that is, it may not actually be inconsistent.

Noah Schweber
  • 245,398
  • You seem to have little faith in a proof. I won't abandon the notion that if something is proven, it is true, otherwise I'd had to discard all of mathematics. So if inconsistency is proven, it is true. And if anything can be proven in a theory, it is certainly inconsistent. No play with words ("soundness") is likely to convince me otherwise. –  May 17 '17 at 18:34
  • 3
    @ProfessorVector Do you really believe that "if inconsistency is proven, it is true" even if the proof is based on false axioms? – Andreas Blass May 17 '17 at 18:38
  • Starting from false statements, you can prove anything, and that's called inconsistence. If a theory $T$ is consistent, $\neg Con(T)$ is a false statement. Theories that prove false statements are called inconsistent. I won't waste more time with that. –  May 17 '17 at 18:42
  • Looks like this is easier than I thought, no wonders why this does not seem to have a name. – snaketail May 17 '17 at 18:46
  • @ProfessorVector This isn't a word game at all (and incidentally soundness is a technical term). The main issue you're having is that you're stating the principle of explosion incorrectly; it is absolutely the case that some axiom systems can prove incorrect things without necessarily being inconsistent. I've edited my answer to address these concerns. Please let me know if there are any further confusions (assuming of course that you are serious about learning this stuff). – Noah Schweber May 17 '17 at 19:01
  • Relatedly, when you write "I won't abandon the notion that if something is proven, it is true, otherwise I'd had to discard all of mathematics. So if inconsistency is proven, it is true.", you're missing the key assumption: that the axiom system you're using is correct. In this case, the theory $T$ we're looking at (PA + "PA is inconsistent") is very incorrect - so there's no reason to trust its proofs. – Noah Schweber May 17 '17 at 19:04
  • Noah, it's great that you added the details. But you're fighting windmills. – Asaf Karagila May 17 '17 at 19:09
  • @AsafKaragila Oh I'm well aware, but every so often you get a surprising windmill (and the details might help other readers). – Noah Schweber May 17 '17 at 19:10
  • In fairness to Professor Vector, it is a bit misleading to say in our metalanguage that the theory $T = PA + \mbox{"$PA$ is inconsistent"}$ proves its own inconsistency. What $T$ proves is the existence of an object $p$ that would be (the arithmetization of) a proof of an inconsistency such as $0 = 1$ in $PA$, if the standard natural numbers were a model for $T$. From this we can conclude that the models of $T$ are all non-standard, but not that $PA$ is inconsistent. – Rob Arthan May 17 '17 at 23:22
  • @RobArthan I disagree, I don't understand how that's misleading at all. T := PA + "PA is inconsistent" definitely proves its own inconsistency: there is a sentence in the language of arithmetic which naturally expresses "T is inconsistent," and T proves this sentence. Now when you unwind what that means, and why it doesn't conflict with the fact that PA is in fact consistent, you get into talking about models as you do and as Hurkyl does above; but that's separate from the statement "T proves its own inconsistency," which is absolutely true. – Noah Schweber May 18 '17 at 02:02
  • 2
    @Noah Schweber Thanks for adding those details to your answer, I think I understand now where I misinterpreted some statements. Gödel's incompleteness theorem is a fascinating thing (one of the most fascinating in all of mathematics, in my opinion), but quite obviously, I still hadn't a complete image of the consequences. One side of it is almost tangible (Goodstein's theorem, say, far closer to life than Ramsey theory, you can code it on your laptop), but others are more tricky, as it turns out. –  May 18 '17 at 06:16
  • @ProfessorVector Thanks, glad to help! Let me know if you have any more questions. – Noah Schweber May 18 '17 at 18:13
  • @NoahSchweber: yes, there is a sentence in the language of arithmetic which naturally expresses "$T$ is inconsistent" when interpreted in the standard natural numbers. $T$ proves that sentence, but as it doesn't have the standard natural numbers as a model, the metalanguage statement "$T$ proves its own inconsistency" is false. You are conflating proof of a formalisation of a property with the property itself. – Rob Arthan May 23 '17 at 21:44
  • @RobArthan "You are conflating proof of a formalisation of a property with the property itself." That's a fair point, but I think that winds up being a too restrictive notion of what it means to formalize a property inside a theory. For me, the notion of "formalize" which I am most interested in and use in practice has the following property: if $p$ adequately formalizes a property $P$ inside a weak theory $T_0$ and $T$ is a theory extending $T_0$, then $p$ also formalizes $P$ inside $T$. This leads to false theories proving formalizations of false properties, but that's not a problem. (contd) – Noah Schweber May 24 '17 at 01:01
  • This issue shows up in natural language theories, too. Let $T$ be some nicely-definable set of natural-language sentences, and consider the sentence in natural language "$T$ is inconsistent." Clearly this expresses that $T$ is inconsistent; but $T$ might still prove it, despite being consistent, by virtue of containing false sentences. Rather than say that a sentence doesn't express inconsistency, I'd argue it's better to say that a proof of that sentence in the theory under consideration doesn't constitute evidence that the claim is true. But of course this is a subjective issue. (contd) – Noah Schweber May 24 '17 at 01:04
  • My viewpoint, then, is: a true metatheory conservative over PA proves that $T$ is inconsistent iff $\mathcal{E}_T$ is true. The sentence "$\mathcal{E}_T$," by virtue of this, expresses the inconsistency of $T$ in $T$, and monotonically will continue to do so in all stronger axiom systems, including $T$ itself. The theory $T$, by proving this sentence, proves its own inconsistency; of course, a $T$-proof of a sentence in no way constitutes a proof of the sentence from true axioms, or indeed evidence of its truth at all, so this isn't a problem. – Noah Schweber May 24 '17 at 01:09
  • (I shifted from "formalize" to "express"; this was purely accidental, and carries no significance.) – Noah Schweber May 24 '17 at 01:12
  • @NoahSchweber: thanks for the explanation (and your concession that my point is a fair one). I can see why you find it convenient to talk about theories for which there is a compelling notion of a standard model in the way you suggest, but it can lead to confusion (as it has here). – Rob Arthan May 24 '17 at 20:53
  • @RobArthan But I don't think it's what led to confusion here. The same issue can be constructed in natural language as per my comments, and unless you want to argue that the sentence "$T$ is inconsistent" doesn't always express the sentence "$T$ is inconsistent" the only resolution is the (correct) observation that proving a sentence from a false set of axioms has no bearing on its truth. So I really don't think the issue here is what it means to precisely express a property - this just comes down to the fact that there's no reason to be surprised that false theories prove false sentences. – Noah Schweber May 24 '17 at 22:15
  • @NoahSchweber: I don't see how you can construct the same issue in natural language: natural language doesn't have a formal proof system. Professor Vector was confused because your choice of technical terminology allows you to say that a consistent system $T$ proves its own inconsistency. If you want to encourage a proper understanding of mathematical logic, I suggest you stop using emotive terms like "false theories" without proper consideration of how those terms will be perceived by non-experts. – Rob Arthan May 24 '17 at 22:41
  • @RobArthan "Professor Vector was confused because your choice of technical terminology allows you to say that a consistent system $T$ proves its own inconsistency." Yes, and I stand by the claim that a consistent theory can prove its own inconsistency. The resolution is that false theories can prove false things, even while being internally consistent. This is an absolutely fundamental fact about reasoning in general, not even formalized reasoning, and understanding it at an intuitive level is crucial to understanding mathematical logic. So I respectfully disagree with your suggestion. – Noah Schweber May 24 '17 at 22:44
  • We will probably just have to agree to differ. I can't make sense of your notion that some first-order theories are "false" and think it is inimical rather than crucial to an understanding of mathematical logic (your "false theories" are just theories whose mathematical models are not the standard, expected, models of the theory in question). – Rob Arthan May 24 '17 at 23:44