## You are here

Homesome meta-theorems of propositional logic

## Primary tabs

# some meta-theorems of propositional logic

Based on the axiom system in this entry, we will prove some meta-theorems of propositional logic. In the discussion below, $\Delta$ and $\Gamma$ are sets of well-formed formulas (wff’s), and $A,B,C,\ldots$ are wff’s.

1. (Deduction Theorem) $\Delta,A\vdash B$ iff $\Delta\vdash A\to B$.

2. (Proof by Contradiction) $\Delta,A\vdash\perp$ iff $\Delta\vdash\neg A$.

3. (Proof by Contrapositive) $\Delta,A\vdash\neg B$ iff $\Delta,B\vdash\neg A$.

4. (Law of Syllogism) If $\Delta\vdash A\to B$ and $\Gamma\vdash B\to C$, then $\Delta,\Gamma\vdash A\to C$.

5. $\Delta\vdash A$ and $\Delta\vdash B$ iff $\Delta\vdash A\land B$.

6. $\Delta\vdash A\leftrightarrow B$ iff $\Delta,A\vdash B$ and $\Delta,B\vdash A$.

7. If $\Delta\vdash A\leftrightarrow B$, then $\Delta\vdash B\leftrightarrow A$.

8. If $\Delta\vdash A\leftrightarrow B$ and $\Delta\vdash B\leftrightarrow C$, then $\Delta\vdash A\leftrightarrow C$.

9. $\Delta\vdash A\land B\to C$ iff $\Delta\vdash A\to(B\to C)$.

10. 11. (Substitution Theorem) If $\vdash B_{i}\leftrightarrow C_{i}$, then $\vdash A[\overline{B}/\overline{p}]\leftrightarrow A[\overline{C}/\overline{p}]$.

12. $\Delta\vdash\perp$ iff there is a wff $A$ such that $\Delta\vdash A$ and $\Delta\vdash\neg A$.

13. If $\Delta,A\vdash B$ and $\Delta,\neg A\vdash B$, then $\Delta\vdash B$.

Remark. The theorem schema $A\to\neg\neg A$ is used in the proofs below.

###### Proof.

The first three are proved here, and the last three are proved here. We will prove the rest here, some of which relies on the deduction theorem.

4. From $\Delta\vdash A\to B$, by the deduction theorem, we have $\Delta,A\vdash B$. Let $\mathcal{E}_{1}$ be a deduction of $B$ from $\Delta\cup\{A\}$, and $\mathcal{E}_{2}$ be a deduction of $B\to C$ from $\Gamma$, then

$\mathcal{E}_{1},\mathcal{E}_{2},C$ is a deduction of $C$ from $\Delta\cup\{A\}\cup\Gamma$, so $\Delta,A,\Gamma\vdash C$, and by the deduction theorem again, we get $\Delta,\Gamma\vdash A\to C$.

5. $(\Rightarrow)$. Since $A\land B$ is $\neg(A\to\neg B)$, by the deduction theorem, it is enough to show $\Delta,A\to\neg B\vdash\perp$. Suppose $\mathcal{E}_{1}$ is a deduction of $A$ from $\Delta$ and $\mathcal{E}_{2}$ is a deduction of $B$ from $\Delta$, then

$\mathcal{E}_{1},\mathcal{E}_{2},A\to\neg B,\neg B,\perp$ is a deduction of $\perp$ from $\Delta\cup\{A\to\neg B\}$.

$(\Leftarrow)$. We first show that $\Delta\vdash B$. Now, $\neg B\to(A\to\neg B)$ is an axiom and $\vdash(A\to\neg B)\to\neg\neg(A\to\neg B)$ is a theorem, $\vdash\neg B\to\neg\neg(A\to\neg B)$, so that by modus ponens, $\vdash\neg(A\to\neg B)\to B$, using axiom schema $(\neg C\to\neg D)\to(D\to C)$. Since by assumption $\Delta\vdash\neg(A\to\neg B)$, by modus ponens again, we get $\Delta\vdash B$.

