Is FOL really sound?

Question

The soundness of FOL is proved in meta-language(natural language) by proving every deduce rule is correct, so we feel peaceful using those rules to deduce. But the process of proving every deduce rule is correct also uses deduce rules in natural language. For example, proving the correctness of PC(Proof by Case) also uses PC in natural language, so we assume the PC rule exists and assume PC is correct in natural language. Do we need to construct another meta-language for the natural language to prove those assumptions like we are doing for FOL? Otherwise, how can we feel peaceful using those rules when deducing in FOL? Furthermore, is it possible to construct such a meta-language for an unrestricted language such as the natural language?

Answer 1

First let's be clear about the fact that there are two levels at play here.

At the top level (sometimes called the "meta-level"), there is the logical reasoning that we human mathematicians do to convince ourselves of things by, for example, writing proofs in natural language.

At the next level down (sometimes called the "object-level"), there's a mathematical system called first-order logic (FOL), with formal proof rules and a set-theoretic semantics. Since the components of FOL are mathematical objects, we can reason about them at the meta-level, just like we reason about numbers and geometry.

Now the object-level system FOL is not picked arbitrarily. It is set up as a mathematical model of our meta-level reasoning. This means that pieces of reasoning we do at the meta-level can, in principle, be coded up as mathematical objects called formal proofs in FOL that we can reason about. More on this later.

The statement "FOL is sound" is a theorem of mathematics about the relationship between the formal proof rules of FOL and its set-theoretic semantics. Viewing this theorem as a fact about our meta-level reasoning is a category error. It's a property of the model, not a property of the thing being modeled.

It seems that you really want an answer to the question "is our meta-level reasoning sound?" Let me stress again that soundness is about the relationship between proof rules and semantics. To even make sense of the question, you would have to set up a semantics for our meta-level reasoning. Working out semantics for natural language is incredibly complicated (ask a linguist! this is why logicians work instead with simpler formal languages). But assuming you've done this, you now need to reason mathematically about this system. And now you realize that what you've done is just come up with a rather more complicated model for meta-level reasoning at the object level, and the situation is the same as before. See my answer to this question for some related thoughts.

---

Your question is predicated on a misapprehension that the goal of mathematical logic is to justify our meta-level reasoning. This is not correct: logic cannot be self-justifying. Nevertheless, it can be interesting and useful to have a mathematical model of our meta-level reasoning. In the comments below, you write "Our natural logic seems the first principle, and if so, the research of FOL seems to lose much of its value." Let me give you some reasons why I disagree with this.

(1) One issue with informal natural-language reasoning is that there's room for people to disagree on what counts as a proof. My intuition for what reasoning is convincing might differ from yours. The mathematical community has essentially accepted ZFC set theory in FOL as a foundation for mathematics. What this means (in my view) is that we have a clearer standard of proof: an acceptable proof is one that, in principle, can be translated into a formal proof in FOL from the axioms of ZFC. Of course, there are issues with this: no one actually does this translation, there may be ambiguity about how exactly to translate natural language, etc. But it means that someone who doubts a proof can ask for more details about a particular step and end up tunneling all the way down, at least in principle, to the axioms and logical reasoning.

(2) As a model-theorist, I feel obliged to point out that FOL is useful in more ways than "just" as a foundation for mathematics. In model theory, we use FOL as a framework for talking about definability in mathematical structures, and we leverage properties of FOL (e.g., the compactness theorem, the Löwenheim-Skolem theorem, etc.) to prove theorems about mathematical structures. Here the fact that FOL is a model for our meta-level reasoning is irrelevant.

(3) Like any mathematical model, we can use this one to make predictions about the real world. For example, it is a theorem that if ZFC is consistent, then ZFC not prove the Continuum Hypothesis (CH). As a result of this theorem, I'm not going to waste my time trying to prove CH, because I am fairly confident no such proof exists in the real world (at the meta-level). Why? Well, because I am fairly confident that ZFC in FOL is an excellent model for our meta-level reasoning, I believe that a proof of CH could be translated into a formal proof. That is, if I had a proof of CH, then I could prove $\mathsf{ZFC}\vdash \mathrm{CH}$. But I also know how to prove $\mathrm{Con}(\mathsf{ZFC})\rightarrow \mathsf{ZFC}\not\vdash \mathrm{CH}$. Putting these together, I could prove $\lnot \mathrm{Con}(\mathsf{ZFC})$. But I am also fairly confident that there is no proof of $\lnot \mathrm{Con}(\mathsf{ZFC})$ (because I am fairly confident that (a) ZFC is consistent, i.e. there is no natural number coding a proof of "false" in ZFC, and (b) mathematics doesn't prove false statements about the existence of natural numbers). Note that I am not 100% certain of any of the three things I said I'm fairly confident about above. That's why I say that "there is no real-world proof of CH" is only a prediction that we can make on the basis of our model.

Maybe I should note here that there's no way our model can make a useful prediction about consistency of pure logical reasoning at the meta-level. For example, the soundness theorem seems to predict that $\not\vdash \bot$, i.e., there is no purely logical (no axioms) proof of a contradiction. If I actually had a proof of false from pure logic, then I could prove anything I like at the meta-level, and in particular I could prove anything I like about the object-level model, so its predictions are useless. This is the issue with trying to use logic to justify logic.

The soundness theorem is not totally useless, though: It does provide a kind of "sanity check". If it were false, i.e. if there were some proof rule in FOL which was shown to not be sound, this would seriously shake our intuitions about what logic means. That is, there would be a conflict between the proof rules and the set-theoretic semantics, both of which seem so natural to us.

Does the theorem that FOL is sound make me "feel peaceful"? Well, yes, to the extent that I know that the hypothetical situation in the previous paragraph won't arise. But at a personal level, the soundness theorem for FOL plays no role in my acceptance of meta-level reasoning. I "feel peaceful" reasoning logically at the meta-level because the kind of logical reasoning mathematicians use seems intuitive and convincing to me.