Rules of Inference

Discrete Mathematics — Lesson 5 (Full Course)

Notes By Pr. El Hadiq Zouhair

1 / 30

Outline of the course

  1. Foundations — argument, premises, conclusion, validity, soundness.
  2. Logical consequence $\Gamma \models \varphi$ and the deduction theorem.
  3. Syntactic vs semantic derivation: $\vdash$ vs $\models$.
  4. Why inference rules? — efficiency over truth tables.
  5. The eight propositional rules — each one stated, proved valid, illustrated.
  6. The two classical fallacies — proved invalid by counter-example.
  7. Building a natural-deduction proof — structure and notation.
  8. Two worked propositional proofs (Resolution-based; six-variable cascade).
  9. The four quantifier rules — UI, UG, EI, EG — with proofs and side conditions.
  10. Counter-examples showing why the side conditions are necessary.
  11. A mixed propositional / predicate worked example.
  12. Derived rules (constructive dilemma, destructive dilemma).
  13. Soundness theorem (proved) and completeness theorem (statement + sketch).
  14. Summary, Wolfram → Python reference, bibliography.

References: Rosen 8e §1.6; Velleman 3e §3.1–3.3; Mendelson 6e ch. 1–2; Cori & Lascar vol. 1 ch. 2; Lalement Logique, réduction, résolution.

2 / 30

1.1 Argument, premises, conclusion, validity

An argument is a finite list of formulas $\varphi_1, \varphi_2, \ldots, \varphi_n$ — called premises (or hypotheses) — together with a distinguished formula $\psi$ — the conclusion. We write it in natural-deduction fraction form: $$\dfrac{\varphi_1,\;\varphi_2,\;\ldots,\;\varphi_n}{\psi}.$$ The argument is valid if in every valuation (interpretation) that makes all premises true, the conclusion is also true. Equivalently, $\{\varphi_1, \dots, \varphi_n\} \models \psi$.
Validity is a structural property of the form of the argument — it has nothing to do with the real-world truth of the premises. An argument can be valid with false premises, and invalid with true premises.

Reading the fraction bar: "from $\varphi_1, \dots, \varphi_n$ we may infer $\psi$".

Rosen 8e §1.6, p. 73; Mendelson 6e §1.5.

3 / 30

1.2 Soundness of an argument

An argument is sound iff it is valid and all of its premises are actually true (in the intended interpretation). Soundness implies that the conclusion is true.
ValidityPremises true?Conclusion guaranteed?Sound?
ValidAll trueYesSound
ValidSome falseNo (irrelevant)Not sound
InvalidAnythingNoNot sound
"All primes are odd; $2$ is prime; therefore $2$ is odd." The argument-form $\forall x(P(x) \to Q(x)),\;P(c)\;\vdash\;Q(c)$ is valid. But the first premise is false, so the argument is not sound — the conclusion happens to be false.

In this course we focus on validity: a purely structural check that the inference is correct. Soundness is left to the user, who must verify the premises are true in the situation at hand.

Velleman 3e §1.5; Rosen 8e §1.6.

4 / 30

2. Logical consequence and the deduction theorem

Let $\Gamma$ be a set of formulas and $\varphi$ a formula. We say $\varphi$ is a logical consequence of $\Gamma$ (or $\Gamma$ entails $\varphi$), written $\Gamma \models \varphi$, iff every valuation that makes all formulas of $\Gamma$ true also makes $\varphi$ true.
Deduction theorem (semantic). For any $\Gamma, \varphi, \psi$, $$\Gamma \cup \{\varphi\} \models \psi \;\;\Longleftrightarrow\;\; \Gamma \models \varphi \to \psi.$$
(⇒) Suppose $\Gamma \cup \{\varphi\} \models \psi$. Let $v$ be any valuation satisfying $\Gamma$. Two cases: if $v(\varphi) = \mathtt F$, then $v(\varphi \to \psi) = \mathtt T$ vacuously; if $v(\varphi) = \mathtt T$, then $v$ satisfies $\Gamma \cup \{\varphi\}$, hence $v(\psi) = \mathtt T$, hence $v(\varphi \to \psi) = \mathtt T$.
(⇐) Suppose $\Gamma \models \varphi \to \psi$. Let $v$ satisfy $\Gamma \cup \{\varphi\}$. Then $v(\varphi \to \psi) = \mathtt T$ (by hypothesis) and $v(\varphi) = \mathtt T$ (since $\varphi \in \Gamma \cup \{\varphi\}$), so $v(\psi) = \mathtt T$. $\square$

