Just like for propositional logic, it turns out first-order logic is also sound and complete. However, this fact is far from obvious.
First, let's state our theorem.
Theorem 18.1. Let $\Sigma$ be a set of formulas and $\varphi$ be a formula. If $\Sigma \vdash \varphi$, then $\Sigma \models \varphi$.
Soundness is the easier direction in the case of predicate logic, since the idea of the proof will be largely similar to the one from propositional logic. Since proofs are finite, we proceed as we did with propositional logic and do a proof by induction on the proof. What is new is that we must now show that each of our new inference rules is sound. Of course, this involves a lot more work than for the propositional case, but the basic idea is not too difficult.
We will need the following lemmas.
Lemma 18.2. Let $s,t$ be terms and let $x$ be a variable. For any interpretation $\mathcal I$ and environment $E$, we have $$s[t/x]^{(\mathcal I,E)} = s^{(\mathcal I, E[x \mapsto t^{(\mathcal I,E)}])}.$$
Lemma 18.3. Let $\alpha$ be a formula and $t$ be a term. For any interpretation $\mathcal I$ with domain $D$ and environment $E$, we have $$\alpha[t/x]^{(\mathcal I,E)} = \alpha^{(\mathcal I, E[x \mapsto t^{(\mathcal I,E)}])}.$$
What do these lemmas say? On the left side, we have a term $s$ or a formula $\alpha$ and we want to replace all instances of a variable $x$ with a term $t$. By now, we should be familiar with how to do this, since it is a purely syntactic operation. However, we want to know what the resulting term or formula means. So what does our substituted expression mean under an interpretation $\mathcal I$ and environment $E$?
Lemma 18.3 says that the meaning of $\alpha[t/x]$ under $\mathcal I$ and $E$ is exactly the same as if you took $\alpha$ and modified the environment $E$ to map $x$ to the term $t$ under the interpretation and environment, $t^{(\mathcal I,E)}$. In other words, this lemma says that the meaning of syntactic substitution is pretty much what you would expect. A similar argument can be made for Lemma 18.2, where the main point is that this tells us the substituted term is an element of the domain.
The difficult part, of course, is proving that this is really the case. Both lemmas can be proved by induction on the formula $\alpha$.
Since our proof of soundness is essentially the same as before, but with more inference rules, all we really need to do is show that each new inference rule is sound.
Proposition 18.4. The inference rule $\forall$e is sound.
Proof. Let $\alpha$ be a formula, $x$ be a variable, and $t$ a term. We will show that $\{(\forall x \alpha)\} \models \alpha[t/x]$. Let $\mathcal I$ be an interpretation and $E$ be an environment such that $\mathcal I \models_E (\forall x \alpha)$. By definition, we have $\alpha^{(\mathcal I,E[x \mapsto d])} = T$ for all $d \in D^\mathcal I$. Observe that by Lemma 18.2, $t^{(\mathcal I,E)} \in D^\mathcal I$. Then by Lemma 18.3, we have $\alpha^{(\mathcal I,E[x \mapsto t^{(\mathcal I,E)}])} = T$ and therefore, $\alpha[t/x]^{(\mathcal I,E)} = T$. Thus, $\mathcal I \models_E \alpha[t/x]$ and we have $\{(\forall x \alpha)\} \models \alpha[t/x]$. $$\tag*{$\Box$}$$
Proposition 18.5. The inference rule $\exists$i is sound.
Proof. Let $\alpha$ be a formula, $x$ be a variable, and $t$ a term. We must show $\{\alpha[t/x]\} \models (\exists x \alpha)$. Let $\mathcal I$ be an interpretation and $E$ be an environment such that $\mathcal I \models_E \alpha[t/x]$, or $\alpha[t/x]^{(\mathcal I,E)} = T$. By Lemma 18.3, this means that $\alpha^{(\mathcal I, E[x \mapsto t^{(\mathcal I,E)}])} = T$. Since $t^{(\mathcal I,E)} \in D^\mathcal I$ by Lemma 18.2, we have that there exists an element $c \in D^\mathcal I$ such that $\alpha^{(\mathcal I,E[x \mapsto c])} = T$ by taking $c = t^{(\mathcal I,E)}$ and therefore, $\mathcal I \models_E (\exists x \alpha)$ by definition. $$\tag*{$\Box$}$$
In the following, we will need another helpful lemma.
Lemma 18.6 (Relevance Lemma). Let $\alpha$ be a well-formed predicate formula and $\mathcal I$ be an interpretation. Let $E_1$ and $E_2$ be two environments such that $E_1(x) = E_2(x)$ for every variable $x$ that occurs free in $\alpha$. Then $\mathcal I \models_{E_1} \alpha$ if and only if $\mathcal I \models_{E_2} \alpha$.
This lemma is another one that confirms our assumptions about what's important about environments. In essence, if we have two environments that agree on mappings of variables that occur in a formula $\alpha$, then they should both produce the same meaning since we really only care about the "relevant" assignments (i.e. those that actually show up in $\alpha$). The Relevance Lemma can be proved by structural induction on $\alpha$.
Proposition 18.7. The inference rule $\forall$i is sound.
Before we get to the proof, we need to think about what it means for $\forall$i to be sound. Just like the rules with subproofs from propositional logic, we need to be careful with what it is that we think the inference rule says. For instance, recall that the rule $\rightarrow$i is stated
If $\Sigma \cup \{\alpha\} \vdash \beta$, then $\Sigma \vdash (\alpha \rightarrow \beta)$.
Then to prove that $\rightarrow$i was sound, we showed that if $\Sigma \cup \{\alpha\} \models \beta$, then $\Sigma \models (\alpha \rightarrow \beta)$. We will state $\forall$i in a similar fashion.
The statement of $\forall$i is
If $\Sigma \vdash \alpha[y/x]$ where $y$ is not free in $\Sigma$, then $\Sigma \vdash (\forall x \alpha)$.
So to show that $\forall$i is sound, we must show that if $\Sigma \models \alpha[y/x]$ where $y$ is not free in $\Sigma$, then $\Sigma \models (\forall x \alpha)$.
Proof (Proposition 18.7). Suppose that $\Sigma \models \alpha[y/x]$ and $y$ is not free in $\Sigma$ or $\alpha$. Let $\mathcal I$ be an interpretation and $E$ be an environment such that $\mathcal I \models_E \Sigma$. We claim that for every element $a \in D^\mathcal I$, we have $\mathcal I \models_{E[y \mapsto a]} \Sigma$ if and only if $\mathcal I \models_E \Sigma$. We will show this by considering an arbitrary formula $\psi \in \Sigma$.
Recall that $y$ is not a free variable in $\Sigma$, and therefore, $y$ is not free in $\psi$. Then we have $E(z) = E[y \mapsto a](z)$ for every free variable $z$ in $\psi$. Therefore, by the Relevance Lemma, we have $\mathcal I \models_E \psi$ if and only if $\mathcal I \models_{E[y \mapsto a]} \psi$. Since $\psi$ was arbitrary, we can conclude that $\mathcal I \models_E \Sigma$ if and only if $\mathcal I \models_{E[y \mapsto a]} \Sigma$.
Therefore, we have that $\mathcal I \models_{E[y \mapsto a]} \Sigma$ for every $a \in D^\mathcal I$ and this means that $\mathcal I \models_{E[y \mapsto a]} \alpha[y/x]$ for all $a \in D^\mathcal I$. Then by definition, we have $\mathcal I \models (\forall x \alpha)$. Thus, $\Sigma \models (\forall x \alpha)$. $$\tag*{$\Box$}$$
Now, recall that
If $\Sigma \vdash (\exists x \alpha)$ and $\Sigma \cup \{\alpha[u/x]\} \vdash \beta$, with $u$ fresh and not free in $\Sigma$, $\alpha$, or $\beta$, then $\Sigma \vdash \beta$.
We must do something similar to express the $\exists$e rule. We will show that if $\Sigma \models (\exists x \alpha)$ and $\Sigma \cup \{\alpha[u/x]\} \models \beta$, with $u$ fresh and not free in $\Sigma$, $\alpha$, or $\beta$, then $\Sigma \models \beta$.
Proposition 18.8. The inference rule $\exists$e is sound.
Proof. Suppose $\Sigma \models (\exists x \alpha)$ and $\Sigma \cup \{\alpha[u/x]\} \models \beta$ with $u$ fresh and not free in $\Sigma$, $\alpha$, or $\beta$. Let $\mathcal I$ be an interpretation and $E$ be an environment such that $\mathcal I \models_E \Sigma$.
Since $\mathcal I \models_E \Sigma$ and $\Sigma \models (\exists x \alpha)$, we have $\mathcal I \models_E (\exists x \alpha)$. This means there exists an element $a \in D^\mathcal I$ such that $\mathcal I \models_{E[x \mapsto a]} \alpha$. Thus, there exists a fresh $u$ which is not free in $\Sigma$, $\alpha$, or $\beta$ such that $\mathcal I \models_E \alpha[u/x]$.
Then since $\mathcal I \models_E \Sigma$ and $\mathcal I \models_E \alpha[u/x]$, we have $\mathcal I \models_E \beta$. $$\tag*{$\Box$}$$
Completeness of first-order logic says the following.
Theorem 18.9. Let $\Sigma$ be a set of formulas and $\varphi$ be a formula. If $\Sigma \models \varphi$, then $\Sigma \vdash \varphi$.
That first-order logic is complete is much more complicated show than soundness and is nowhere near as obvious. Recall that our proof of completeness of propositional logic relied on the fact that there were only finitely many valuations to consider. We have no such luck in the case of first-order logic, where we have an infinite number of interpretations to consider, nor do we have any guarantee that these interpretations will even look like each other.
Completeness of predicate logic was proved by Kurt Gödel in his PhD thesis in 1930 (although, again not for natural deduction because natural deduction was defined by Gentzen later in the 30s). The proof that we sketch, which is the one that is more commmonly used nowadays, is due to Leon Henkin in 1949.
We will make use of the notion of consistency of a set of formulas. Recall from Lecture 9, Definition 9.4, which I'll reproduce here.
Definition 9.4. A set $\Sigma$ is inconsistent if $\Sigma \vdash \bot$. Equivalently, if $\Sigma \vdash \varphi$ and $\Sigma \vdash (\neg \varphi)$ for some formula $\varphi$. We say $\Sigma$ is consistent if it is not inconsistent (i.e. if $\Sigma \not \vdash \bot$).
Lemma 18.10. $\Sigma \vdash \varphi$ if and only if $\Sigma \cup \{(\neg \varphi)\}$ is inconsistent.
Proof. If $\Sigma \vdash \varphi$, then $\Sigma \cup \{(\neg \varphi)\} \vdash \varphi$. Then since also $\Sigma \cup \{(\neg \varphi)\} \vdash (\neg \varphi)$, $\Sigma \cup \{(\neg \varphi)\}$ is inconsistent.
Conversely, suppose that $\Sigma \cup \{(\neg \varphi)\}$ is inconsistent. Then since $\Sigma \cup \{(\neg \varphi)\} \vdash \bot$ by definition, there exists a proof that ends in the following way:
| $\vdots$ | |||||||||||
| |||||||||||
| $n-1$ | $(\neg(\neg \varphi))$ | $\neg$i $k$-$(n-2)$ | |||||||||
| $n$ | $\varphi$ | $\neg\neg$e $(n-1)$ | |||||||||
Therefore, $\Sigma \vdash \varphi$. $$\tag*{$\Box$}$$
Lemma 18.11. For all sets of formulas $\Sigma$ and formulas $\varphi$, $\Sigma \models \varphi$ if and only if $\Sigma \cup \{(\neg \varphi)\}$ is unsatisfiable.
Proof. Observe that by definition, $\Sigma \models \varphi$ if and only if for all interpretations $\mathcal I$ and environments $E$, if $\mathcal I \models_E \Sigma$, then $\mathcal I \models_E \varphi$. This is equivalent to saying that there is no interpretation $\mathcal I$ and environment $E$ such that $\mathcal I \models_E \Sigma$ but $\mathcal I \not \models_E \varphi$. This is also equivalent to saying that there is no interpretation $\mathcal I$ and environment $E$ such that $\mathcal I \models_E \Sigma \cup \{(\neg \varphi)\}$. But this is exactly the definition of unsatisfiability, and therefore $\Sigma \cup \{(\neg \varphi)\}$ is unsatisfiable. $$\tag*{$\Box$}$$
Theorem 18.12 (Henkin's theorem). If $\Sigma$ is consistent, then $\Sigma$ is satisfiable.
This step is the one where all the action happens and there is a formal, proper way to do all of this, but unfortunately we don't have the time or energy for it. To prove this theorem, we must show that there exists an interpretation $\mathcal I$ and environment $E$ such that $\mathcal I \models_E \Sigma$. Keep in mind that at this point, all we have to go on is the set of formulas itself. However, we can also rely on the fact that our set is consistent.
In essence, what we need to do is reverse-engineer a suitable interpretation out of our set of formulas. For example, what is our domain? Well, we'll just make all of the terms that show up in our set of formulas our domain. Then, once we have set our domain, we can look at each predicate that occurs in our set of formulas and define them in such a way that makes every formula true. We can do this because we already know our set of formulas is consistent.
This is obviously a huge simplification of what we would need to do to formally prove this theorem. As one example, does it really make sense to make every term that occurs a distinct element of the domain? No, of course not, and so defining our domain really involves carefully defining an equivalence relation on terms.
Unfortunately, going any further into the details is beyond the scope of this course. This may be unsatisfying for some of you. If that is the case, you should take PMATH 432.
The proof of completeness then simply puts these three results together.
Proof of Theorem 18.9. We have $\Sigma \models \varphi$. Suppose that $\Sigma \not \vdash \varphi$. Then by Lemma 18.10, since $\Sigma \not \vdash \varphi$, we have that $\Sigma \cup \{(\neg \varphi)\}$ is consistent. By Theorem 18.12, this means that $\Sigma \cup \{(\neg \varphi)\}$ is satisfiable. Then, by Lemma 18.11, this means that $\Sigma \not \models \varphi$, which contradicts that $\Sigma \models \varphi$. Thus, $\Sigma \vdash \varphi$. $$\tag*{$\Box$}$$
One of the interesting observations about this proof is that it is not effective. Unlike the proof of completeness for propositional logic, we don't construct a proof to show that one exists. As mentioned before, there is no way to brute-force check every interpretation in the same way that we did with valuations, since there are only finitely many valuations and infinitely many interpretations.
Given an arbitrary formula in predicate logic, if we know that the formula has a proof, then finding the proof is not too difficult: we just systematically enumerate every string and see if it is a proof of our formula. If our formula is provable, then this algorithm will find it eventually. But what if our formula doesn't have a proof? Then we are in a bit of a pickle.
Completeness tells us that if we want to show that a formula is not valid, then all we need to do is find an interpretation under which it is not satisfied. The "all we need" in the previous sentence does a lot of work here, since even finding a single sufficient interpretation still involves searching through infinitely many possible interpretations.
As it turns out, the problem of determining whether a formula is valid or provable is undecidable. That is, there is no algorithm that can tell you whether a given formula is provable or not. This result was shown by Alonzo Church in 1936. Church is the Church in Church-Turing thesis and, among other things, defined the lambda calculus and was Alan Turing's doctoral advisor.
Church's proof of the undecidability of validity of first-order formulas is dependent on another result of Gödel, his incompleteness theorem. Now, it seems a bit strange, you might say, that Gödel proved the completeness of first-order logic and then just a few years later, proved the incompleteness theorem. It turns out that the use of completeness in these two results is slightly different (the incompleteness theorem is about the completeness of a theory, which is a proof system together with a set of axioms).
Both the incompleteness theorem and Church's proof of undecidability of validity in their original forms are complicated and both are made much simpler once we have the concept of a computer. We may talk about this more closer to the end of the course.