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

When reading discussions of Gödel's theorems one is always heeded that just because formal system $$F$$ proves a theorem $$T$$ that doesn't necessarily mean that when one applies the intended interpretation the theorem is actually true. After all, even if one assumes that $$F$$ is consistent, it might still be unsound.

But this puzzles me. When setting up $$F$$ one always makes sure that all the axioms are true under the intended interpretation. Presumably, one would also make sure that all the rules of inference are valid. That is, if all the theorems proven so far are true, then the rules of inference only produce further true theorems. Is that too much to ask?
However, this straightforward construction immediately implies that I can't prove falsehoods under the intended interpretation. Further, I'd be hesitant to even call something for which the rules of inference aren't truth preserving an "interpretation".
But then it seems that unsound formal systems couldn't even exist. So where's the problem with this view?

• Here is a famous quote from logicians and mathematicians, "what is obvious is not obvious at all". A super super solid logic chain of 1000 deductions can break down totally because of one single seemingly harmless vagueness. The more you know, the more likely you might fail. Those are my first thoughts when I see "it seems" in your question. I had been you. – Apass.Jack Nov 21 '18 at 20:22
• Well, the "more you know, the more likely you might fail" is a bit of a stretch there. – Andrej Bauer Nov 21 '18 at 21:08
• Crossposted: math.stackexchange.com/questions/3007684/… – Noah Schweber Jan 1 at 20:49

You jumped to a conclusion when you said that "when setting up $$F$$ one always makes sure that all the axioms are true under the intended interpretation". This is not the case at all. Using theories and formal systems as devices with which we reliably discover thruths is only one possible application.

Insisting that a formal system must be sound with respect to an "intended interpretation" can have the unfortunate effect of holding back development. For example, in order to discover non-Euclidean geometry someone had to contradict the dogma that Euclid's geometry was obviously true, and suggesting a theory which was non-Euclidean (which was considered obviously unsound) amounted to taking a professional career risk.

Sometimes there is no intended interpretation because we are exploring a new mathematical theory with which we have very little experience. In such a situation we will attempt to identify possible axioms and hope that their consequences will inform us about what is going on.

Sometimes we simply do not know what the intended interpretation is, and so we have to make a choice about accepting or rejecting an axiom based on other criteria than truth. Or better, we do not make a choice and study several options, without obsessing about "intended model". The most famous example of this is the axiom of choice in set theory. We know that set theory with choice is consistent if, and only if, set theory without choice is consistent. Which one is sound? On what grounds do we decide whether the axiom of choice is "true in the intended interpretation"?

So what is wrong with your view? I don't think much is wrong, except that it can hinder mathematical development. I advocate the position that the so called "intended interpretation" is in general an unknowable and uncommunicable entity whose existence is grounded in history and collective social norms. Of course, this does not imply that the "intended interpretation" is completely useless. On the contrary, it binds mathematicians together and allows them to share intuitions, and give coherence to mathematical development. But let us not confound an informal mathematical idea of "intended interpetation" with its mathematical ideal of a model.

• The point you raise is well taken. But it doesn't seem to actually address the root of my concern. I've restated the question more elaborately here: math.stackexchange.com/questions/3007684/… without the mention of an "intended interpretation" or of the process of setting up a formal system. – Sebastian Oberhoff Nov 21 '18 at 18:46
• Is there a version of your question which doesn't use the vague expression "non-obviously"? As it stands, if I delete the phrase, the question becomes a mere technicality. With the phrase, I am not sure it is a question about mathematics. – Andrej Bauer Nov 21 '18 at 19:41
• The "non-obviously" isn't central to my question. It's just that, if the unsoundness was obvious, then one should be able to dismiss the formal system immediately. But I'm concerned with situations such as $\neg G$ being true while $G$ is false ($G$ being the Gödel sentence) where the unsoundness sneaks up on one. – Sebastian Oberhoff Nov 22 '18 at 0:23
• I still don't understand what you're after, sorry. There is no mathematical problem in having a consistent theory which is unsound with respect to a particular model. – Andrej Bauer Nov 22 '18 at 13:20

Yes, that's too much to ask.

It is not trivial to define an interpretation, i.e. a model where $$F$$ is true, in the general case.

Consider Frege's naive set theory. To most people, it looks extremely natural. It basically "only" says that:

• (comprehension) for any property $$p$$ there exists a set $$\{x | p(x)\}$$,
• (membership) $$y \in \{x|p(x)\}$$ iff $$p(y)$$

Yet, it is inconsistent because of Russel's paradox. If we take $$p(x) = (x\notin x)$$, and $$A = \{x|p(x)\}$$, we get

$$A \in A \iff p(A) \iff A \notin A$$

Contradictions like Girard's paradox are more involved, but are surprising since they start from quite reasonable assumptions. If we consider, in type theory, an axiom like $$*:*$$ stating that the universe of types is one of its types, one might still expect that some paradox will arise, because the "circularity" of the universe could allow something similar to Russell's paradox. However, Girard's paradox even works in $$\lambda U$$ where we only have $$*:\square:\Delta$$ without any circularity! The issue comes, roughly, from the impredicativity of such universes. It is not at all obvious that impredicativity alone, without circularity, is inconsistency.