Mendelson 6e §1.5, Theorem 1.10; Cori & Lascar vol. 1 ch. 2.

5 / 30

3. Syntactic ($\vdash$) vs semantic ($\models$)

Fix a finite set $\mathcal{R}$ of inference rules. A derivation (or proof) of $\psi$ from $\Gamma$ is a finite sequence of formulas $\varphi_1, \varphi_2, \ldots, \varphi_n = \psi$ such that each $\varphi_i$ is either an element of $\Gamma$, an axiom, or follows from earlier $\varphi_j$'s by a rule of $\mathcal{R}$. We write $\Gamma \vdash \psi$ when such a derivation exists.

The relation $\Gamma \models \psi$ is semantic (about valuations). The relation $\Gamma \vdash \psi$ is syntactic (about formal proofs). They are connected by two foundational theorems:

DirectionTheoremMeaning
$\vdash \Rightarrow \models$SoundnessEvery theorem is true: derivations preserve validity (slide 26).
$\models \Rightarrow \vdash$CompletenessEvery truth is provable: anything entailed is also derivable (slide 27).

Mendelson 6e §1.6 (soundness), §2.4 (completeness); Cori & Lascar vol. 1.

6 / 30

4. Why inference rules? — vs truth tables

For a formula on $n$ propositional variables, a truth table has $2^n$ rows.

$n$ atomsRows
532
101 024
20$\approx 10^6$
50$\approx 10^{15}$
100$\approx 10^{30}$
Truth-table checking is complete (it always works) but exponential. Rules of inference give a structured, often-polynomial way to manipulate symbols and reach the conclusion without enumerating valuations — exactly how human mathematicians prove things.

Beyond efficiency, inference rules also generalise to predicate logic, where the universe may be infinite and truth tables make no sense at all.

Rosen 8e §1.6, p. 73; Lalement, ch. 3.

7 / 30

5. The eight propositional rules — overview

Each rule is written as $\dfrac{\text{premises}}{\text{conclusion}}$. We prove the validity of each one in the next eight slides.

$\dfrac{p,\;\; p \to q}{q}$Modus Ponens
$\dfrac{\neg q,\;\; p \to q}{\neg p}$Modus Tollens
$\dfrac{p \to q,\;\; q \to r}{p \to r}$Hyp. Syllogism
$\dfrac{p \vee q,\;\; \neg p}{q}$Disj. Syllogism
$\dfrac{p}{p \vee q}$Addition
$\dfrac{p \wedge q}{p}$Simplification
$\dfrac{p,\;\; q}{p \wedge q}$Conjunction
$\dfrac{p \vee q,\;\; \neg p \vee r}{q \vee r}$Resolution

General validity criterion: $\dfrac{\varphi_1,\ldots,\varphi_n}{\psi}$ is valid iff the formula $\varphi_1 \wedge \cdots \wedge \varphi_n \wedge \neg\psi$ is unsatisfiable — i.e. there is no valuation making the premises true and the conclusion false simultaneously. We will use this criterion in every proof below.

Rosen 8e §1.6, Table 1, p. 75.

8 / 30

5.1 Modus Ponens (MP)

$\{p,\; p \to q\} \;\models\; q.$  Equivalently: $(p \wedge (p \to q)) \to q$ is a tautology.
Semantic argument. Let $v$ be any valuation satisfying both premises: $v(p) = \mathtt T$ and $v(p \to q) = \mathtt T$. Suppose, for contradiction, that $v(q) = \mathtt F$. Then $v(p \to q) = \mathtt T \to \mathtt F = \mathtt F$, contradicting $v(p \to q) = \mathtt T$. Hence $v(q) = \mathtt T$.
Truth-table argument. Enumerate the four valuations of $(p, q)$ and check the column $(p \wedge (p \to q)) \to q$:
$p$$q$$p \to q$$p \wedge (p \to q)$$\Rightarrow q$
TTTTT
TFFFT
FTTFT
FFTFT
The last column is all $\mathtt T$. $\square$

Rosen 8e §1.6 p. 74; Mendelson 6e §1.5.

9 / 30

5.2 Modus Tollens (MT)

$\{\neg q,\; p \to q\} \;\models\; \neg p.$
Let $v$ satisfy both premises: $v(\neg q) = \mathtt T$ (so $v(q) = \mathtt F$) and $v(p \to q) = \mathtt T$. Suppose $v(p) = \mathtt T$. Then $v(p \to q) = \mathtt T \to \mathtt F = \mathtt F$, contradicting $v(p \to q) = \mathtt T$. Hence $v(p) = \mathtt F$, i.e. $v(\neg p) = \mathtt T$. $\square$
Alternative proof. Recall the contrapositive equivalence $p \to q \;\equiv\; \neg q \to \neg p$ (proved in Lesson 2). Substituting into the premise gives $\{\neg q,\; \neg q \to \neg p\} \models \neg p$ — which is exactly Modus Ponens on $\neg q$ and $\neg q \to \neg p$.
From "If I work, I am tired" and "I am not tired", we conclude "I do not work".

Rosen 8e §1.6 p. 75.

10 / 30

5.3 Hypothetical Syllogism (HS)

$\{p \to q,\; q \to r\} \;\models\; p \to r.$
Let $v$ satisfy both premises. We show $v(p \to r) = \mathtt T$ by cases on $v(p)$.
Case $v(p) = \mathtt F$. Then $v(p \to r) = \mathtt T$ vacuously.
Case $v(p) = \mathtt T$. Since $v(p \to q) = \mathtt T$ and $v(p) = \mathtt T$, by the truth table of $\to$ we get $v(q) = \mathtt T$. Since $v(q \to r) = \mathtt T$ and $v(q) = \mathtt T$, similarly $v(r) = \mathtt T$. Hence $v(p \to r) = \mathtt T \to \mathtt T = \mathtt T$. $\square$

This is the formal version of "transitivity of implication". Chaining HS gives the general principle:

$$\{p_1 \to p_2,\; p_2 \to p_3,\; \ldots,\; p_{n-1} \to p_n\} \;\models\; p_1 \to p_n.$$

Rosen 8e §1.6 p. 75; Velleman 3e §1.2.

11 / 30

5.4 Disjunctive Syllogism (DS)

$\{p \vee q,\; \neg p\} \;\models\; q.$
Let $v$ satisfy both premises: $v(p \vee q) = \mathtt T$ and $v(\neg p) = \mathtt T$, i.e. $v(p) = \mathtt F$. From the truth table of $\vee$, $v(p \vee q) = \mathtt T$ with $v(p) = \mathtt F$ forces $v(q) = \mathtt T$. $\square$
From "I left my keys in the car or in the office" and "they are not in the car", we conclude "they are in the office".

By symmetry of $\vee$, the dual form is also valid: $\{p \vee q,\; \neg q\} \models p$.

Rosen 8e §1.6 p. 75.

12 / 30

5.5 / 5.6 Addition and Simplification

Addition. $\;p \models p \vee q.$
If $v(p) = \mathtt T$, then $v(p \vee q) = \mathtt T \vee v(q) = \mathtt T$ regardless of $v(q)$. $\square$
Simplification. $\;p \wedge q \models p.$
If $v(p \wedge q) = \mathtt T$, then by the truth table of $\wedge$ both $v(p) = \mathtt T$ and $v(q) = \mathtt T$. In particular $v(p) = \mathtt T$. By symmetry, the dual $p \wedge q \models q$ also holds. $\square$
Addition weakens: from $p$ alone you can conclude something less informative ($p \vee q$). Simplification extracts: from a conjunction you can pull out either conjunct. These two rules let you reshape the conclusion to match the next inference step.

