More logic: PredicateLogic, InferenceRules and ProofTechniques. Readings: Sections 1.4-1.6, 3.6.

Proving things in propositional logic

tautology is a proposition that is always true, regardless of the truth-value of its components, e.g. P /\ Q => P. Can check tautologies using truth tables.
P and Q are logically equivalent iff P <=> Q is a tautology.
When proving things, we combine propositions known to be true---tautologies and axioms---using InferenceRules. Inference rules are designed to preserve truth and thus give us new true statements.
- Most important inference rule is modus ponens: P, P => Q |- Q.
- Also important: conjunction rule: P, Q |- P /\ Q.
- There are many other named inference rules but they can mostly be derived from conjunction, modus ponens, and throwing in the appropriate tautologies.
- Deduction Theorem: to prove P => Q, assume P and prove Q. The Deduction Theorem says that from any such proof it is possible to mechanically extract a proof of P => Q without assuming that P is true.

Proving things in predicate logic

PropositionalLogic adds variables and quantifiers to PredicateLogic. So now we can say things like ∀x Human(x) => Mortal(x).

∀x P(x) is like P(x₁) /\ P(x₂) /\ ... where x_i span universe of all objects under consideration.
To specify universe, can use ∀x∈U P(x); this is equivalent to ∀x (x∈U => P(x))
∃x P(x) is like P(x₁) \/ P(x₂) \/ ...
De Morgan's law applies: ¬∀x P(x) ≡ ∃x ¬P(x) and ¬∃x P(x) ≡ ∀x ¬P(x).
All inference rules for PropositionalLogic still apply.
New inference rules of specialization and generalization allow moving back and forth from quantified statements to statements about specific things (see InferenceRules).

Choosing a proof technique

Key idea is that structure of consequent hints at possible structure for the proof, e.g. to prove P /\ Q prove P and Q separately (and then use conjunction to smack them together---this step is usually implicit); to prove P => Q assume P and prove Q (then Deduction Theorem does the rest---again this is usually not stated explicitly); to prove ∀x P(x) prove that P(x) holds for some arbitrary x. See ProofTechniques for the big table.

Often there is more than one technique you can try. If the first one doesn't work, try another one. Repeat until something works. If it doesn't look like anything is working, look for a counterexample or disproof.