So after a long treatise on proof systems, we are ready to begin answering those questions about proof and truth that I keep bringing up.
Definition 9.1. We say a proof system is sound if whenever $\Sigma \vdash \varphi$, then $\Sigma \models \varphi$. We say a proof system is complete if whenever $\Sigma \models \varphi$, then $\Sigma \vdash \varphi$.
Soundness says that if we have a proof in our proof system, then it says something about the relationship of the formulas involved under all valuations. Completeness says that for a particular relationship between valuations of formulas, there must exist a proof for the same set of formulas.
For example, if we think about those statements that have no formulas on the left hand side ($\emptyset \vdash \varphi$ and $\emptyset \models \varphi$), we have a relationship between theorems and tautologies. Soundness says that every theorem is a tautology and completeness says that every tautology is a theorem. This maps to our understanding of what a theorem is: it's a mathematical property that is always true, and we know this because we have (presumably) proved it.
So it is fairly obvious that "proofs" have a connection with proofs and theorems and now we have linked this idea to truth and tautology, but what else is there? Back when we started talking about negation, I mentioned a bunch of stuff about how we can think of all of this proof stuff as talking about what happens when we know we have a proof for something, rather than the usual notions of true or false. This, of course, leads to some complications about what it means to negate something. In particular, this causes a problem with $\neg\neg e$.
Let's think about what it means under what we call the intuinistic interpretation of propositional logic. If we have $(\neg(\neg \varphi))$, what this says is that we do not have a proof that there is no proof of $\varphi$. From this perspective, we can't get $\varphi$ from $(\neg(\neg \varphi))$ and so if we were intuitionists, we can't use this rule. This has wider ranging consequences in that we are no longer to make use of proof by contradiction or the law of excluded middle.
Under an intuitionistic interpretation of natural deduction, we would reject the $\neg\neg e$ rule from our system. However, this means that we can no longer prove the law of excluded middle in this system (for an exercise, give it a shot). This implies that intuitionistic natural deduction is not complete. We know from our examination of semantics in propositional logic that $(p \vee (\neg p))$ is a tautology. However, we would never be able to prove it in intuitionistic propositional logic.
Then are there proof systems that are complete but not sound? Sure, and this is even easier to come up with. Let's add the following rule to natural deduction: $$\frac{\quad}{(\alpha \wedge (\neg \alpha))}.$$ Then any proof system with this rule will have $\emptyset \vdash (\alpha \wedge (\neg \alpha))$. In fact, it's not difficult to show that in this proof system we will be able to prove $\Sigma \vdash \varphi$ for any $\Sigma$ and $\varphi$. In this case, if we have $\Sigma \models \varphi$, we can definitely prove $\Sigma \vdash \varphi$, so our contrived proof system is complete. However, our proof system is not sound, since $\emptyset \not\models (\alpha \wedge (\neg \alpha))$.
These are some simple examples of how often we take the notions of truth and proof as synonymous for granted. Luckily, the soundness and completeness of (classical) propositional logic was shown by Emil Post in 1920 in his PhD thesis. He showed this for another proof system, described in Principia Mathematica, by Whitehead and Russell. This proof system for propositional logic contained a set of axioms and only substitution and modus ponens rules. As it turns out, Post will go on to make some important contributions in early computability theory.
Theorem 9.2. (Soundness) If $\Sigma \vdash \varphi$, then $\Sigma \models \varphi$.
Proof. Let $\Sigma = \{\alpha_1, \dots, \alpha_n\}$. Since $\Sigma \vdash \varphi$, there must be a proof that uses only the natural deduction rules and no derived rules. We will show that $\Sigma \models \varphi$ by induction on the length of the proof of $\Sigma \vdash \varphi$.
For the base case, a minimal proof must have at least one line. Then if the proof for $\Sigma \vdash \varphi$ has one line, it must be of the form
| 1 | $\varphi$ | premise |
This means we have $\varphi \in \Sigma$ and therefore, $\Sigma \models \varphi$.
For the inductive step, we assume that soundness holds for all $\Sigma \vdash \varphi$ with proofs of length less than $k$. In this case, we know that the $k$th and final line of any such proof must be
| $k$ | $\varphi$ | (rule) |
The rest of the proof depends on which rule we apply to get the $k$th line. Since natural deduction has a number of rules, we will have to consider each case (luckily, we chose not to include derived rules). Many of the cases follow the same kind of argument, so we will only go through a few.
(Case $\wedge i$). Suppose that on the $k$th line, we apply $\wedge i$, as follows
| $k$ | $\varphi$ | $\wedge i$ $k_1, k_2$ |
In this case, we know that $\varphi = \psi_1 \wedge \psi_2$ for some formulas $\psi_1$ and $\psi_2$, and that $\psi_1$ appears on line $k_1$ and $\psi_2$ appears on line $k_2$. This means that we have $\Sigma \vdash \psi_1$ and $\Sigma \vdash \psi_2$. Furthermore, the length of the proof of $\Sigma \vdash \psi_1$ is at most $k_1$ and the length of the proof of $\Sigma \vdash \psi_2$ is at most $k_2$. Since $k_1, k_2 < k$, by our inductive hypothesis, we can conclude $\Sigma \models \psi_1$ and $\Sigma \models \psi_2$.
Since these entailments hold, we know that if $\Sigma^t = T$, then $\psi_1^t = T$ and $\psi_2^t = T$. Because $\varphi = \psi_1 \wedge \psi_2$, we have $\varphi^t = (\psi_1 \wedge \psi_2)^t = T$ whenever $\Sigma^t = T$. Therefore, $\Sigma \models \varphi$.
The other main type of rule that we need to consider are those rules that rely on subproofs.
(Case $\rightarrow\!i$). For instance, if on the $k$th line, we apply $\rightarrow\!i$, this means our proof looks like the following:
| $\vdots$ | |||||||||||
| |||||||||||
| $k$ | $(\alpha \rightarrow \beta)$ | $\wedge i$ $i$-$k-1$ | |||||||||
It is not entirely obvious how to come up with a shorter proof just by removing the $k$th line. However, we can modify this proof as follows:
| $\vdots$ | ||
| $i$ | $\alpha$ | premise |
| $\vdots$ | ||
| $k-1$ | $\beta$ | (rule) |
This is a proof for $\Sigma \cup \{\alpha\} \vdash \beta$ of length at most $k-1$. Since our proof is of length less than $k$, we can apply our inductive hypothesis and we have $\Sigma \cup \{\alpha\} \models \beta$. We will use this entailment to show that the entailment $\Sigma \models (\alpha \rightarrow \beta)$ holds.
Consider a valuation $t$ that satisfies $\Sigma$ and assume that $\Sigma \models (\alpha \rightarrow \beta)$ does not hold under this valuation. Then we must have $(\alpha \rightarrow \beta)^t = F$. By the definition of $\rightarrow$, we know that we must have that $\alpha^t = T$ while $\beta^t = F$. However, this contradicts that the entailment $\Sigma \cup \{\alpha\} \models \beta$ holds. Therefore, we cannot have $(\alpha \rightarrow \beta)^t = F$ when $\Sigma^t = T$ and therefore, the entailment $\Sigma \models (\alpha \rightarrow \beta)$ holds.
(Case $\vee e$). Suppose on the $k$th line, we apply $\vee e$. Here, we have a few things to consider. First, we know that on some line $k' < k$, we have a disjunction $(\alpha \vee \beta)$ upon which we apply $\vee e$. Secondly, we have to consider two subproofs: one beginning with an assumption on $\alpha$ and another beginning with an assumption on $\beta$ and both concluding with $\psi$. Just like with $\rightarrow\!i$, we can rewrite our proof so that $\alpha$ and $\beta$ are premises and we know that both of these proofs will have length less than $k$. Putting these facts together, we have the following entailments by our inductive hypothesis.
Using these three entailments, we will show that we must have $\Sigma \models \psi$. Suppose for contradiction that this entailment does not hold. This means that there exists a valuation $t$ such that $\Sigma^t = T$ and $\psi^t = F$. Observe that since $\Sigma^t = T$, we must have $(\alpha \vee \beta)^t = T$ by entailment (1). This means we must have at least one of $\alpha^t = T$ or $\beta^t = T$.
Suppose $\alpha^t = T$. However, this contradicts entailment (2), since $\Sigma^t = T$ and $\psi^t = F$. Then $\alpha^t = F$. By a similar argument, we must conclude that $\beta^t = F$ since otherwise, entailment (3) would be contradicted. But then this valuation contradicts entailment (1) and we must conclude that such a valuation cannot exist. Therefore, $\Sigma \models \psi$.
The two cases $\wedge i$ and $\rightarrow\!i$ cover the main proof ideas for showing that soundness holds. For a complete proof, we will need to examine and argue about each natural deduction rule. After doing so for all the cases, we would then be able to conclude that we have shown that if $\Sigma \vdash \varphi$, then $\Sigma \models \varphi$. $$\tag*{$\Box$}$$
The notion of soundness is already very useful even without completeness. For instance, suppose we want to show that a proof doesn't exist. Without soundness, it isn't clear how we would do this. Certainly, we can say that we don't know if a proof exists or not since we aren't able to find one, but there's always the possibility that maybe we just weren't clever enough to find it. Soundness finally lets us do what many of you have been trying to do over the last week or so: appeal to our understanding of semantics. Soundness tells us if we have $\Sigma \not \models \varphi$, then $\Sigma \not \vdash \varphi$. So proving the non-existence of a proof comes down to showing that the equivalent entailment doesn't hold.
Example 9.3. Let $\Sigma, \varphi$ be such that $\Sigma \models \varphi$. Then does $\Sigma \not \models (\neg \varphi)$? The answer to this turns out to be no. A simple example would be $\Sigma = \{\varphi, (\neg \varphi)\}$. However, recall that if $\Sigma$ is unsatisfiable, then we have both $\Sigma \models \varphi$ and $\Sigma \models (\neg \varphi)$. Soundness gives us a bit of insight into what may be going on. Any unsatisfiable set will be inconsistent and therefore, will give us a contradiction in the proof setting, after which we may conclude anything.
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$).
The notions of satisfiability and consistency are related, but not the same, in the same way that the notions of proof and truth are not the same, but related (at least once we finish proving that this is the case).