• InferenceRules

1. Proofs

A proof is a way to derive statements of the form P ⇒ Q from other statements. It starts with axioms (statements that are assumed in the current context always to be true), theorems or lemmas (statements that were proved already), and premises (P), and uses inference rules to derive Q. The axioms, theorems, and premises are in a sense the starting position of a game whose rules are given by the inference rules. The goal of the game is to apply the inference rules until Q pops out. We refer to anything that isn't proved in the proof itself (ie., an axiom, theorem, lemma, or premise) as a hypothesis; the result Q is the conclusion.

2. Inference Rules

The main source of inference rules is tautologies of the form P ⇒ Q; given such a tautology, there is a corresponding inference rule that allows us to assert Q once we have P (either because it's an axiom/theorem/premise or because we proved it already while doing the proof). The most important inference rule is modus ponens, based on the tautology (p ∧ (p ⇒ q)) ⇒ q; this lets us, for example, write the following famous argument:

1. If it doesn't fit, you must acquit. [Axiom]
2. It doesn't fit. [Premise]
3. You must acquit. [Modus ponens applied to 1+2]

There are many named inference rules in classical propositional logic. We'll list some of them below. You don't need to remember the names of anything except modus ponens, and most of the rules are pretty much straightforward applications of modus ponens plus some convenient tautology that can be proved by truth tables or stock logical equivalences. (For example, the "addition" rule below is just the result of applying modus ponens to p and the tautology p ⇒ (p ∨ q).)

Inference rules are often written by putting the premises above a horizontal line and the conclusion below. In text, the horizontal line is often replaced by an entailment symbol or "turnstile", which looks like this: ⊢. Premises are listed on the left-hand side separated by commas, and the conclusion is placed on the right. We can then write

Addition

p ⊢ p ∨ q.

Simplification

p ∧ q ⊢ p.

Conjunction

p, q ⊢ p ∧ q.

Modus ponens

p, p ⇒ q ⊢ q.

Modus tollens

¬q, p ⇒ q ⊢ ¬p.

Hypothetical syllogism

p ⇒ q, q ⇒ r ⊢ p ⇒ r.

Disjunctive syllogism

p ∨ q, ¬p ⊢ q.

Resolution

p ∨ q, ¬p ∨ r ⊢ q ∨ r.

Of these rules, Addition, Simplification, and Conjunction are mostly used to pack and unpack pieces of arguments. Modus ponens (and its reversed cousin modus tollens) let us apply implications. You only need to remember modus ponens if you can remember the contraposition rule (p ⇒ q) ≡ (¬q ⇒ ¬p). Hypothetical syllogism just says that implication is transitive; it lets you paste together implications if the conclusion of one matches the premise of the other. Disjunctive syllogism is again a disguised version of modus ponens (via the logical equivalence (p ∨ q) ≡ (¬p ⇒ q)); you don't need to remember it if you can remember this equivalence. Resolution is almost never used by humans but is very popular with computer theorem provers.

An argument is valid if the conclusion is true whenever the hypotheses are true. Any proof constructed using the inference rules is valid. It does not necessarily follow that the conclusion is true; it could be that one or more of the hypotheses is false:

1. If you give a mouse a cookie, he's going to ask for a glass of milk. [Axiom]
2. If he asks for a glass of milk, he will want a straw. [Axiom]
3. You gave a mouse a cookie. [Premise]
4. He asks for a glass of milk. [Modus ponens applied to 1 and 3.]
5. He will want a straw. [Modus ponens applied to 2 and 4.]

Will the mouse want a straw? No: Mice can't ask for glasses of milk, so axiom 1 is false.

3. The Deduction Theorem

Often we want to package the result of a proof as a Theorem (a proven statement that is an end in itself) or Lemma (a proven statement that is intended mostly to be used in other proofs). Typically a proof shows that if certain premises P₁, P₂, ... hold, then some conclusion Q holds (with various axioms or previously-established theorems assumed to be true from context). To use this result later, it is useful to be able to package it as an implication P₁ ∨ P₂ ∨ ... ⇒ Q. That we can do this is the Deduction Theorem:

Deduction Theorem

If there is a proof of Q from premises P₁, P₂, ... P_n, then the implication P₁ ∧ P₂ ∧ ... ∧ P_n ⇒ Q is true.

4. Inference rules for quantified statements

Universal generalization

If P ⊢ Q(x) and x does not appear in P, then P ⊢ ∀x Q(x).

Universal specialization

∀x Q(x) ⊢ Q(c).

Existential generalization

∃x Q(x) ⊢ Q(c) for some particular c. (The real rule is more complicated and says ((∀x (Q(x) ⇒ P)) ∧ ∃y Q(y)) ⇒ P; but the intent in both cases is that once you have proven that at least one c satisfying Q exists, you can give it a name and treat it as an object you actually have in your hands.)

Existential specialization

Q(c) ⊢ ∃x Q(x).

CategoryMathNotes