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

Question

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.

Answer 1

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.

Answer 2

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}$.