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?

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.

StackExchange Computer Science Q#100354, answer score: 5