Rosen 8e §1.6 p. 75.

13 / 30

5.7 Conjunction (Adjunction)

$\{p,\; q\} \;\models\; p \wedge q.$
If a valuation $v$ satisfies both premises, then $v(p) = \mathtt T$ and $v(q) = \mathtt T$, hence by the truth table of $\wedge$, $v(p \wedge q) = \mathtt T \wedge \mathtt T = \mathtt T$. $\square$

This is the converse of Simplification: it lets you combine two already-derived facts into a single conjunction, often to match the antecedent of a future implication of the form $p \wedge q \to r$.

In the cascade proof of slide 17 we will use Conjunction to combine $r$ (derived at step 5) and $s$ (premise $H_5$) into $r \wedge s$ — exactly the antecedent of hypothesis $H_3: (r \wedge s) \to t$.

Rosen 8e §1.6 p. 75.

14 / 30

5.8 Resolution

$\{p \vee q,\; \neg p \vee r\} \;\models\; q \vee r.$
Let $v$ satisfy both clauses. We split by the value of $v(p)$.
Case $v(p) = \mathtt T$. Then $v(\neg p) = \mathtt F$, so $v(\neg p \vee r) = \mathtt T$ forces $v(r) = \mathtt T$. Hence $v(q \vee r) = \mathtt T$.
Case $v(p) = \mathtt F$. Then $v(p \vee q) = \mathtt T$ forces $v(q) = \mathtt T$. Hence $v(q \vee r) = \mathtt T$.
In both cases $v(q \vee r) = \mathtt T$. $\square$
Why Resolution matters. Resolution is the single inference rule used by automated theorem provers and modern SAT solvers (DPLL/CDCL). Combined with CNF normalisation (Lesson 2), resolution refutation is a complete decision procedure for propositional unsatisfiability.

Sub-cases: $\{p,\; \neg p \vee r\} \models r$ (a special case with $q$ replaced by $\bot$) is exactly Modus Ponens written in disjunctive form, since $\neg p \vee r \equiv p \to r$.

Rosen 8e §1.6 p. 75; Lalement, ch. 3.

15 / 30

6. The two classical fallacies — proved invalid

Affirming the consequent

$\dfrac{p \to q,\; q}{p}$Invalid
Take the valuation $v(p) = \mathtt F$, $v(q) = \mathtt T$. Then $v(p \to q) = \mathtt F \to \mathtt T = \mathtt T$ and $v(q) = \mathtt T$, so both premises hold; yet $v(p) = \mathtt F$, so the conclusion fails. The argument is invalid. $\square$

Denying the antecedent

$\dfrac{p \to q,\; \neg p}{\neg q}$Invalid
Take the same valuation $v(p) = \mathtt F$, $v(q) = \mathtt T$. Then $v(p \to q) = \mathtt T$, $v(\neg p) = \mathtt T$ — both premises hold; yet $v(\neg q) = \mathtt F$, so the conclusion fails. The argument is invalid. $\square$
A single counter-example valuation is enough to refute an argument form. Memorise this valuation $v(p) = \mathtt F,\; v(q) = \mathtt T$ — it breaks both fallacies.

Rosen 8e §1.6 p. 77; Velleman 3e §1.2.

16 / 30

7. Building a natural-deduction proof

A natural-deduction proof of $\Gamma \vdash \psi$ is a numbered list of formulas $\varphi_1, \varphi_2, \ldots, \varphi_n = \psi$ where each $\varphi_i$ is justified by one of: The right-hand justification column names the rule and cites the line numbers used.

Practical workflow:

  1. Write the hypotheses $H_1, H_2, \ldots$ as the first lines.
  2. Identify what the goal looks like — if it is $\alpha \to \beta$, plan an $\to$-intro at the end (assume $\alpha$, derive $\beta$).
  3. Forward-chain: at each step, look for a rule whose premises are already on the page, and add its conclusion as a new line.
  4. Stop when the goal $\psi$ appears as the last line.

