Created
March 17, 2011 19:31
-
-
Save kanak/874964 to your computer and use it in GitHub Desktop.
Discrete Math Using a Computer: Chapter 7 Review Exercises Solutions
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #+TITLE: DiscreteMathComputer 07-Predicate Logic | |
| #+DATE: | |
| #+LATEX_HEADER: \usepackage{fullpage} | |
| #+OPTIONS: H:3 toc:nil | |
| * Introduction: Why Predicates Logic | |
| - Want to make the statement that everything has a certain property | |
| + e.g. "All men are mortal" | |
| - Propositional Logic doesn't provide us any structure to express this | |
| + e.g. could say "P = all men are mortal" | |
| + but P is atomic, and we can't make any use of the fact that the property is supposed to hold everywhere | |
| - Predicate Logic is propositional logic with quantifiers | |
| * Language of Predicate Logic | |
| ** Predicates | |
| - A statement that an object has a property | |
| + e.g. x is even | |
| - We write predicate names with capital letters and variables in lowercase | |
| + e.g. $F(x)$ | |
| *** Definition: Predicate | |
| - Any term in the form $F(x)$, where F is a predicate name and $x$ is a variable name is a well formed formula | |
| - Similarly, $F(x_1, x_2, \cdots, x_k)$ is a well formed formula and represents a predicate with $k$ variables | |
| *** Definition: Universe | |
| - Defines the set of values that variables can have | |
| - e.g. for "x is even", we can define the universe as the natural numbers | |
| - Universe usually written $U$ | |
| ** Quantifiers | |
| *** Definition: Universal Quantification $\forall$ | |
| - Suppose $F(x)$ is a WFF involving the variable $x$ | |
| - Then, $\forall x. F(x)$ is a WFF called *universal quantification* | |
| - It says that every item in the universe has the property $F$ | |
| *** Examples of Universal Quantification | |
| - $\forall x. E(x), U = \{x \in \mathbb{N} | even(x)\}$ where $E(x)$ means $x$ is even | |
| - This says that every item in the set of even natural numbers is even. | |
| - It is true. | |
| - $\forall x \in \mathbb{N}. E(x)$ | |
| - This says that every natural number is even. | |
| - It is false. Counterexample: 1 | |
| *** Definition: Existential Quantification $\exists$ | |
| - Suppose $F(x)$ is a WFF involving the variable $x$ | |
| - Then, $\exists x. F(x)$ is a WFF called *existential quantification* | |
| - It says that at least one item in the universe has the property. | |
| *** Examples of Existential Quantification | |
| - $\exists x \in \mathbb{N}. 2 * x = 6$ | |
| - Says that there is a natural number which when multiplied by 2 gives 6. | |
| - This is true (x = 3) | |
| - $\exists x \in \mathbb{Q}. x * x = 2$ | |
| - Says that there is a rational number which when multiplied by itself gives 2 | |
| - This is false ($\sqrt{2}$ is irrational) | |
| *** Nesting Quantifiers | |
| - Want to say: for every integer, there is another one that is larger | |
| - $\forall x \in \mathbb{Z}, \exists y \in \mathbb{Z}, x < y$ | |
| - Note that order is significant | |
| - $\exists x \in \mathbb{Z}, \forall y \in \mathbb{Z}, x < y$ says that there is an integer that is smaller than every other integer. This is false. | |
| ** Expanding Quantified Expressions | |
| *** Expansions | |
| - $\forall x. F(x) = F(c_1) \wedge F(c_2) \wedge \cdots \wedge F(c_n)$ | |
| - $\exists x. F(x) = F(c_1) \vee F(c_2) \vee \cdots \vee F(c_n)$ | |
| *** Exercise 1 | |
| - $U = \{1,2,3\}$ | |
| - Remove the quantifiers in the following | |
| - $\forall x. F(x)$ | |
| + $F(1) \wedge F(2) \wedge F(3)$ | |
| - $\exists x. F(x)$ | |
| + $F(1) \vee F(2) \vee F(3)$ | |
| - $\exists x. \forall y. G(x, y)$ | |
| - $(G(1,1) \wedge G(1,2) \wedge G(1,3)) \vee (G(2,1) \wedge G(2,2) \wedge G(2,3)) \vee (G(3,1) \wedge G(3,2) \wedge G(3,3))$ | |
| *** Exercise 2 | |
| - $U = \mathbb{Z}$ | |
| - Expand: $\forall x \in \{1,2,3,4\}. \exists y \in \{5,6\}. F(x,y)$ | |
| - $(F(1,5) \vee F(1,6)) \wedge (F(2,5), F(2,6)) \wedge (F(3,5), F(3,6)) \wedge (F(4,5) \vee F(4,6))$ | |
| ** Scope of Variable Bindings | |
| - Use parentheses to clarify scope | |
| - Assume smallest scope is smallest subexpression otherwise | |
| ** Translating Between English and Logic | |
| *** Example: "Some birds can fly" | |
| - Assume universe is all animals | |
| - $B(x)$ is true if x is a bird | |
| - $F(x)$ is true if x can fly | |
| - Then, $\exists x. B(x) \wedge F(x)$ expresses "some birds can fly" | |
| - *NOTE*: $\exists x. B(x) \Rightarrow F(x)$ is wrong | |
| + If $B(x)$ is false, then the implication is true | |
| + Then, if x is a horse, the implication is true | |
| + Suppose all the birds in the universe can't actually fly | |
| + Since we've found something that makes the implication true, by existential quantification, the implication is true | |
| + This is a contradiction | |
| *** Exercise 3: Express the statements formally | |
| - Given: $E(x)$ means x is even, $O(x)$ means x is odd, Universe is natural numbers | |
| - There is an even number. | |
| + $\exists x. E(x)$ | |
| - Every number is either even or odd. | |
| + $\forall x. E(x) \vee O(x)$ | |
| - No number is both even and odd. | |
| + $\forall x. \neg(E(x) \wedge O(x))$ | |
| - Sum of two odd numbers is even | |
| + $\forall x,y. O(x) \wedge O(y) \Rightarrow E(x + y)$ | |
| - Sum of an odd number and an even number is odd | |
| + $\forall x,y. O(x) \wedge E(y) \Rightarrow O(x + y)$ | |
| - We don't have the same bug as "some birds can fly" with the implication because we're doing a universal quantification and not an existential one. So, if there is a single pair of odd numbers whose sum is not even, the implication would be false, which is what we want. | |
| *** Exercise 4: Animal Logic 193 | |
| - Given: predicates for Bird, Dove, Chicken, Pig, Fly, Wings, $M(x,y)$ means x has more feathers than y | |
| - Chickens are bird | |
| + $\forall x. C(x) \Rightarrow B(x)$ | |
| - Some doves can fly | |
| + $\exists x. D(x) \wedge F(x)$ | |
| - Pigs are not birds | |
| + $\forall x. P(x) \Rightarrow \neg B(x)$ | |
| - Some birds can fly, some can't | |
| + $\exists x. B(x) \wedge F(x)$ | |
| - An animal needs wings in order to fly | |
| + $\forall x. F(x) \Rightarrow W(x)$ | |
| - If a chicken can fly, then pigs have wings | |
| + $\exists x, \forall y. (C(x) \wedge F(x)) \Rightarrow (P(y) \wedge W(y))$ | |
| - Chickens have more feathers than pigs do. | |
| + $\forall x, \forall y. C(x) \wedge P(y) \wedge M(x,y)$ | |
| - An animal with more feathers than any chicken can fly. | |
| - $\forall x, \forall y. C(y) \wedge M(x,y) \Rightarrow F(x)$ | |
| *** Exercise 5: Back to english | |
| - $\forall x. (\exists y. wantsToDanceWith (x, y)$ | |
| + everyone has someone they would like to dance with | |
| - $\exists x. (\forall y. wantsToPhone(y,x))$ | |
| + everyone has someone they would like to phone | |
| - $\exists x. (tired(x) \wedge \forall y. helpsMoveHouse(x,y)) | |
| + there is someone who will help anyone move despite being tired | |
| * Computing with Quantifiers | |
| - Predicate is just a function that returns a boolean | |
| - Quantifiers built into haskell | |
| + all : a -> Bool -> [a] -> Bool | |
| + any : a -> Bool -> [a] -> Bool | |
| + and : [Bool] -> Bool | |
| + or : [Bool] -> Bool | |
| ** Exercise 6: Haskell expression to Logic, compute value | |
| - Note: using haskell's builtin functions instead of equivalent Stdm ones | |
| - all (== 2) [1,2,3] | |
| + $\forall x \in \{1,2,3\}. x = 2$ | |
| + False: counterexample is '1' | |
| - all (< 4) [1,2,3] | |
| + $\forall x \in \{1,2,3\}. x < 4$ | |
| + True | |
| ** Exercise 7: Haskell expressions to Logic, compute values | |
| - any (== 2) [0,1,2] | |
| + $\exists x \in \{1,2,3\}. x = 2$ | |
| + True | |
| - any (> 5) [1,2,3] | |
| + $\exists x \in \{1,2,3\}. x > 5$ | |
| + False | |
| ** Example 7: $\forall x \in \{1,2}. (\exists y \in \{1,2\}. x = y)$ | |
| - Convert to haskell | |
| - every (\ x -> any (== x) [1,2]) [1,2] | |
| - (any (== 1) [1,2]) && every (\ x -> any (== x) [1,2]) [ 2] | |
| - ((== 1) 1 || any (== 1) [ 2]) && every (\ x -> (== x) [1,2]) [ 2] | |
| - (True || any (== 1) [ 2]) && every (\ x -> (== x) [1,2]) [ 2] | |
| - True && every (\ x -> (== x) [1,2]) [ 2] | |
| - every (\ x -> (== x) [1,2]) [ 2] | |
| - True && every (\ x -> (== x) [1,2]) [] | |
| - True | |
| ** Exercise 8: Calculate values of expressions | |
| - $p x y$ means $x = y + 1$ | |
| - $U = \{1,2\}$ | |
| - $\forall x. (\exists y. p(x,y))$ | |
| + $(\exists y. p(1,y)) \wedge (\exists y. p(2,y))$ (by removing forall) | |
| + $(p(1,1) \vee p(1,2)) \wedge (p(2,1) \vee p(2,2)$ (by removing exists) | |
| + $(False \vee False) \wedge (True \vee False)$ | |
| + $False \wedge True$ | |
| + $False$ | |
| + (Haskell verification: all (\ x -> any (p x) [1,2]) [1,2] gives False) | |
| - $\exists x, y. p(x,y)$ | |
| + $(\exists x. \exists y p(x, y)$ | |
| + $((\exists y. p(1,y)) \vee (\exists x. p(2, y))$ (by removing exists x) | |
| + $((p(1,1) \vee p(1,2)) \vee (p(2,1) \vee p(2,2))$ | |
| + Since $p(2, 1)$ is true, the whole expression is True | |
| + (Haskell verification: any (\ x -> any (p x) [1,2]) [1,2] gives True) | |
| - $\exists x. (\forall y. p(x,y))$ | |
| + $(\forall y. p(1,y)) \wedge (\forall y. p(2,y))$ (by removing exists) | |
| + $(p(1,1) \vee p(2,1)) \wedge (p(1,2) \vee p(2,2))$ (by removing forall) | |
| + $(False \vee True) \wedge (False \vee False)$ | |
| + $True \wedge False$ | |
| + (haskell verification: any (\ x -> all (p x) [1,2]) [1,2] gives False) | |
| - $\forall x, y. p(x,y)$ | |
| + $(\forall y. p(1,y)) \wedge (\forall y. p(2,y))$ (removing forall) | |
| + $(p(1,1) \wedge p(1,2)) \wedge (p(2,1) \wedge p(2,2))$ (removing forall) | |
| + Since $p(1,1)$ is false, the whole thing becomes false | |
| + (haskell verification: all (\ x -> all (p x) [1,2]) [1,2] gives False) | |
| * Logical Inference with Predicates | |
| ** Introduction | |
| - Can view inference rules of predicate logic as generalizations of rules from propositional logic | |
| - If universe is finite, then the rules might not be necessary | |
| + e.g. $\forall x. F(x)$ could be replaced by $F(x_1), \cdots F(x_n)$, $n$ is the size of the universe | |
| + But, propositional inference rules allow us to do deductions when the universe is infinite | |
| - Assume universe is nonempty | |
| + e.g. forall elimination is invalid when the universe is empty | |
| ** Universal Introduction | |
| - If you can prove an element about an arbitrary element of the universe, you have a statement about all elements of the universe. | |
| *** Append Example | |
| **** Definition | |
| #+begin_src haskell | |
| (++) :: [a] -> [a] -> [a] | |
| [] ++ ys = ys | |
| (x:xs) ++ ys = x : (xs ++ ys) | |
| #+end_src | |
| **** Theorem: $Let x :: a, xs :: [a]. Then, x:xs = [x] ++ xs$ | |
| - Proof follows directly from the definition of append | |
| - RHS = [x] ++ xs = x : xs = LHS | |
| **** Theorem: $\forall x :: a. \forall xs :: [a]. x:xs = [x] ++ xs$ | |
| - This theorem makes the same claim as the previous | |
| - Style is different: | |
| + Previous one talked about arbitrary elements from the universe | |
| + This makes claim about all elements in the universe | |
| *** Universal Introduction Definition | |
| - $F(x), {x arbitrary} \vdash \forall x. F(x)$ | |
| *** Example: $\vdash \forall x. E(x) \Rightarrow (E(x) \vee \neg E(x))$ | |
| - Proof Idea: | |
| + We need an implication, which means we have to do Imply Introduction | |
| + To do an imply introduction, we need to prove the sequent $E(x) \Rightarrow E(x) \vee \neg E(x)$ | |
| + $E(x) \vee \neg E(x)$ can be shown just by assuming either $E(x)$ or $\neg E(x)$ to be true | |
| - Proof | |
| + Assume $E(p)$, $p$ is an arbitrary value | |
| + By _Or introduction_, we have $E(p) \vdash E(p) \vee \neg E(p)$ | |
| + This sequent doesn't rely on any more assumptions, and in particular, we can discharge the $E(x)$ assumption | |
| + By _Introduce Implication_, we have $E(p) \Rightarrow E(p) \vee \neg E(p)$ | |
| + Since $p$ is arbitrary, by _introduce forall_, we have $\forall x. E(x) \Rightarrow E(x) \vee \neg E(x)$ | |
| *** Anti-Example: All natural numbers are even | |
| - Let $E(x)$ mean that $x$ is even | |
| - $E(2) \vdash \forall x. E(x)$ [WRONG] | |
| - Problem is that we didn't show that it works for an arbitrary natural number; we just showed that it works for a particular one. | |
| ** Universal Elimination | |
| *** Definition | |
| - $\forall x. F(x) \vdash F(p)$ | |
| - If you have established a property for everything in the universe, you can assume it holds for a particular element of the universe. | |
| *** Example: $F(p), \forall x. F(x) \Rightarrow G(x) \vdash G(p)$ | |
| - By _forall elimination_, $\forall x. F(x) \Rightarrow G(x) \vdash F(p)$ where $p$ is the same variable as in $F(p)$ | |
| - Now we have $F(p), F(p) \Rightarrow G(p)$ | |
| - By _Modus Ponens_, we have $G(p)$ | |
| *** Example: $\forall x. F(x) \Rightarrow G(x), \forall x. G(x) \Rightarrow H(x) \vdash \forall x. F(x) \Rightarrow H(x)$ | |
| - By _forall elimination_, $F(p) \Rightarrow G(p)$ for an arbitrary $p$ | |
| - By _forall elimination_, $G(p) \Rightarrow H(p)$ | |
| - By _implication chain_, $F(p) \Rightarrow G(p), G(p) \Rightarrow H(p) \vdash F(p) \Rightarrow H(p)$ | |
| - Since this is for an arbitrary $p$, we can use _forall introduction_ to get $\forall x. F(x) \Rightarrow G(x), \forall x. G(x) \Rightarrow H(x) \vdash \forall x. F(x) \Rightarrow H(x)$ | |
| *** Example: $\forall x. \forall y. F(x, y) \vdash \forall y. \forall x. F(x,y)$ | |
| - By _forall elimination_, we have $\forall y. F(p, y)$ where $p$ is arbitrary | |
| - By _forall elimination_, we have $F(p,q)$ where $q$ is arbitrary | |
| - By _forall introduction_, we have $\forall x. F(x, q)$ | |
| - By _forall introduction_, we have $\forall y. \forall x. F(x, q)$ | |
| - So, we have just shown that the order of forall quantifiers does not matter. | |
| *** Example: $\forall x. P \Rightarrow f(x) \vdash P \Rightarrow \forall x. f(x)$ | |
| - By _forall elimination_, we have $\forall x. P \Rightarrow f(x) \vdash P \Rightarrow f(c)$, $c$ is arbitrary | |
| - Assume P. Then, we have $P, P \Rightarrow f(c)$ | |
| - By _modus ponens_, we have $f(c)$. | |
| - By _forall introduction_, we have $\forall x. f(x)$ | |
| - By _introduce implication_, we have $P \Rightarrow \forall x. f(x)$ | |
| *** Exercise 9: Prove $\forall x. F(x), \forall x. F(x) \Rightarrow G(x) \vdash \forall x G(x)$ | |
| - By _forall elimination_, we have $F(c)$, c is arbitrary. | |
| - By _forall elimination_, we have $F(c) \Rightarrow G(c)$ | |
| - By _modus ponens_ on $F(c), F(c) \Rightarrow G(c)$, we have $G(c)$ | |
| - Since $c$ was arbitrary, we can _introduce forall_ to get $\forall x. G(x)$ | |
| ** Existential Introduction | |
| *** Definition | |
| - If $f(p)$ has been established for a particular $p$, then you can infer $\exists p. f(p)$ | |
| *** Example: $\forall x. F(x) \vdash \exists x. F(x)$ | |
| - By _forall elimination_, we have $F(c)$ for an arbitrary $c$ | |
| - By _exists introduction_, we have $\exists x. F(x)$ | |
| ** Existential Elimination | |
| *** Definition | |
| - Recall _or elimination_: | |
| + If you have $a \vee c$, and $a \vdash c$ and $b \vdash c$ then you have $c$ | |
| + This was proof by cases | |
| - Existential Elimination is a generalization of this idea | |
| - If you have $\exists x. F(x), F(c) \vdash A \{c arbitrary \}$ then you can infer $A$ | |
| *** Example: $\exists x. P(x), \forall x. P(x) \Rightarrow Q(x) \vdash \exists x. Q(x)$ | |
| - By _forall elimination_, we have $P(c) \Rightarrow Q(c)$, $c$ is arbitrary. | |
| - Assume $P(c)$. This is allowed because we have $\exists x, P(x)$ | |
| - By _modus ponens_ on $P(c), P(c) \Rightarrow Q(c)$, we have $Q(c)$. | |
| - By _existential introduction_ on $Q(c)$, we have $\exists x. Q(x)$ | |
| *** Example: $\exists x. \forall y F(x, y) \vdash \forall y. \exists x. F(x, y)$ | |
| - By _forall elimination_ on $\forall y F(x,y)$, we have $F(x,q)$, $q$ arbitrary | |
| - So we have $\exists x. F(x,q)$ | |
| - By _forall introduction_, we have $\forall y \exists x. F(x, y)$ | |
| *** Exercise 10: Prove $\exists x. \exists y. F(x, y) \vdash \exists y. \exists x. F(x, y)$ | |
| - Assume $F(a,b)$. This is allowed because there must be atleast one $a$ and one $b$ for which $F$ holds. | |
| - By _existential elimination_, we have $\exists y. F(a, y)$, $a$ arbitrary | |
| - By _existential elimination_, we have $F(a, b)$, $b$ arbitrary | |
| - By _existential introduction_, we have $\exists x. F(x, b)$ | |
| - By _existential introduction_, we have $\exists y, \exists x. F(x, y)$ | |
| - (This proof might be incorrect) | |
| *** Exercise 11: Find a counterexample for: $\forall y, \exists x. F(x, y) \vdash \exists x. \forall y F(x,y)$ | |
| - Let $F(x,y)$ mean that $x$ is greater than $y$ | |
| - Suppose the universe is the natural numbers | |
| - Then, $\forall y, \exists x. F(x, y)$ says that the natural numbers is unbounded, which is correct | |
| - But, $\exists x. \forall y. F(x, y)$ says that there is some natural number that is larger than all others, which is incorrect. | |
| *** Exercise 12: Prove: $\forall x, (F(x) \wedge G(x)) \vdash (\forall x F(x)) \wedge (\forall x. G(x))$ | |
| - By _forall elimination_, we have $F(c) \wedge G(c)$, $c$ arbitrary | |
| - By _and elimination_, we have $F(c)$ as well as $G(c)$ | |
| - By _forall introduction_, we have $\forall x. F(x)$ as well as $\forall x. G(x)$ | |
| - By _and introduction_, we have $(\forall x F(x)) \wedge (\forall x. G(x))$ | |
| * Algebraic Laws of Predicate Logic | |
| ** Law: Introducing and removing quantifiers | |
| - $\forall x. f(x) \Rightarrow f(c)$ | |
| - $f(c) \Rightarrow \exists x. f(x)$ | |
| - Note that these are implications and only work in one direction | |
| ** Example: $\forall x. f(x) \Rightarrow \exists x. f(x)$ | |
| - $\forall x. f(x)$ | |
| - $f(c)$, for arbitrary $c$ | |
| - $\exists x. f(x)$ | |
| ** Law: Quantifiers and Negations | |
| - $\forall x. \neg f(x) = \neg (\exists x. f(x))$ | |
| - $\exists x. \neg f(x) = \neg (\forall x. f(x))$ | |
| ** Law: Combining Propositions | |
| - In all of the following, $q$ does not contain $x$ as a variable | |
| - $(\forall x. f(x)) \wedge q = \forall x (f(x) \wedge q)$ | |
| - $(\forall x. f(x)) \vee q = \forall x (f(x) \vee q)$ | |
| - $(\exists x. f(x)) \wedge q = \exists x. (f(x) \wedge q)$ | |
| - $(\exists x. f(x)) \vee q = \exists x. (f(x) \vee q)$ | |
| - Summary: we can push in propositions inside quantifiers if they don't have the quantified variable | |
| ** Laws: Combining Quantifiers | |
| - $\forall x. f(x) \wedge \forall x. g(x) = \forall x (f(x) \wedge g(x))$ | |
| - $\forall x. f(x) \vee \forall x. g(x) \Rightarrow forall x (f(x) \vee g(x))$ | |
| + we're going from a strong statement to a weak one | |
| + Strong statement: both properties $f$ and $g$ hold for all x | |
| + Weak statement: atleast one of $f$ and $g$ hold for all x | |
| - $\exists x. (f(x) \vee g(x)) \Rightarrow \exists x. f(x) \wedge \exists x. g(x)$ | |
| + Also going from strong to weak | |
| + Strong: there's atleast one element which has both properties $f$ and $g$ | |
| + Weak: there is atleast one element which has $f$, and atleast one which has $g$. The two elements don't have to be the same. | |
| - $\exists x. f(x) \vee \exists x. g(x) = \exists x. (f(x) \vee g(x))$ | |
| ** Example: $\forall x. (f(x) \wedge \neg g(x)) = \forall x. f(x) \wedge \neg \exists. g(x)$ | |
| - Direct proof starting from the left side | |
| - $\forall x. (f(x) \wedge \neg g(x))$ | |
| - $(\forall x. f(x)) \wedge (\forall x. \neg g(x))$ | |
| - $(\forall x. f(x)) \wedge \neg (\exists x. g(x))$ | |
| ** Example: $\exists x. (f(x) \Rightarrow g(x)) \wedge (\forall x. f(x)) \Rightarrow \exists x. g(x)$ | |
| - Direct proof starting from the left side | |
| - First, _rename variable_ to get $\forall y. f(y)$ | |
| - Now, push the forall inside the exists to get $\exists x. ((f(x) \Rightarrow g(x)) \wedge \forall y. f(y))$ | |
| - _Remove the forall_ to get: $\exists x. ((f(x) \Rightarrow g(x)) \wedge f(x))$ | |
| - Use _modus ponens_ to get $\exists x. g(x)$ | |
| * Further Reading | |
| - See references at end of chapter 6 | |
| - *Mathematical Writing* by Knuth, larrabee, and Roberts | |
| - *Proofs from THE BOOK* by Aigner and Ziegler | |
| * Review Exercises | |
| ** Exercise 13 | |
| *** Problem | |
| - Universe has 10 elements | |
| - Expression: $\forall x. \exists y. \forall z F(x, y, z)$ | |
| - want to express it in a quantifier free form. | |
| *** How many times will $F$ occur in that form? | |
| - Eliminating $\forall z$, we have this innermost expression: $F(x, y, n_1) \wedge F(x, y, n_2) \wedge \cdots \wedge F(x, y, n_10)$ | |
| - This has 10 items | |
| - Eliminating the $\exists y$ replaces $F(x, y, n_1)$ with $F(x, n_1, n_1) \vee F(x, n_2, n_1) \vee \cdots \vee F(x, n_10, n_1)$ | |
| - So, 10 terms per term from before. (Total: 100) | |
| - Eliminating the $\forall x$ replaces each $F(x, n_1, n_1)$ with $F(n_1, n_1, n_1) \vee F(n_2, n_1, n_1) \vee \cdots \vee F(n_10, n_1, n_1)$ | |
| - So, 10 terms per term from before. (Total: 1000) | |
| - In general, we have $N^k$ terms where $N$ is size of universe, $k$ is the number of quantifiers we're removing | |
| ** Exercise 14: Prove $(\exists f(x)) \vee (\exists g(x)) \vdash \exists x. (f(x) \wedge g(x))$ | |
| - By _exists elimination_, we get $f(c)$ for some $c$ | |
| - By _exists elimination_, we get $g(d)$ for some $d$ | |
| - By _or introduction_, we get $f(c) \vee g(d)$ | |
| - By _exists introduction_, we get $\exists x. (f(x) \vee g(d))$ | |
| - By _exists introduction_, we get $\exists y \exists x. (f (x) \vee g(y))$ | |
| - Since the existence of either $x$ or $y$ makes the whole statement true, we can combine them to get $\exists x. f(x) \vee g(x)$ | |
| ** Exercise 15: Prove $(\forall x. f(x)) \vee (\forall x. g(x)) \vdash \forall x (f(x) \vee g(x))$ | |
| - By _forall elimination_, we get $f(c)$ for arbitrary $c$ | |
| - By _forall elimination_, we get $g(c)$ | |
| - By _or introduction_, we have $f(c) \vee g(c)$ | |
| - Since the above holds true for arbitrary $c$, by _universal introduction_, $\forall x. (f(x) \vee g(x))$ | |
| ** Exercise 16: Prove converse of Theorem 63 | |
| - Theorem 63: $\forall x. P \Rightarrow f(x) \vdash P \Rightarrow \forall x. f(x)$ | |
| - The converse of this is: $P \Rightarrow \forall x. f(x) \vdash \forall x. P \Rightarrow f(x)$ | |
| - Assume $P$. Then by _modus ponens_ on $P, P \Rightarrow \forall x. f(x)$, we have $\forall x. f(x)$ | |
| - By _forall elimination_, we have $f(c)$ | |
| - By _implies introduction_, we have $P \Rightarrow f(c)$ | |
| - By _forall introduction_, we have $\forall x. P \Rightarrow f(x)$ | |
| ** Exercise 17: Provide Counterexamples | |
| - In "combining quantifiers", we had two laws that were implications not equalities. | |
| - Provide counterexamples that show why the laws don't hold in the opposite direction | |
| - Counterexample for $\forall x. (f(x) \vee g(x)) \Rightarrow \forall x. f(x) \vee \forall x. g(x))$ | |
| + Suppose $f(x)$ means x is even | |
| + Suppose $g(x)$ means x is odd | |
| + Universe is natural numbers. | |
| + Then, left side is true because every number is either even or odd | |
| + But on the right side we also claim that every number is even, and every number is odd. Both of which are false. | |
| - More concrete counterexample: | |
| + Universe is: $\{Shrek, Donkey\}$ | |
| + $f(x)$ means $x = Shrek$ | |
| + $g(x)$ means $x = Donkey$ | |
| + Left Side: | |
| + $\forall x. (f(x) \vee g(x))$ | |
| + $(f(Shrek) \vee g(Shrek)) \wedge (f(Donkey) \vee g(Donkey))$ | |
| + $(True \vee False) \wedge (False \vee True)$ | |
| + $True$ | |
| + Right Side: | |
| + $(\forall x. f(x)) \vee (\forall x. g(x))$ | |
| + $(f(Shrek) \wedge f(Donkey)) \vee (g(Shrek) \wedge g(Donkey))$ | |
| + $(True \wedge False) \vee (False \wedge True)$ | |
| + $False \vee False = False$ | |
| + So, we're trying to do a $True \Rightarrow False$, which is $False$ | |
| - Counterexample for $\exists x. f(x) \wedge \exists x. g(x) \Rightarrow \exists x. (f(x) \wedge g(x))$ | |
| + Again using the Shrek, Donkey example | |
| + Left side: | |
| + $\exists x. f(x) \wedge \exists x. g(x)$ | |
| + $(f(Shrek) \vee f(Donkey)) \wedge (g(Shrek) \vee g(Donkey))$ | |
| + $(True \vee False) \wedge (False \vee True)$ | |
| + $True$ | |
| + Right side: | |
| + $\exists x. (f(x) \wedge g(x))$ | |
| + $(f(Shrek) \wedge g(Shrek)) \vee (f(Donkey) \wedge g(Donkey))$ | |
| + $(True \wedge False) \vee (False \wedge True)$ | |
| + $False \vee False$ | |
| + $False$ | |
| + So, we're trying to do a $True \Rightarrow False$, which is $False$ | |
| ** TODO: Exercise 18: Prove $(\forall x. f(x) \Rightarrow h(x) \wedge \forall x. g(x) \Rightarrow h(x)) \Rightarrow \forall x. (f(x) \vee g(x) \Rightarrow h(x))$ | |
| - By using the laws on combining quantifiers, we can get $\forall x. ((f(x) \Rightarrow h(x)) \wedge (g(x) \Rightarrow h(x))$ | |
| - TODO: Now we need to do some kind of or elimination and combine. | |
| ** Exercise 19 | |
| - Universe is natural numbers | |
| - predicate: "if a number occurs in either of the sequences that are arguments to append, it occurs in the final series as well" | |
| - (The proof is easy by induction, but they want something else) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment