6.2 KiB
6.2 KiB
Slide Notes:
Slide 0: Learning Objectives
- Identify genuine variables and variables standing for unknowns.
- Describe the role of inference rules for eliminating and introducing quantifiers.
- Justify constraints on handling variables when eliminating and introducing quantifiers.
- Conduct proofs in predicate logic.
- Prove the validity of an argument presented in English.
Slide 1: Contents
- Recap on inference rules
- Deductive proof in predicate logic
- Genuine variables versus unknown variables
- Extra inference rules for predicate logic
- Constraints on variables
- Summary, reading and references
Slide 2: Recap on Inference Rules
| Connective | Introduction Rule | Elimination Rule |
|---|---|---|
| ∧ (and) | ∧ Intro:$p, q \vdash p \land q$ | ∧ Elim:$p \land q, p \vdash q$ |
| ∨ (or) | ∨ Intro:$p \vdash p \lor q$,$q \vdash p \lor q$ | ∨ Elim:$p \vdash \varnothing$,$p \lor q \vdash \varnothing$x |
| ¬ (not) | N/A | ¬ Elim:$\neg p, q \vdash p$ |
| ⇒ (implies) | ⇒ Intro:$p, p \Rightarrow q \vdash q$ | ⇒ Elim (Modus Ponens):$p \Rightarrow q, p \vdash q$ |
| ⇔ (if and only if) | ⇔ Intro:$p \Rightarrow q, q \Rightarrow p \vdash p \leftrightarrow q$ | ⇔ Elim:$p \leftrightarrow q, p, q \vdash \varnothing$ |
Slide 3: Deductive Proof in Predicate Logic
- Reduce formulae to propositional form by removing quantifiers.
- Manipulate formulae using inference rules and logical laws of propositional logic.
- Reintroduce quantifiers at the end, depending on the goal.
Slide 4: Genuine Variables vs. Unknown Variables
- Genuine variable:
- A free variable whose universal quantification yields a true formula.
- Unknown variable:
- A free variable whose existential quantification yields a true formula.
Slide 5: Exercise
Example:
-\frac{9}{z} = 3
-\text{even}(n) \lor \text{odd}(n)
| Variable | Status | Justification |
|---|---|---|
z |
Unknown variable | \exists z \cdot \frac{9}{z} = 3 |
n |
Genuine variable | \forall n \cdot (\text{even}(n) \lor \text{odd}(n)) |
Slide 6: Extra Inference Rules for Predicate Logic
| Quantifier | Introduction Rule | Elimination Rule |
|---|---|---|
| $\forall$(for all) | \forall \text{Intro}: \varphi(x), x \neq y \vdash \varphi(x) |
\forall \text{Elim}: \forall x \cdot \varphi(x), \varphi(x) \vdash \varnothing |
| $\exists$(there exists) | \exists \text{Intro}: \varphi(x), x \neq y \vdash \exists x \cdot \varphi(x) |
\exists \text{Elim}: \exists x \cdot \varphi(x), \varphi(x) \vdash \varnothing |
Slide 7: Freeing Variables from$\forall$
- Example:
-
\forall x \cdot \text{lecturer}(x), \text{lecturer}(bryant)-\forall x \cdot \text{lecturer}(x), \text{lecturer}(y)-$y$is a genuine variable.
Slide 8: Freeing Variables from$\exists$
- Example:
-
\exists x \cdot \text{student}(x), \text{student}(y)-$y$is an unknown variable.
Slide 9: Introduction of$\forall$
- Constraint:
- Do not introduce$\forall$on the basis of an individual (a constant).
Slide 10: Constraint 1
- When eliminating$\exists$, do not instantiate its variable with a constant.
Slide 11: Constraint 2
- When eliminating$\exists$, do not instantiate its variable with an existing free variable.
Slide 12: Constraint 3
- Do not introduce$\forall$on the basis of an individual (a constant).
Slide 13: Constraint 4
- Do not introduce$\forall$on the basis of an unknown.
Slide 14: Constraint 5
- Do not quantify a variable by introducing$\forall$in a formula if the formula contains another var obtained by eliminating$\exists$.
Slide 15: Constraint 6
- Within the scope of an assumption, do not introduce$\forall$on the basis of a variable appearing in the assumption.
Slide 16: Constraint 7
- Every instantiation, whether following the elimination of a$\forall$or$\exists$, must always be done with a free var, rather than a bound var.
Slide 17: Constraint 8
- Beware of binding any newly quantified var by an unintended quantifier.
Slide 18: Summary
- Use inference rules to eliminate and introduce logical connectives.
- Handle quantifiers carefully, following constraints when eliminating and introducing them.
Slide 19: Summary of Constraints
- Do not assume a property holds for a particular individual based on it holding for at least one individual.
- When eliminating$\exists$, do not instantiate its var with a constant or existing free var.
- Do not introduce$\forall$on the basis of a constant or unknown.
- Do not quantify a variable by introducing$\forall$if the formula contains another var from$\exists$elimination.
- Within an assumption, do not introduce$\forall$based on a var in the assumption.
- Instantiate variables only with free vars, not bound vars.
- Avoid binding newly quantified vars by unintended quantifiers.
Slide 20: Deducing a Conclusion
Example: 1.$\forall x \cdot (\text{master}(x) \lor \text{slave}(x)) \Rightarrow \text{adult}(x) \land \text{man}(x)$ 2.$\neg \forall x \cdot (\text{adult}(x) \land \text{man}(x))$ 3.$\exists x \cdot (\neg (\text{adult}(x) \land \text{man}(x)))$ 4.$\neg (\text{master}(x) \lor \text{slave}(x))$ 5.$\neg \text{master}(x) \land \neg \text{slave}(x)$ 6.$\neg \text{master}(x)$ 7.$\exists y \cdot (\neg \text{master}(y))$