Velleman 3e §3.1; Mendelson 6e §1.6.

17 / 30

8.1 Example 1 — proof by Resolution

Let $p, q, r$ be propositional variables. Hypotheses:

LabelFormula
$H_1$$p \vee q$
$H_2$$p \to r$

Goal: derive $r \vee q$.

  1. 1.$p \vee q$$H_1$
  2. 2.$p \to r$$H_2$
  3. 3.$\neg p \vee r$implication identity on (2)
  4. 4.$\dfrac{p \vee q,\;\; \neg p \vee r}{q \vee r}$Resolution (1, 3)
  5. 5.$r \vee q$commutativity of $\vee$  $\square$
Python — entailment check from sympy import symbols, And, Or, Not, Implies from sympy.logic.inference import satisfiable p, q, r = symbols('p q r') premises = And(Or(p, q), Implies(p, r)) goal = Or(r, q) print(satisfiable(And(premises, Not(goal))) is False) # True — entailed

Rosen 8e §1.6 Example 4.

18 / 30

8.2 Example 2 — six-variable cascade

Variables $p, q, r, s, t, u$. Hypotheses:

LabelFormula
$H_1$$p \to q$
$H_2$$q \to r$
$H_3$$(r \wedge s) \to t$
$H_4$$t \to u$
$H_5$$s$

Goal: derive $p \to u$.

  1. 1.$p \to q$$H_1$
  2. 2.$q \to r$$H_2$
  3. 3.$\dfrac{p \to q,\;\; q \to r}{p \to r}$HS (1, 2)
  4. 4.$p$assumption (for $\to$-intro)
  5. 5.$\dfrac{p,\;\; p \to r}{r}$MP (4, 3)
  6. 6.$s$$H_5$
  7. 7.$\dfrac{r,\;\; s}{r \wedge s}$Conjunction (5, 6)
  8. 8.$(r \wedge s) \to t$$H_3$
  9. 9.$\dfrac{r \wedge s,\;\; (r \wedge s) \to t}{t}$MP (7, 8)
  10. 10.$t \to u$$H_4$
  11. 11.$\dfrac{t,\;\; t \to u}{u}$MP (9, 10)
  12. 12.$p \to u$$\to$-intro discharging (4)–(11)  $\square$

Rosen 8e §1.6 Example 5.

19 / 30

9.1 Universal Instantiation (UI)

For any term $c$ of the language, $\;\dfrac{\forall x\, P(x)}{P(c)}.$
Fix an interpretation $\mathcal{M} = (U, \cdot^{\mathcal{M}})$ in which $\forall x\, P(x)$ holds. By the semantics of $\forall$, $P^{\mathcal{M}}(a)$ is true for every $a \in U$. Let $a := c^{\mathcal{M}}$, the element of $U$ denoted by the term $c$. Then $P^{\mathcal{M}}(c^{\mathcal{M}})$ is true, i.e. $\mathcal{M} \models P(c)$. $\square$
From $\forall x \in \mathbb{R}\,(x^2 \geq 0)$ apply UI with $c := -3$ to conclude $(-3)^2 \geq 0$, i.e. $9 \geq 0$.
No side condition on $c$: any term (variable, constant, or compound term like $f(t_1, \dots, t_n)$) is allowed, provided the substitution $P(x)[c/x]$ is capture-avoiding (Lesson 4, §1.7).

Rosen 8e §1.6 Table 2; Velleman 3e §3.3.

20 / 30

9.2 Universal Generalization (UG)

