160 lines
6.2 KiB
Markdown
160 lines
6.2 KiB
Markdown
### **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**
|
||
1. Reduce formulae to propositional form by removing quantifiers.
|
||
2. Manipulate formulae using inference rules and logical laws of propositional logic.
|
||
3. 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**
|
||
1. Do not assume a property holds for a particular individual based on it holding for at least one individual.
|
||
2. When eliminating$\exists$, do not instantiate its var with a constant or existing free var.
|
||
3. Do not introduce$\forall$on the basis of a constant or unknown.
|
||
4. Do not quantify a variable by introducing$\forall$if the formula contains another var from$\exists$elimination.
|
||
5. Within an assumption, do not introduce$\forall$based on a var in the assumption.
|
||
6. Instantiate variables only with free vars, not bound vars.
|
||
7. 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))$
|
||
|
||
---
|
||
|