Rules of Inference

Discrete Mathematics — Lesson 5

Notes By Pr. El Hadiq Zouhair

1 / 11

Overview

Most of the time, the full explanation is not needed.
Inference is the process of deriving logical conclusions from known premises.
Aristotle classically divided it in two: deduction and induction.

2 / 11

Motivation

Assume the following statements as true:

If you have cherries, you can eat. $\mathit{have} \Rightarrow \mathit{eat}$
You have cherries. $\mathit{have}$

Intuitively, by inference, this implies you can eat. But how do you get there?

Python — imports (run once) from sympy import symbols, And, Implies, simplify_logic from sympy.logic.boolalg import truth_table have, eat = symbols('have eat')

Python expr = And(Implies(have, eat), have) print(simplify_logic(expr)) # eat & have for vals, result in truth_table(expr, [have, eat]): print(list(vals), '->', result)

have	eat	eat ∧ have
True	True	True
True	False	False
False	True	False
False	False	False

3 / 11

Limits of Truth Tables

Simplification through equivalences is often insufficient to obtain conclusive results:

Python — imports (run once) from sympy import symbols, Or, And, simplify_logic from sympy.logic.boolalg import truth_table from itertools import combinations

Python a, b, c, d, e = symbols('a b c d e') # BooleanCountingFunction[2, 5]: at least 2 of 5 are True expr = Or(*[And(x, y) for x, y in combinations([a,b,c,d,e], 2)]) simplified = simplify_logic(expr) print(simplified) # still complex # Truth table: 2^5 = 32 rows — too large to inspect by hand for vals, result in truth_table(simplified, [a, b, c, d, e]): print(list(vals), '->', result)

With 5 variables a truth table has $2^5 = 32$ rows. Rules of inference provide a structured shortcut.

4 / 11

Rules of Inference

Each rule is written as a natural-deduction fraction: premises above the bar, conclusion below. Unlike equivalence, the conclusion is weaker than the premises.

$\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}$ Hypothetical Syllogism

$\dfrac{p \vee q,\;\; \neg p}{q}$ Disjunctive 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

Read the bar as "therefore": from the premises listed above the line, you may infer the conclusion below.

Python — verify all rules from sympy import symbols, And, Or, Not, Implies from sympy.logic.inference import satisfiable p, q, r = symbols('p q r') # A rule is valid iff premises & ~conclusion is UNSAT checks = { 'Modus Ponens': And(p, Implies(p,q), Not(q)), 'Modus Tollens': And(Not(q), Implies(p,q), p), 'Hyp. Syllogism': And(Implies(p,q), Implies(q,r), Not(Implies(p,r))), 'Disj. Syllogism': And(Or(p,q), Not(p), Not(q)), 'Resolution': And(Or(p,q), Or(Not(p),r), Not(Or(q,r))), } for name, f in checks.items(): print(name, ':', not satisfiable(f)) # all True

5 / 11

Example 1

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

Label	Formula
$H_1$	$p \vee q$
$H_2$	$p \to r$

Goal: derive $\;\boxed{\,r \vee q\,}\;$ from $H_1, H_2$.

The conditional $p \to r$ is equivalent to $\neg p \vee r$. Apply Resolution:

$\dfrac{p \vee q,\;\; \neg p \vee r}{q \vee r}$ Resolution

Hence $\;\;$$r \vee q$$\;\;$ follows. $\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)) # H1 ∧ H2 goal = Or(r, q) # premises ⊨ goal iff premises ∧ ¬goal is unsatisfiable print(satisfiable(And(premises, Not(goal))) is False) # True

6 / 11

Example 2

Let $p, q, r, s, t, u$ be propositional variables. Assume the following well-formed formulae as hypotheses:

Label	Formula
$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$

Show that, under these hypotheses, the well-formed formula $\;\;\boxed{\;p \to u\;}\;$ is a logical consequence:

$$\{\,p \to q,\;\; q \to r,\;\; (r \wedge s) \to t,\;\; t \to u,\;\; s\,\}\;\vdash\; p \to u$$ 7 / 11

Example 2 (continued)

Each inference step is written as a fraction $\dfrac{\text{premises}}{\text{conclusion}}$:

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

