A truth table tells you whether a formula is a tautology, but with many variables it becomes unmanageable. There is another way to reason: start from known premises and derive new conclusions through simple steps, each of which is guaranteed to be correct. These steps are called rules of inference, and they are the grammar of every proof, from mathematics to automated verification systems.
What makes an inference valid
An inference is valid when it is impossible for the premises to be all true and the conclusion false. Formally: if the premises are P₁, …, Pₙ and the conclusion is C, the inference is valid if (P₁ ∧ … ∧ Pₙ) → C is a tautology.
Validity and truth are different things. A valid argument with a false premise can lead to a false conclusion; an invalid argument can reach a true conclusion by chance. Validity concerns form alone.
The main rules
| Rule | Premises | Conclusion |
|---|---|---|
| Modus ponens | p → q, p | q |
| Modus tollens | p → q, ¬q | ¬p |
| Hypothetical syllogism | p → q, q → r | p → r |
| Disjunctive syllogism | p ∨ q, ¬p | q |
| Addition | p | p ∨ q |
| Simplification | p ∧ q | p |
| Conjunction | p, q | p ∧ q |
| Resolution | p ∨ q, ¬p ∨ r | q ∨ r |
Let's look at the meaning of a few.
Modus ponens
This is the most natural rule: if "if p then q" holds and p holds, then q holds. "If the certificate has expired, the browser shows a warning. The certificate has expired. Therefore the browser shows a warning."
Modus tollens
You reason backwards from the negated conclusion: "if the disk is full, the log reports a write error. The log reports no write errors. Therefore the disk is not full." This is the rule used to rule out hypotheses during a diagnosis.
Disjunctive syllogism
If one of two alternatives must hold and one is excluded, the other remains. "The fault is in the client or in the server. The client works with another server. Therefore the fault is in the server." Careful: it only works if the initial disjunction really is complete.
Resolution
This is the least intuitive rule, but the most powerful for machines. If p appears in one clause and ¬p in another, the two can be merged by removing the pair. From "p ∨ q" and "¬p ∨ r" we derive "q ∨ r": if p is true, r must be true by the second clause; if p is false, q must be true by the first. Either way q ∨ r holds.
An example of formal deduction
Premises:
- If the nightly backup succeeded, then the status file exists. (b → f)
- If the status file exists, then monitoring is green. (f → m)
- Monitoring is not green. (¬m)
- The nightly backup succeeded or the alarm went off. (b ∨ a)
We want to prove that the alarm went off (a).
| Step | Formula | Justification |
|---|---|---|
| 5 | b → m | hypothetical syllogism from 1 and 2 |
| 6 | ¬b | modus tollens from 5 and 3 |
| 7 | a | disjunctive syllogism from 4 and 6 |
Three steps, each applying a single rule. This is the style of a formal proof: no jumps, every line justified by rules and earlier lines.
Proof by refutation with resolution
Automated provers often take a different approach: they add the negation of the goal to the premises and try to derive a contradiction, that is, the empty clause. If they succeed, the goal follows from the premises.
Let's redo the example this way. Turn everything into clauses: ¬b ∨ f, ¬f ∨ m, ¬m, b ∨ a, and the negated goal ¬a.
- From b ∨ a and ¬a: b.
- From ¬b ∨ f and b: f.
- From ¬f ∨ m and f: m.
- From m and ¬m: the empty clause.
Contradiction reached, so a is proved. The advantage is that the machine needs only one rule, applied repeatedly. This is the idea behind the Prolog language and many verification tools.
Errors to recognise
Two patterns look like rules but are not:
- Affirming the consequent: from p → q and q, concluding p.
- Denying the antecedent: from p → q and ¬p, concluding ¬q.
A quick check: if you have doubts about a pattern, look for an assignment that makes the premises true and the conclusion false. If you find one, the pattern is invalid. For affirming the consequent, p false and q true is enough.
In short
- An inference is valid if true premises cannot lead to a false conclusion; only the form matters.
- Modus ponens, modus tollens and the syllogisms cover most everyday reasoning.
- A formal proof is a sequence of lines, each justified by a rule.
- Resolution combined with refutation lets machines prove things with a single rule.
- To expose an invalid pattern, finding one counterexample is enough.
