# How can a formal system ever be non-obviously unsound?

When reading about formal systems one is often warned that, even assuming the system is consistent, one can't be sure that any theorem proved in the system is actually true. For instance, if one can prove $$\neg G$$ where $$G$$ is the Gödel sentence in some formal system $$S$$, then that doesn't immediately make $$S$$ inconsistent. $$G$$ might not be provable despite the fact that that's exactly what $$\neg G$$ asserts. $$S$$ would have proven a falsehood, making it unsound, yet it might still be consistent.

What bugs me is: if one has arrived at a falsehood, doesn't that imply that either one of the axioms was false or that one of the rules of inference was invalid (capable of deducing a falsehood from truths)? But if either of those were the case that would make the interpretation under consideration no longer be an interpretation at all. And that would annul the charge that $$S$$ was unsound.

Take the following section from Torkel Franzén's Gödel's Theorem - An Incomplete Guide to its Use and Abuse:

There is a class of statements that are guaranteed to be true if provable in a consistent system $$S$$ incorporating some basic arithmetic. Suppose $$A$$ is a Goldbach-like statement [a statement similar to the Goldbach conjecture where, if it is false, a mechanically verifiable counterexample exists]. We can then observe that if $$A$$ is provable in such a system $$S$$, it is in fact true. For if $$A$$ is false, it is provable in $$S$$ that $$A$$ is false, since this can be shown by a computation applied to a counterexample, and so if $$S$$ is consistent, it cannot also be provable in $$S$$ that $$A$$ is true. Thus, for example, it is sufficient to know that Fermat's theorem is provable in ZFC and that ZFC is consistent to conclude that the theorem is true. But in the case of a statement that is not Goldbach-like, for example the twin prime conjecture, we cannot in general conclude anything about the truth or falsity of the conjecture if all we know is that it is provable, or disprovable, in some consistent theory incorporating basic arithmetic.
The incompleteness theorem gives us concrete examples of consistent theories that prove false theorems. This is most easily illustrated using the second incompleteness theorem. Given that ZFC is consistent, ZFC + "ZFC is inconsistent" is also consistent, since the consistency of ZFC is not provable in ZFC itself, but this theory disproves the true Goldbach-like statement "ZFC is consistent."

(emphasis mine)

So according to Franzén ZFC + "ZFC is inconsistent" is unsound because it proves the falsehood "ZFC is inconsistent". But that's not how I see it. To me any structure where "ZFC is inconsistent" is a false statement can't serve as an interpretation of this system to begin with. After all, one of the axioms is false.

The above reminds me of Saccheri's famous "the hypothesis of the acute angle is absolutely false; because it is repugnant to the nature of straight lines". Non Euclidean geometry isn't unsound just because some of its theorems are false according to the straight line interpretation. By the same token ZFC + "ZFC is inconsistent" isn't unsound just because one of its theorems is false in the standard ZFC structure.

But then this raises the larger question how any formal system could ever be unsound. It would seem that any structure that might hope to serve as a witness for the systems unsoundness would immediately disqualify from being an interpretation at all.

• "inconsistent" implies not sound, because an incons system proves all, and this also $A$ and $\lnot A$, and one of them must be false. Nov 21, 2018 at 12:50
• But an "unsound" system can be consistent : it is "wrong" but does not prove contradictions. Nov 21, 2018 at 12:51
• "By the same token ZFC + "ZFC is inconsistent" isn't unsound just because one of its theorems is false in the standard ZFC structure." - that is exactly the definition of "unsound"! "Sound" is a technical term here, which has to be read according to its definition. Nov 21, 2018 at 19:43
• I think you have to be clear on the definitions. Soundness of a deductive system with respect to some semantics means that the deductive rules are truth-preserving with respect to that semantics. But arithmetical soundness of a formal system $S$ that interprets arithmetic (there is a computable translation of arithmetical sentences into $S$) means that $S$ does not prove the translation of any false sentence about naturals. Take a look at this post under "Soundness versus consistency". Nov 24, 2018 at 12:24