If $P(c)$ has been derived and $c$ is an arbitrary constant (see side condition), then $\;\dfrac{P(c)}{\forall x\, P(x)}.$
The justification is a meta-argument about derivations. Suppose we have a derivation of $P(c)$ from $\Gamma$ in which $c$ never appears in $\Gamma$ and is never named otherwise. The derivation uses no fact specific to $c$ — every step works for any element of $U$. Hence the same derivation, with $c$ replaced everywhere by any element $a \in U$, would yield $P(a)$. Therefore $P^{\mathcal{M}}(a)$ holds for every $a$, i.e. $\mathcal{M} \models \forall x\,P(x)$. $\square$
$c$ must be arbitrary: it must not occur free in any hypothesis still active in the proof, and it must not have been introduced by Existential Instantiation. In practice, every proof starting with "Let $c$ be an arbitrary element of $U$…" is preparing to invoke UG.
To prove $\forall x \in \mathbb{R}\,(x \geq 0 \to x^2 \geq 0)$: Let $c$ be an arbitrary real number. Suppose $c \geq 0$. Then $c \cdot c \geq 0 \cdot c = 0$. By UG, $\forall x \in \mathbb{R}\,(x \geq 0 \to x^2 \geq 0)$.

Mendelson 6e §2.4; Rosen 8e §1.6 Table 2.

21 / 30

9.3 Existential Instantiation (EI)

$\;\dfrac{\exists x\, P(x)}{P(c)}\;$ where $c$ is a fresh constant.
By the semantics of $\exists$, if $\mathcal{M} \models \exists x\, P(x)$ then there is some element $a \in U$ with $P^{\mathcal{M}}(a)$. Introduce a new constant symbol $c$ and extend the interpretation by $c^{\mathcal{M}} := a$. Then $\mathcal{M} \models P(c)$. The freshness of $c$ ensures the extension does not conflict with prior interpretations. $\square$
$c$ must be fresh: it must not have been used anywhere earlier in the proof, in the hypotheses, or in the goal. The constant names the witness whose existence has just been asserted; we are not allowed to assume anything else about it.
EI is the formal version of "Pick such an $x$ and call it $c$". Once you have $P(c)$, you reason about $c$ as if it were a specific (but unknown) element.

Rosen 8e §1.6 Table 2; Velleman 3e §3.3.

22 / 30

9.4 Existential Generalization (EG)

For any term $c$, $\;\dfrac{P(c)}{\exists x\, P(x)}.$
If $\mathcal{M} \models P(c)$, then $P^{\mathcal{M}}(c^{\mathcal{M}})$ holds. Setting $a := c^{\mathcal{M}}$, we have an element $a \in U$ with $P^{\mathcal{M}}(a)$, hence $\mathcal{M} \models \exists x\, P(x)$. $\square$

No side condition: any concrete witness justifies existence. EG is the symbolic encoding of "from $7^2 + 24^2 = 25^2$ we conclude $\exists x\,\exists y\,\exists z\,(x^2 + y^2 = z^2)$".

Summary of the four quantifier rules

$\dfrac{\forall x\, P(x)}{P(c)}$Univ. Instantiation
$\dfrac{P(c)\,[\,c\,\text{arbitrary}\,]}{\forall x\, P(x)}$Univ. Generalization
$\dfrac{\exists x\, P(x)}{P(c)\,[\,c\,\text{fresh}\,]}$Exist. Instantiation
$\dfrac{P(c)}{\exists x\, P(x)}$Exist. Generalization

Rosen 8e §1.6 Table 2.

23 / 30

10. Why the side conditions are necessary

UG without "arbitrary" fails

From $\;H(c)\;$ (where $c$ is a particular named constant in the hypotheses, e.g. "Socrates is human"), applying UG would yield $\;\forall x\,H(x)\;$ ("everybody is human") — clearly invalid. The side condition "$c$ does not occur in any active hypothesis" blocks this incorrect step.

EI without "fresh" fails

Suppose we have $\exists x\,P(x)$ and $\exists x\,Q(x)$. If we instantiate both with the same name $c$, we wrongly derive $P(c) \wedge Q(c)$, hence $\exists x\,(P(x) \wedge Q(x))$.
Counter-example on $U = \{1, 2\}$ with $P(x) := (x = 1)$ and $Q(x) := (x = 2)$. Then $\exists x\,P(x)$ and $\exists x\,Q(x)$ both hold (witnesses $1$ and $2$), but no element of $U$ satisfies both — there is no $x$ with $x = 1 \wedge x = 2$. The "shared $c$" derivation is invalid because the second EI must introduce a different fresh name. $\square$