Python — entailment check with SymPy from sympy import symbols, And, Implies, Not from sympy.logic.inference import satisfiable p, q, r, s, t, u = symbols('p q r s t u') premises = And( Implies(p, q), # H1 Implies(q, r), # H2 Implies(And(r, s), t), # H3 Implies(t, u), # H4 s, # H5 ) goal = Implies(p, u) # (premises ∧ ¬goal) must be unsatisfiable iff premises ⊨ goal print(satisfiable(And(premises, Not(goal))) is False) # True → entailed

8 / 11

Rules for Quantified Statements

Inference also has four rules for quantifiers. Let $P$ be a unary predicate and $c$ a constant.

$\dfrac{\forall x\, P(x)}{P(c)}$ Universal Instantiation

$\dfrac{P(c)\;\;[\,c\text{ arbitrary}\,]}{\forall x\, P(x)}$ Universal Generalization

$\dfrac{\exists x\, P(x)}{P(c)\;\;[\,c\text{ fresh}\,]}$ Existential Instantiation

$\dfrac{P(c)}{\exists x\, P(x)}$ Existential Generalization

Side conditions: in UG, $c$ must not occur free in any open assumption; in EI, $c$ must be a fresh name not used elsewhere.

Worked example

Let $H, L$ be unary predicates and $o$ a constant. Hypotheses:

Label	Formula
$H_1$	$\forall x\,\bigl(H(x) \to L(x)\bigr)$
$H_2$	$H(o)$

Derive $\;\boxed{\,L(o)\,}\;$:

1.$\forall x\,\bigl(H(x) \to L(x)\bigr)$$H_1$
2.$\dfrac{\forall x\,(H(x) \to L(x))}{H(o) \to L(o)}$Universal Instantiation
3.$H(o)$$H_2$
4.$\dfrac{H(o),\;\; H(o) \to L(o)}{L(o)}$Modus Ponens $\square$

Python — Z3 from z3 import DeclareSort, Function, BoolSort, Const, ForAll, Implies, Solver, Not Person = DeclareSort('Person') o = Const('o', Person) x = Const('x', Person) H = Function('H', Person, BoolSort()) L = Function('L', Person, BoolSort()) s = Solver() s.add(ForAll([x], Implies(H(x), L(x)))) # H1 : ∀x. H(x) → L(x) s.add(H(o)) # H2 : H(o) s.add(Not(L(o))) # assume ¬L(o) — should contradict print(s.check()) # unsat → L(o) follows

9 / 11

Example 3 — Existential reasoning

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

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

Hypotheses:

Label	Formula
$H_1$	$\neg p \to \neg q$
$H_2$	$D(o)$
$H_3$	$\neg p \vee r$

Goal: derive $\;\boxed{\,r\,}\;$ (i.e. $\exists x\, E(x)$).

1.$D(o)$$H_2$
2.$\dfrac{D(o)}{\exists x\, D(x)} \;\equiv\; q$Existential Generalization
3.$\dfrac{\neg p \to \neg q,\;\; q}{p}$Modus Tollens (H$_1$, 2)
4.$\dfrac{\neg p \vee r,\;\; p}{r}$Disjunctive Syllogism (H$_3$, 3)
5.$r$, i.e. $\exists x\, E(x)$conclusion $\square$

Python — entailment check from sympy import symbols, And, Or, Not, Implies from sympy.logic.inference import satisfiable # Propositional abstractions of the existentials p, q, r = symbols('p q r') premises = And( Implies(Not(p), Not(q)), # H1 : ¬p → ¬q q, # H2 → q (after Existential Generalization on D(o)) Or(Not(p), r), # H3 : ¬p ∨ r ) goal = r # premises ⊨ goal iff premises ∧ ¬goal is unsatisfiable print(satisfiable(And(premises, Not(goal))) is False) # True

10 / 11

Summary

The main rules of inference are modus ponens, modus tollens, hypothetical syllogism, disjunctive syllogism, addition, simplification, conjunction and resolution.
Quantified rules of inference are universal instantiation, universal generalization, existential instantiation and existential generalization.
These rules make it easy to extract useful conclusions out of compound propositions.
You should now have a good understanding of logic.
The next lesson goes beyond true/false values — onward with sets.

11 / 11