- Last time:
- Models vs theories. Axioms and proofs.
- Propositions.
- Logical connectives: ¬, ∧, ∨, ⇒, ⇔.
- Modus ponens: P, P ⇒ Q ⊢ Q.

- This time:
- Tautologies.
- Proving tautologies using truth tables.

- More on entailment (⊢)
- If P ⇒ Q is a tautology, then P ⊢ Q
- Proof: We can always add tautologies to our list of axioms, then P, P ⇒ Q ⊢ Q by modus ponens.
- We can get new inference rules by proving tautologies of the form P ⇒ Q.
- Example: P ⊢ P ∨ Q (addition rule) follows from P ⇒ (P ∨ Q).
- Example: P ∧ Q ⊢ P (simplification rule) follows from P ∧ Q ⇒ P.

- Converse: If P, R ⊢ Q, then R ⊢ P ⇒ Q. (Deduction Theorem)
- We can prove P ⇒ Q by assuming P and proving Q.

- Note distinction between implication (⇒) and entailment (⊢)
- Implication is inside the theory: P ⇒ Q might be true, might be false.
- Entailment is outside: P ⊢ Q depends only on structure of P and Q.

- If P ⇒ Q is a tautology, then P ⊢ Q
- More on logical equivalence (≡)
- P ≡ Q if P and Q are true under exactly the same conditions.
- To prove P ≡ Q:
- Use truth tables.
- Prove P ⇔ Q is a tautology.

- Payoff: if P ≡ Q, then we can substitute either for the other inside compound propositions.
- Example: ¬¬P ≡ P. (Double-negation elimination: prove using truth table.)
- Example: ¬(P∨Q) ≡ ¬P ∧ ¬Q. (De Morgan's Law: prove using truth table.)
- Example: ¬(P∧Q) ≡ ¬P ∨ ¬Q. Proof: ¬(P∧Q) ≡ ¬(¬¬P ∧ ¬¬Q) [double-negation] ≡ ¬¬(¬P ∨ ¬Q) [De Morgan] ≡ ¬P ∨ ¬Q [double-negation]
- Example: P ⇒ Q ≡ ¬Q ⇒ ¬P (contraposition). Proof: P ⇒ Q ≡ ¬P ∨ Q ≡ Q ∨ ¬P ≡ ¬¬Q ∨ ¬P ≡ ¬Q ⇒ ¬P.

- Predicate logic [if we get to it]
- Add constants: Socrates, 12/37, the 1962 Red Sox.
- Add predicates: e.g. P(x) for "x is mortal"
- Add quantifiers
- Universal quantifier ∀x P(x) ("for all x, P(x)") means P(x) is true for any x in the universe: essentially a very big AND.
- Existential quantifier: ∃x P(x) ("there exists x such that P(x)") means P(x) is true for at least one x in the universe: essentially a very big OR.
How to interpret nested quantifiers, e.g. ∀x∃y y > x.

- Add inference rules
- Universal/existential specialization/generalization

- Optional: add function names and equality

- Tautologies.