Intro

Last time, we built a computer system that can prove propositional formulas using a set of 3 axioms and MP. It was proven that it was sound, and then I claimed that it was complete without actually proving it. Let’s continue, and then also cover adequacy, inconsistency, compactness, decidability. Go back and read the post on propositional logic proofs if you need a reminder of our proof system or the Deduction Theorem. I will keep using $\Gamma\vdash\phi$ for “there is a formal proof of $\phi$ from $\Gamma$” and $\Gamma\models\phi$ for “every assignment satisfying $\Gamma$ also satisfies $\phi$.”

Math

Inconsistency

Before we can prove completeness, let’s define inconsistency

Definition (Inconsistent): A set of formulas $\Gamma$ is inconsistent if there is some formula $\psi$ for which both $\Gamma\vdash\psi$ and $\Gamma\vdash\neg\psi$. Otherwise, $\Gamma$ is consistent.

This is about what our computer can prove. Recall that $\Gamma$ is unsatisfiable if there is no truth assignment that makes every formula in $\Gamma$ true. That is about what the formulas mean.

We know from soundness that an inconsistent set of formulas must be unsatisfiable, because there exists no assignment that can make both $\psi$ and $\neg\psi$ true at the same time. Adequacy is the reverse idea, eg: if a set of formulas is unsatisfiable, then it is inconsistent. This is the hard part of completeness, and we will prove it in the next section.

First, let’s quickly show that an inconsistent set of formulas can prove any formula. Suppose $\Gamma\vdash\psi$ and $\Gamma\vdash\neg\psi$, and we want to prove $\chi$. Axiom (A1) gives us $\psi\to(\neg\chi\to\psi)$ and $\neg\psi\to(\neg\chi\to\neg\psi)$. Using MP, we therefore get both $\neg\chi\to\psi$ and $\neg\chi\to\neg\psi$. Axiom (A3), with $\phi=\chi$, says

Two more uses of MP give us $\Gamma\vdash\chi$. This is our formal version of “from a contradiction, anything follows.”

Adequacy

This is a different use of adequacy from the adequacy of connectives in the first propositional logic post. There, adequacy meant “a small collection of connectives could express every truth function”. Here, it means that our proof system can detect an impossible collection of formulas. Confusing, I know

Theorem (Adequacy): If $\Gamma$ is unsatisfiable, then $\Gamma$ is inconsistent.

Another perspective: if $\Gamma$ is consistent, then it should have a satisfying truth assignment. This is the contrapositive of the theorem, and it is easier to prove. We will build a truth assignment from a consistent set of formulas.

Proof: There are only countably many formulas, since each formula is a finite string made from countably many variables and finitely many symbols. List them as $\phi_1,\phi_2,\ldots$, and set $\Gamma_0=\Gamma$. For each $n\geq 1$, choose

We should check that the second choice is always safe. Suppose $\Gamma_{n-1}\cup\{\phi_n\}$ and $\Gamma_{n-1}\cup\{\neg\phi_n\}$ were inconsistent. The latter would prove some $\psi$ and $\neg\psi$. By the Deduction Theorem, $\Gamma_{n-1}$ would prove both $\neg\phi_n\to\psi$ and $\neg\phi_n\to\neg\psi$. Axiom (A3) and MP would then give $\Gamma_{n-1}\vdash\phi_n$. But if $\phi_n$ can be proven by $\Gamma_{n-1}$, any contradiction proven after adding $\phi_n$ was also provable before adding $\phi_n$. That is a contradiction because it would make $\Gamma_{n-1}$ inconsistent. Thus, all $\Gamma_n$ stay consistent.

Now let $\Gamma^*=\bigcup_{n\geq 0}\Gamma_n$. This union is still consistent. Any proof is finite, so a proof of a contradiction from $\Gamma^*$ would use only finitely many assumptions. All of them would already occur in some one $\Gamma_n$, which we know is consistent.

Thus for all formula $\phi$, only one of $\phi$ and $\neg\phi$ belongs to $\Gamma^*$. Thus, when we consider $\phi$, add one of them, and consistency prevents us from adding both.

