Inference rules: modus ponens, modus tollens, instantiation; sound & complete

Deriving new truths mechanically

An inference rule is a syntactic pattern that produces a new sentence from existing ones. A proof procedure is an inference rule *plus* an algorithm that decides when and where to apply it. The rules below are the practical toolkit for rule-based AI.

- Modus ponens (MP) — from $P \to Q$ and $P$, infer $Q$. ("The way that affirms by affirming.") This is the basis of forward chaining (Module 5, exam Q8). - Modus tollens (MT) — from $P \to Q$ and $\neg Q$, infer $\neg P$. (Affirms by denying — work backward from a false consequent.) - And-Elimination — from $P \wedge Q$, infer $P$ (or infer $Q$). - And-Introduction — from $P$ and $Q$ separately, infer $P \wedge Q$. - Universal Instantiation (UI) — from $\forall X\,p(X)$, infer $p(a)$ for any constant $a$ in the domain.

Watch the fallacy: from $P \to Q$ and $Q$ you may not infer $P$ — that is *affirming the consequent* (abduction), which is *unsound*. Wet ground does not prove it rained.

Sound vs complete

Two correctness properties measure an inference system:

- Sound — every sentence the rule produces from a set $S$ *logically follows from* $S$. A sound rule never derives a falsehood from truths. - Complete — the rule can produce *every* sentence that logically follows from $S$. A complete rule misses nothing.

The two are independent. Modus ponens alone is sound but not complete (it cannot derive everything that follows — e.g. it does not do proof by cases). Resolution (Module 9) is both sound and complete. Heuristic and probabilistic reasoners (Modules 4, 7) deliberately *relax* soundness to gain speed under uncertainty.

Worked example: the Socrates syllogism

Knowledge base: the rule $\forall X\,(man(X) \to mortal(X))$ and the fact $man(socrates)$. Derive $mortal(socrates)$ in two steps:

1. Universal Instantiation — substitute $socrates$ for $X$ in the rule, giving the ground implication $man(socrates) \to mortal(socrates)$.
2. Modus Ponens — we now have both this implication and the fact $man(socrates)$ (its antecedent), so MP yields $mortal(socrates)$.

This two-step pattern — *instantiate a general rule to a ground case, then fire MP* — is the heartbeat of predicate-calculus inference. (Unification, Lesson 6, automates step 1 by finding the substitution {socrates/X} mechanically.) The Python engine below applies MP to a fixpoint and derives mortal(socrates).