When we say that a theory (like ZFC+"ZFC is inconsistent") is unsound, we are (at least naively) speaking with respect to a specific "intended model." So - under the usual hypotheses - there are models of ZFC+"ZFC is inconsistent" (because it's consistent), but $$V$$ isn't one of them.

For a more concrete example, insofar as $$\mathbb{R}^2$$ is our "intended model" non-Euclidean geometry is indeed unsound, since it doesn't hold in $$\mathbb{R}^2$$. That is, your claim "non-Euclidean geometry isn't unsound just because some of its theorems are false according to the straight line interpretation" is exactly wrong. What is true is that non-Euclidean geometry isn't inconsistent just because some of its theorems are false in the "intended model," and this is exactly the difference between inconsistency and unsoundness.

• Note that this is an important example of how the technical meaning of "sound" in mathematical logic differs from its intuitive meaning in mathematics more generally: "unsound" doesn't mean "doesn't work at all" - that meaning is taken up more accurately by "inconsistent" - but rather "doesn't accurately describe this thing we care about over here." Whether or not a principle is sound depends on the thing in question.

What if we don't consider $$\mathbb{R}^2$$ to be our intended model? Well, there's no need to posit an intended model at all! We could consider all models of the given theory as being on the same footing. In the absence of an intended model, "soundness" does indeed collapse to mere consistency. For example, there's no "intended model of the group axioms," so you'll never hear people talking about the abelian axiom $$\forall x,y(x*y=y*x)$$ being sound or not.

Now, postulating an intended model of set theory is a bit worrying without strong Platonic commitments, and even leaving set theory aside we may reasonably want to minimize our philosophical commitments (I certainly do). So we often want to fall back to the weaker idea of relative soundness: a theory $$T$$ is sound with respect to a theory $$S$$ if $$T$$ doesn't prove anything $$S$$ disproves. Note that this isn't quite the same as saying $$T\subseteq S$$ - we could have the language of $$T$$ include symbols which the language of $$S$$ doesn't, so that $$T$$ would contain sentences which $$S$$ simply doesn't see.

• You are using the term soundness differently than I am used to. I'm following the definition laid out, for example, in the Princeton companion to mathematics on page 324: "soundness is the assertion that if $T\vdash\Phi$ then $T\vDash\Phi$" ($T\vdash\Phi$ means the theory $T$ proves the sentence $\Phi$. $T\vDash\Phi$ means $\Phi$ is true in every model of $T$). Nov 21, 2018 at 23:56
• @SebastianOberhoff That's the soundness of the provability relation $\vdash$. When we say a sentence (or theory) is sound, we mean that it holds of an intended structure. Soundness of a proof system is a different concept than soundness of a sentence/theory. Nov 22, 2018 at 0:09
• That said, there is definitely a similarity. When we say "$T$ is sound," we mean "$T$ holds of $\mathcal{M}$" (where $\mathcal{M}$ is our intended model). When we say "$\vdash$ is sound," we mean that $\vdash$ "holds of our intended semantics." Other semantics are possible: e.g. sheaf models are more general than classical models, and the classical provability relation $\vdash$ is not sound for this semantics (sheaf models are actually intuitionistic). Nov 22, 2018 at 0:13
• In general, when we say "--- is sound" we mean "--- asserts only true statements about the thing under discussion." When "---" is a theory or sentence, the thing under discussion is a specific structure; when "---" is a provability relation, the thing under discussion is a whole notion of semantics. In general, you need to carefully keep theories and proof systems/satisfaction notions separate (e.g. "first-order logic is complete but first-order arithmetic is incomplete") Nov 22, 2018 at 0:15
• So when Gödel spoke of a sound formal system capable of expressing primitive recursive arithmetic he meant sound as in "appropriate to the usual conception of natural numbers" not as in "can only prove true statements regardless of the model currently used"? Nov 22, 2018 at 0:20

First read this post on the incompleteness theorems and pay attention to the section of "Soundness versus consistency". If a formal system can talk about finite binary strings (via an appropriate translation), then its soundness for finite binary strings is strictly stronger than its soundness for program halting, which in turn is strictly stronger than consistency. This should adequately explain why systems such as ZFC+¬Con(ZFC) is consistent but unsound for program halting.

But I think I should also explicitly address your misconception about axioms. An axiom is neither true nor false by itself. This misconception is propagated by the innumerable inaccurate pop-science articles on the incompleteness theorems. One must always remember that any string of symbols is devoid of meaning until it is interpreted. Likewise, any sentence over some first-order language $$L$$ is a meaningless string of symbols until it is interpreted in some $$L$$-structure. ( ZFC is consistent ) can be encoded into an arithmetical sentence (namely a first-order sentence over the language of arithmetic $$A$$), so you can only talk about its truth of falsehood in an $$A$$-structure. $$\mathbb{N}$$ is an $$A$$-structure, so you can talk about its truth-value in $$\mathbb{N}$$.

And let's talk about a simple formal system like PA first, before talking about complicated ones like ZFC. If PA is consistent (which virtually all logicians believe), then PA+¬Con(PA) must also be consistent (by the incompleteness theorem) but PA+¬Con(PA) trivially proves ¬Con(PA), which is false in $$\mathbb{N}$$. On the other hand, by the completeness theorem the consistency of PA+¬Con(PA) implies the existence of a model of PA+¬Con(PA), which hence cannot be isomorphic to $$\mathbb{N}$$.

• I'm not sure "inaccurate" is really fair. Even in the research literature, "true" is generally accepted as shorthand for "true in the structure under consideration" (e.g. "proves every true $\Sigma_1$ sentence"). While the model-dependent nature of truth is important, and indeed the key point here, I don't think it's fair to blame pop science articles since the same usage of "truth" occurs professionally. Nov 24, 2018 at 15:31
• @NoahSchweber: I have said elsewhere exactly the same thing as you, when explaining what a logician means by "true arithmetical sentence". But a pop-science article cannot afford to not define or state things clearly. The fact that innumerable people reading those articles are really confused by this exact point (as the many questions on Math SE arising from that confusion attests), supports my view. In fact, it's clear that many pop-science article authors don't even understand the incompleteness theorems themselves, so obviously they can't help their readers. Nov 24, 2018 at 15:51
• @NoahSchweber: By the way, I'm not making any judgement on the specific book the asker cited, because I've not read it and hence do not know if the issue had been addressed properly in it. But I don't think any proper text can avoid making very clear the distinction between syntax and semantics without resulting in almost all lay readers getting badly confused. That's all. =) Nov 24, 2018 at 16:00