Another useful consequence: if $\Gamma^*\vdash\phi$, then $\phi\in\Gamma^*$. Otherwise $\neg\phi\in\Gamma^*$, giving a contradiction. We have made a set that contains every formula it proves.

Define a truth assignment $\mathcal{A}$ by saying that a propositional variable $P$ is true exactly when $P\in\Gamma^*$. The part we need to prove is

We can do this by structural induction on $\phi$.

• Variable: This holds by definition of $\mathcal{A}$.
• Negation: $\psi$ is true when $\psi\in\Gamma^*$ by induction. Since exactly one of $\psi$ and $\neg\psi$ is in $\Gamma^*$, $\neg\psi$ is true exactly when $\neg\psi\in\Gamma^*$.
• Implication: Suppose $\psi\to\chi\in\Gamma^*$. If $\psi$ is true, then $\psi\in\Gamma^*$ by induction, so MP gives $\Gamma^*\vdash\chi$. Thus $\chi\in\Gamma^*$ and $\chi$ is true. This means $\psi\to\chi$ is true. In the converse, let $\psi\to\chi$ be true. If $\chi$ is true, then $\chi\in\Gamma^*$, and (A1) gives $\Gamma^*\vdash\psi\to\chi$. If $\psi$ is false, then $\neg\psi\in\Gamma^*$. Assuming $\psi$ as well would give a contradiction, and that would let us prove $\chi$; by the Deduction Theorem $\Gamma^*\vdash\psi\to\chi$. Either way, our earlier observation concludes $\psi\to\chi$ in $\Gamma^*$.

That’s the induction; we have shown that $\mathcal{A}$ makes exactly the formulas in $\Gamma^*$ true, thus $\Gamma$ is satisfiable, and we have proven adequacy.

Completeness

Now the theorem from last time finally has a proof.

Theorem (Completeness of Propositional Logic): If $\Gamma\models\phi$, then $\Gamma\vdash\phi$.

Proof: If every model of $\Gamma$ satisfies $\phi$, then $\Gamma\cup\{\neg\phi\}$ has no model. Adequacy says this set is inconsistent, so for some $\psi$ it proves both $\psi$ and $\neg\psi$. Apply the Deduction Theorem to both proofs. We get

But (A3) is $(\neg\phi\to\neg\psi)\to((\neg\phi\to\psi)\to\phi)$. Two applications of MP give $\Gamma\vdash\phi$. So our “computer” can prove everything that is true under every assignment satisfying its assumptions.

Compactness

A clean consequence of the fact that formal proofs only use finitely many assumptions:

Theorem (Propositional Compactness): A set of propositional formulas $\Gamma$ is satisfiable iff. every finite subset of $\Gamma$ is satisfiable.

Proof: If one assignment satisfies all of $\Gamma$, it obviously satisfies every subset.

For the other direction, suppose all finite subsets are not satisfiable. If $\Gamma$ were inconsistent, its proof of some $\psi$ and $\neg\psi$ would together use finitely many assumptions from $\Gamma$. That finite subset would be inconsistent, and soundness would make it unsatisfiable, a contradiction. Thus $\Gamma$ is consistent, and adequacy admits a model of $\Gamma$.

You will frequently cite this theorem to show that a set of formulas is unsatisfiable. If you can find a finite subset that is unsatisfiable, then the whole set is unsatisfiable.

Decidability

The last major idea for propositional logic is decidability.

Theorem (Decidability of Propositional Logic): Given a finite set of formulas $\Gamma$ and a formula $\phi$, there is an algorithm that determines whether $\Gamma\vdash\phi$.

This is useful because it means we can write some program for our “computer” that will stop and tell us if the proof exists, eg $\Gamma\vdash\phi$.

Proof: List the variables appearing in $\Gamma$ or $\phi$. Since there are finitely many, we can make a truth table with a row for all assignments, to those variables. Check all rows where all formulas in $\Gamma$ are true. If $\phi$ is true in all of them, then $\Gamma\models\phi$, and by completeness $\Gamma\vdash\phi$. If there is a row where $\Gamma$ is true and $\phi$ is false, by soundness $\Gamma\nvdash\phi$. Regardless of which case, we are done.

End

Next time: FOL!