We next show that $\Delta\vdash A$. From the deduction $A,A\to\perp,\perp$, we have $A,\neg A\vdash\perp$, so certainly $\Delta,\neg A,A,B\vdash\perp$. By three applications of the deduction theorem, we get $\Delta\vdash\neg A\to(A\to\neg B)$. By theorem $(A\to\neg B)\to\neg\neg(A\to\neg B)$, $\Delta\vdash\neg A\to\neg\neg(A\to\neg B)$. By axiom schema $(\neg C\to\neg D)\to(D\to C)$ and modus ponens, we get $\Delta\vdash\neg(A\to\neg B)\to A$. Since $\Delta\vdash\neg A\to\neg B$ by assumption, $\Delta\to A$ as a result.

6. $\Delta\vdash A\leftrightarrow B$ iff $\Delta\vdash A\to B$ and $\Delta\vdash B\to A$ iff $\Delta,A\vdash B$ and $\Delta,B\vdash A$.

7. Apply 6 to $\Delta\vdash A\to B$ and $\Delta\vdash B\to A$.

8. Apply 5 and 6.

9. Since $\Delta,A\vdash B\to A\land B$ by the theorem schema $\vdash A\to(B\to A\land B)$, together with $\Delta\vdash A\land B\to C$, we have $\Delta,A\vdash B\to C$ by law of syllogism, or equivalently $\Delta\vdash A\to(B\to C)$, by the deduction theorem. Conversely, $\Delta,A\vdash B\to C$ and theorem schema $A\land B\to B$ result in $\Delta,A\vdash A\land B\to C$ by law of syllogism. So $\Delta\vdash A\to(A\land B\to C)$ by the deduction theorem. But $A\land B\to A$ is a theorem schema, $\Delta\vdash A\land B\to(A\land B\to C)$, and therefore $\Delta\vdash A\land B\to C$ by the theorem schema $(X\to(X\to Y))\leftrightarrow(X\to Y)$.

10. Assume the former. Then a deduction of $B$ from $\Delta$ may or may not contain $A$. In either case, $\Delta,A\vdash B$, so $\Delta\vdash A\to B$ by the deduction theorem. Next, assume the later. Let $\mathcal{E}_{1}$ be a deduction of $A\to B$ from $\Delta$. Then if $\mathcal{E}_{2}$ is a deduction of $A$ from $\Delta$, then $\mathcal{E}_{1},\mathcal{E}_{2},B$ is a deduction of $B$ from $\Delta$, and therefore $\Delta\vdash B$.

To see the last meta-theorem implies the deduction theorem, assume $\Delta,A\vdash B$. Suppose $\Delta\vdash A$. Let $\mathcal{E}_{1}$ be a deduction of $A$ from $\Delta$, and $\mathcal{E}_{2}$ a deduction of $B$ from $\Delta\cup\{A\}$. Then $\mathcal{E}_{1},\mathcal{E}_{2}$ is a deduction of $B$ from $\Delta$. So $\Delta\vdash B$. As a result $\Delta A\to B$ by the statement of the meta-theorem. ∎

Remark. Meta-theorems 7 and 8, together with the theorem schema $A\leftrightarrow A$, show that $\leftrightarrow$ defines an equivalence relation on the set of all wff’s of propositional logic. Formally, for any two wff’s $A,B$, if we define $A\sim B$ iff $\vdash A\leftrightarrow B$, then $\sim$ is an equivalence relation.

## Mathematics Subject Classification

03B05*no label found*

- Forums
- Planetary Bugs
- HS/Secondary
- University/Tertiary
- Graduate/Advanced
- Industry/Practice
- Research Topics
- LaTeX help
- Math Comptetitions
- Math History
- Math Humor
- PlanetMath Comments
- PlanetMath System Updates and News
- PlanetMath help
- PlanetMath.ORG
- Strategic Communications Development
- The Math Pub
- Testing messages (ignore)

- Other useful stuff
- Corrections