Chapter 3 — Key Takeaways

Rules of Inference: How to Reason Validly. A one-page reference. Reread before an exam.

Core definitions

Term One-line definition
Argument A finite list of premises followed by one conclusion (written with $\therefore$).
Premise A statement assumed/given as input to the argument.
Conclusion The final statement the argument claims the premises support.
Validity No truth assignment makes all premises true and the conclusion false. A property of form.
Soundness Valid and all premises actually true ⟹ conclusion guaranteed true.
Fallacy An invalid form commonly mistaken for a valid one.
Derivation ($\Gamma \vdash C$) Numbered sequence ending in $C$; each line is a premise or follows from earlier lines by a named rule.

Validity test (the definition, operationalized): the argument is valid $\iff$ $\big(\text{premise}_1 \land \dots \land \text{premise}_n\big) \rightarrow \text{conclusion}$ is a tautology (all-T truth table — Ch. 1).

Valid vs. sound vs. invalid (decision table)

Premises true? Valid form? Conclusion guaranteed?
Sound Yes Yes Yes
Valid but unsound No Yes No
Invalid (fallacy) Either No No

Ask two questions: Is the reasoning airtight? (validity) and Are the inputs true? (soundness).

The propositional inference rules (memorize)

Rule Premises $\Rightarrow$ Conclusion Gloss
Modus ponens $p\rightarrow q,\ p \ \Rightarrow\ q$ Affirm antecedent.
Modus tollens $p\rightarrow q,\ \neg q \ \Rightarrow\ \neg p$ Deny consequent.
Hypothetical syllogism $p\rightarrow q,\ q\rightarrow r \ \Rightarrow\ p\rightarrow r$ Chain implications.
Disjunctive syllogism $p\lor q,\ \neg p \ \Rightarrow\ q$ Eliminate an option.
Addition $p \ \Rightarrow\ p\lor q$ Weaken to a disjunction.
Simplification $p\land q \ \Rightarrow\ p$ Drop a conjunct.
Conjunction $p,\ q \ \Rightarrow\ p\land q$ Combine two truths.
Resolution $p\lor q,\ \neg p\lor r \ \Rightarrow\ q\lor r$ Cancel $p/\neg p$ (engine of Prolog & SAT solvers).

The two fallacies (the evil twins)

Fallacy Form (INVALID) Counterexample row CS instance
Affirming the consequent $p\rightarrow q,\ q \ \Rightarrow\ p$ $p=$F, $q=$T "Tests passed ⟹ code correct."
Denying the antecedent $p\rightarrow q,\ \neg p \ \Rightarrow\ \neg q$ $p=$F, $q=$T "Not admin ⟹ can't read file."

The four moves on $p \rightarrow q$:

Extra premise Conclude Valid? Name
$p$ $q$ ✅ modus ponens
$\neg q$ $\neg p$ ✅ modus tollens
$q$ $p$ ❌ affirming the consequent
$\neg p$ $\neg q$ ❌ denying the antecedent

Litmus test for a fallacy: Could the consequent be true some other way? If yes, the backward move is invalid.

The four quantifier rules

Rule From $\Rightarrow$ To Side condition (do not skip)
Universal instantiation (UI) $\forall x\,P(x) \Rightarrow P(c)$ $c$ = any element of the domain.
Universal generalization (UG) $P(c) \Rightarrow \forall x\,P(x)$ $c$ must be truly arbitrary (no special assumptions).
Existential instantiation (EI) $\exists x\,P(x) \Rightarrow P(c)$ $c$ must be a fresh name (never reused).
Existential generalization (EG) $P(c) \Rightarrow \exists x\,P(x)$ none.

Two-phase rhythm of quantified proofs: instantiate (UI/EI) → do propositional logic → generalize (UG/EG) if the goal is quantified.

Common pitfalls

Pitfall Fix
"Conclusion is true ⟹ argument valid." Validity is about form/connection, not the outcome.
Confusing a fallacy with a false premise. Fallacy = bad form (unfixable by checking facts); unsound = bad input.
Generalizing (UG) from a special element (e.g., $c=0$). UG needs $c$ unconstrained throughout the subproof.
Instantiating two $\exists$ with the same name. Each EI gets its own fresh name.
Treating "tests passed" as proof of correctness. That's affirming the consequent; only a proof closes the gap.
Citing a later line in a derivation. Justifications point backward only (no circularity).

Building a derivation (procedure)

  1. Backward: look at the goal; pick a rule that could produce it; its inputs become sub-goals.
  2. Repeat until every sub-goal is a premise or already derivable.
  3. Forward: write lines premises-first; each cites a named rule + earlier line numbers.
  4. A finished derivation is machine-checkable line by line (how Coq/Lean/Isabelle work).

Finding a proof is hard; checking it is easy. (This asymmetry returns as P vs. NP, Ch. 37.)

Where it lives in CS

System Inference idea in use
Type inference (ML, Rust, Haskell, TS) Typing rules = inference rules; the bar = $\therefore$; a type is a derivation.
Prolog / logic programming Clauses = implications; the engine derives via resolution + UI + modus ponens.
SMT / model checkers "Verified" = no counterexample assignment exists (the validity question, scaled up).

Toolkit increment (logic.py, Chapters 1–3)

def is_valid(premises, conclusion, names):
    """True iff no assignment makes all premises True and conclusion False."""
    from itertools import product
    for vals in product([False, True], repeat=len(names)):
        if all(p(*vals) for p in premises) and not conclusion(*vals):
            return False
    return True
  • Composes with truth_table, is_tautology, equivalent (same boolean-function representation).
  • is_valid(prems, c, names) agrees with is_tautology applied to prems... -> conclusion.
  • Use it to test validity on finitely many variables; use the rules to prove it when the table is too big.