This is the same issue as the failed equivalence $\exists x(P \wedge Q) \not\equiv \exists x P \wedge \exists x Q$ from Lesson 4 §8.2.

Mendelson 6e §2.4; Velleman 3e §3.3.

24 / 30

11. Mixed propositional / predicate example

Let $C(x), D(x), E(x)$ be unary predicates and $o$ a constant. Abbreviate

SymbolStands for
$p$$\exists x\, C(x)$
$q$$\exists x\, D(x)$
$r$$\exists x\, E(x)$

Hypotheses: $H_1: \neg p \to \neg q,\;\;\; H_2: D(o),\;\;\; H_3: \neg p \vee r$. Goal: derive $r$.

  1. 1.$D(o)$$H_2$
  2. 2.$\dfrac{D(o)}{\exists x\, D(x)} \equiv q$EG (1)
  3. 3.$\neg p \to \neg q$$H_1$
  4. 4.$\dfrac{\neg p \to \neg q,\;\; q}{p}$MT (3, 2) — contrapositive form
  5. 5.$\neg p \vee r$$H_3$
  6. 6.$\dfrac{\neg p \vee r,\;\; p}{r}$DS (5, 4)  $\square$
Python — entailment check from sympy import symbols, And, Or, Not, Implies from sympy.logic.inference import satisfiable p, q, r = symbols('p q r') premises = And(Implies(Not(p), Not(q)), # H1 q, # q follows from EG on D(o) Or(Not(p), r)) # H3 print(satisfiable(And(premises, Not(r))) is False) # True — r is entailed

Rosen 8e §1.6 Example 16.

25 / 30

12. Derived rules — constructive & destructive dilemma

Beyond the eight basic rules, several derived rules are convenient. Each is a shorthand for a short proof from the basic rules.

Constructive dilemma. $\;\{(p \to q) \wedge (r \to s),\;\; p \vee r\} \;\models\; q \vee s.$
Given the premises, suppose $v$ satisfies them. By DS / case analysis on $p \vee r$: if $v(p)$, then by MP on $p \to q$ we get $v(q)$, hence $v(q \vee s)$; if $v(r)$, then by MP on $r \to s$ we get $v(s)$, hence $v(q \vee s)$. $\square$
Destructive dilemma. $\;\{(p \to q) \wedge (r \to s),\;\; \neg q \vee \neg s\} \;\models\; \neg p \vee \neg r.$
By case analysis on $\neg q \vee \neg s$: if $v(\neg q)$, then by MT on $p \to q$ we get $v(\neg p)$, hence $v(\neg p \vee \neg r)$; if $v(\neg s)$, then by MT on $r \to s$ we get $v(\neg r)$, hence $v(\neg p \vee \neg r)$. $\square$
Absorption. $\;p \to q \;\models\; p \to (p \wedge q).$
Assume $p$. By MP on $p \to q$ derive $q$. By Conjunction derive $p \wedge q$. Discharge the assumption by $\to$-intro to obtain $p \to (p \wedge q)$. $\square$

Rosen 8e §1.6 Ex. 11–14; Mendelson 6e §1.6.

26 / 30

13.1 Soundness theorem (proved)

Soundness. For every finite set $\Gamma$ of propositional formulas and every formula $\psi$, $$\Gamma \vdash \psi \;\;\Longrightarrow\;\; \Gamma \models \psi.$$ In words: every formula derivable by the eight rules is also a logical consequence of $\Gamma$.
By induction on the length $n$ of the derivation $\varphi_1, \varphi_2, \ldots, \varphi_n = \psi$.
Base case $n = 1$. Then $\varphi_1$ is either a hypothesis (in which case trivially $\Gamma \models \varphi_1$) or an axiom (a tautology, true in every valuation). In both cases $\Gamma \models \varphi_1$.
Inductive step. Assume every formula appearing before $\varphi_n$ is entailed by $\Gamma$. If $\varphi_n$ is a hypothesis or axiom, the base argument applies. Otherwise $\varphi_n$ was obtained from some earlier $\varphi_{i_1}, \ldots, \varphi_{i_k}$ by a rule $\mathcal{R}$. By the inductive hypothesis, $\Gamma \models \varphi_{i_j}$ for each $j$, so any valuation satisfying $\Gamma$ also satisfies all premises of $\mathcal{R}$. By the validity of $\mathcal{R}$ (proved on slides 9–15), the conclusion $\varphi_n$ is also satisfied. Hence $\Gamma \models \varphi_n$. $\square$
Soundness reduces the correctness of the whole proof system to the correctness of each individual rule — exactly what we verified, one rule at a time, in slides 9–15.

Mendelson 6e Theorem 1.13; Cori & Lascar vol. 1.

27 / 30

13.2 Completeness theorem (statement & sketch)

Completeness (Post 1921 / Gödel 1929 for first-order logic). For every finite set $\Gamma$ and every formula $\psi$, $$\Gamma \models \psi \;\;\Longleftrightarrow\;\; \Gamma \vdash \psi.$$ Hence semantic entailment and syntactic derivability coincide.

Sketch of proof (propositional case). The non-trivial direction is $\models \Rightarrow \vdash$. The standard Henkin-style argument runs as follows.

  1. Assume $\Gamma \not\vdash \psi$. We construct a valuation satisfying $\Gamma$ but falsifying $\psi$, contradicting $\Gamma \models \psi$.
  2. By Zorn / Lindenbaum, extend $\Gamma \cup \{\neg \psi\}$ to a maximal consistent set $\Gamma^*$ (one that proves no contradiction yet adding any formula to it would).
  3. Define $v(p) := \mathtt T$ iff $p \in \Gamma^*$. By maximality and consistency, $v$ extends to all formulas and $v(\chi) = \mathtt T \Leftrightarrow \chi \in \Gamma^*$.
  4. Then $v$ satisfies $\Gamma$ and falsifies $\psi$ — contradiction. Hence $\Gamma \vdash \psi$.

For first-order logic, Gödel's 1929 completeness theorem extends this construction; the Henkin proof additionally produces witnesses for existential statements via fresh constants. Note: this is completeness, not Gödel's later incompleteness theorem, which concerns Peano arithmetic.

Mendelson 6e §1.6 / §2.5; Cori & Lascar vol. 1 ch. 4.

28 / 30

14. Wolfram → Python quick reference

TaskWolframPython (SymPy / Z3)
Check a tautologyTautologyQ[expr]not satisfiable(Not(expr))
Check entailment $\Gamma \models \psi$Resolve[Implies[And@@G, psi]]satisfiable(And(G, Not(psi))) is False
Modus PonensAnd(Implies(p,q), p) implies q
Find a modelFindInstancesatisfiable(expr) returns a dict
First-order entailmentResolve[ForAll[…]]z3.Solver() / z3.prove()
Python — generic entailment helper from sympy import And, Not from sympy.logic.inference import satisfiable def entails(premises, goal): """Return True iff premises ⊨ goal.""" return satisfiable(And(premises, Not(goal))) is False
Python — verify all eight propositional rules from sympy import symbols, And, Or, Not, Implies p, q, r = symbols('p q r') checks = { 'Modus Ponens' : (And(p, Implies(p, q)), q), 'Modus Tollens' : (And(Not(q), Implies(p, q)), Not(p)), 'Hyp. Syllogism' : (And(Implies(p, q), Implies(q, r)), Implies(p, r)), 'Disj. Syllogism' : (And(Or(p, q), Not(p)), q), 'Addition' : (p, Or(p, q)), 'Simplification' : (And(p, q), p), 'Conjunction' : (And(p, q), And(p, q)), 'Resolution' : (And(Or(p, q), Or(Not(p), r)), Or(q, r)), } for name, (G, psi) in checks.items(): print(f'{name:<18} {entails(G, psi)}') # all True
29 / 30

Summary & bibliography

What we proved

Bibliography

Notes By Pr. El Hadiq Zouhair

30 / 30