辅导案例-COMP2620
Final Examination, Semester 1 2018 LOGIC (COMP2620 and PHIL2080) Specimen answers Page 1 of 11 – LOGIC – (COMP2620, PHIL2080) A1 (a) ] In first order logic, what is a term? A term is the result of applying an n-ary function symbol to n terms (i.e. terms in virtue of this definition). This includes the case n = 0 where the term is a name. A1 (b) State the rule ∃E. X ` ∃vAvm Y,A ` B (m not in B or in any formula in Y ) ∃E X,Y ` B A1 (c) Express ∃(x : ∀(y : Rxy) Fy) ¬∀(z : Rxz) Gz using unrestricted (unary) quantifiers. ∃x(∀y(Rxy→Fy)∧¬∀z(Rxz→Gz)) A1 (d) What are numerically indefinite quantifiers? ’At least n’ and ’at most n’ for a given natural number n. These can be expressed in first order logic with identity as ∀x1 . . . ∀xn−1∃y(Fy ∧x1 6= y ∧ . . . ∧xn−1 6= y) ∃x1 . . . ∃xn∀y(Fy→(x1 = y ∨ . . . ∨xn = y)) A1 (e) Briefly, what is the sorites paradox? It is a logical puzzle regarding vague predicates P such that the truth value of P (a) seems insensitive to small changes in some aspect of a but sensitive to large changes in that aspect of a, although the large change is made up of small ones. This creates apparent counter-examples to→E and similar foms of inference where these are iterated many times. Page 2 of 11 – LOGIC – (COMP2620, PHIL2080) A2 (a) Use a semantic tableau to show that the following sequent is valid: ∀x(Fx→∃y(Gy ∨Rxy)),¬∃x(Fx∧Gx) ` ∀x(Fx→∃y(¬Fy ∨Rxy)) 1. t: ∀x(Fx→∃y(Gy ∨Rxy)) 2. t: ¬∃x(Fx∧Gx) 3. f: ∀x(Fx→∃y(¬Fy ∨Rxy)) 4. f: ∃x(Fx∧Gx) from 2 5. f: Fa→∃y(¬Fy ∨Ray) from 3 6. t: Fa 7. f: ∃y(¬Fy ∨Ray) 8. t: Fa→∃y(Gy ∨Ray) from 1 9. f: Fa × t: ∃y(Gy ∨Ray) 10. t: Gb∨Rab 11. f: ¬Fb∨Rab from 7 12. f: ¬Fb 13. f: Rab 14. t: Fb 15. t: Gb t: Rab × from 10 16. f: Fb∧Gb from 4 17. f: Fb × f: Gb × Page 3 of 11 – LOGIC – (COMP2620, PHIL2080) A2 (b) The following is a “model” produced by Logic for Fun. thing | 0 1 2 ------+------------------ F | TRUE TRUE FALSE R | 0 1 2 --+------------------ 0 | FALSE FALSE FALSE 1 | TRUE FALSE TRUE 2 | FALSE FALSE TRUE a = 1 b = 1 c = 2 A2 (b.i) Re-express this as an interpretation in the technical set-theoretic style, defining the domain D and interpretation function I. The domain of the interpretation is the sort “thing”: D = {0, 1, 2} The interpretation function assigns values to the symbols in the vocabu- lary: I(a) = 1 I(b) = 1 I(c) = 2 I(F ) = {0, 1} I(R) = {〈1, 0〉, 〈1, 2〉, 〈2, 2〉} A2 (b.ii) Explain, with detailed reference to the evaluation conditions for con- nectives and quantifiers how the formula ∀x∀y((Rxy→Ryx)→(Fx→Fy)) gets its truth value for this interpretation. Consider the interpretation I[a←0,b←2]. Call it K for brevity. Since it is a b-variant of an a-variant of I, we know K(F ) = I(F ) and K(R) = I(R). Clearly, K(a) = 0 and K(b) = 2. Now: truth value because Rab false for K 〈0, 2〉 /∈ K(R) Rab→Rba true for K Rab false for K Fa true for K 0 ∈ K(F ) Fb true for K 2 /∈ K(F ) Fa→Fb false for K Fa true, Fb false for K (Rab→Rba)→(Fa→Fb) false for K truth table for → ∀y((Ray→Rya)→(Fa→Fy)) false for I[a←0] (Rab→Rba)→(Fa→Fb) false for a b-variant ∀x∀y((Rxy→Ryx)→(Fx→Fy)) false for I ∀y((Ray→Rya)→(Fa→Fy) false for an a-variant Page 4 of 11 – LOGIC – (COMP2620, PHIL2080) 2c.i The following natural deduction proof in propositional logic has some parts missing. Fill in the gaps to make a valid proof. Note that all discharges of assumptions are as given in the right column. (1) A (2) A (3) A (4) q→r 3 [ ] (5) p (6) 5 (7) 2, 4 [ ] (8) s 7 (9) 8 [3] (10) 9 (11) 1, 6 [5], 10 [2] 1 (1) p∨¬(q→r) A 2 (2) ¬(q→r) A 3 (3) r A 3 (4) q→r 3 [ ] →I 5 (5) p A 5 (6) p∨ (r→s) 5 ∨I 2, 3 (7) ¬¬s 2, 4 [ ] RAA 2, 3 (8) s 7¬¬E 2 (9) r→s 8 [3] →I 2 (10) p∨ (r→s) 9 vI 1 (11) p∨ (r→s) 1, 6 [5], 10 [2] ∨E Page 5 of 11 – LOGIC – (COMP2620, PHIL2080) 2c.ii Prove in the natural deduction calculus: ∀x∃y(Rxy ∧¬Fy),∀x(¬Gx→Fx) ` ∀x∃y(Gy ∧Rxy 1 (1) ∀x∃y(Rxy ∧¬Fy) A 2 (2) ∀x(¬Gx→Fx) A 1 (3) ∃y(Ray ∧¬Fy) 1 ∀E 4 (4) Rab∧¬Fb A (instance of 3, for ∃E) 4 (5) Rab 4 ∧E 4 (6) ¬Fb 4 ∧E 7 (7) ¬Gb A 2 (8) ¬Gb→Fb 2 ∀E 2, 7 (9) Fb 7, 8→E 2, 4 (10) ¬¬Gb 6, 9 [7] RAA 2, 4 (11) Gb 10¬¬E 2, 4 (12) Gb∧Rab 5, 11 ∧I 2, 4 (13) ∃y(Gy ∧Ray) 12 ∃I 1, 2 (14) ∃y(Gy ∧Ray) 3, 13 [4] ∃E Page 6 of 11 – LOGIC – (COMP2620, PHIL2080) B1 (a) ∃xFx∨∃xGx, ∀x((Fx∨Gx)→Hx) ` ∃xHx 1 (1) ∃xFx∨∃xGx A 2 (2) ∀x((Fx∨Gx)→Hx) A 3 (3) ∃xFx A (left disjunct for ∨E) 4 (4) Fa A (instance of 3 for ∃E) 2 (5) (Fa∨Ga)→Ha 2 ∀E 4 (6) Fa∨Ga 4 ∨I 2, 4 (7) Ha 5, 6→E 2, 4 (8) ∃xHx 7 ∃I 2, 3 (9) ∃xHx 3, 8 [4] ∃E 10 (10) ∃xGx A (right disjunct for ∨E) 11 (11) Ga A (instance of 10 for ∃E) 11 (12) Fa∨Ga 11 ∨I 2, 11 (13) Ha 5, 12→E 2, 11 (14) ∃xHx 13 ∃I 2, 10 (15) ∃xHx 10, 14 [11] ∃E 1, 2 (16) ∃xHx 1, 9 [3], 15 [10] ∨E B1 (b) ∀x(Fx→(x = f(x)∨Gx)) ` ∀x(Fx→(Gf(f(x))→Gx)) 1 (1) ∀x(Fx→(x = f(x)∨Gx)) A 2 (2) Fa A 3 (3) Gf(f(a)) A 1 (4) Fa→(a = f(a)∨Ga) 1 ∀E 1, 2 (5) a = f(a)∨Ga 2, 4→E 6 (6) a = f(a) A 6 (7) a = f(f(a)) 6, 6 =E 3, 6 (8) Ga 3, 7 =E 9 (9) Ga A 1, 2, 3 (10) Ga 5, 8 [6], 9 [9] ∨E 1, 2 (11) Gf(f(a))→Ga 10 [3] →I 1 (12) Fa→(Gf(f(a))→Ga) 11 [2] →I 1 (13) ∀x(Fx→(Gf(f(x))→Gx)) 12 ∀I Page 7 of 11 – LOGIC – (COMP2620, PHIL2080) B1 (c) ∀(x : ∃yRxy) (Fx∨Gx), ∃(x : ¬Fx) Rxa ` ∃(x : Gx) ∃yRxy 1 (1) ∀(x : ∃yRxy) (Fx∨Gx) A 2 (2) ∃(x : ¬Fx) Rxa A 3 (3) ¬Fb A 4 (4) Rba A 4 (5) ∃yRby 4 ∃I 1, 4 (6) Fb∨Gb 1, 5 ∀ER 7 (7) Fb A 3, 7 (8) ¬¬Gb 3, 7 [ ] RAA 3, 7 (9) Gb 8¬¬E 10 (10) Gb A 1, 3, 4 (11) Gb 6, 9 [7], 10 [10] ∨E 1, 3, 4 (12) ∃(x : Gx) ∃yRxy 5, 11 ∃IR 1, 2 (13) ∃(x : Gx) ∃yRxy 2, 12 [3,4] ∃ER Page 8 of 11 – LOGIC – (COMP2620, PHIL2080) B2 We know that all truth functions can be represented using conjunction and negation (∧ and ¬) only. Define disjunction (∨ ) and implication (→) in terms of conjunction and negation. Show that the introduction and elimination rules ∨I, ∨E, →I and→E are all derivable on your definitions using ∧I, ∧E, RAA and¬¬E only. Similarly, the existential quantifier can be defined in terms of the universal one by taking ∃vA to mean ¬∀v¬A. Show that the rules ∃I and ∃E are derivable on that definition using ∀I and ∀E and the negation rules. For instance, for ∃I , you must show that if a sequent X `Atv is provable then so is X ` ¬∀v¬A. This question is not actually very complicated or difficult, although most students who attempted it scored badly on it. Defining disjunction and implication is easy: A∨B =df ¬(¬A∧¬B) A→B =df ¬(A∧¬B) In terms of these definitions, we may write the introduction and elimina- tion rules using conjunction and negation. ∨I becomes: A ∨I ¬(¬A∧¬B) A ∨I ¬(¬B ∧¬A) To derive these, we need to show that if any sequent X `A is derivable, then so are X ` ¬(¬A∧¬B) and X ` ¬(¬B ∧¬A). This is not difficult: X (1) A proved somehow 2 (2) ¬A∧¬B A 2 (3) ¬A 2 ∧E X (4) ¬(¬A∧¬B) 1, 3 [2] RAA There proof of the other ∨I rule is exactly similar, with the conjuncts in the4 opposite order, and is omitted here. ∨E is slightly more complicated. It reads X ` ¬(¬A∧¬B) Y,A `C Z,B `C ∨E X,Y, Z `C We suppose that the three input sequents are all derivable, and proceed thus: Page 9 of 11 – LOGIC – (COMP2620, PHIL2080) X (1) ¬(¬A∧¬B) proved somehow 2 (2) A A Y, 2 (3) C proved somehow 4 (4) B A Z, 4 (5) C proved somehow 6 (6) ¬C A Y, 6 (7) ¬A 3, 6 [2] RAA Z, 6 (8) ¬B 5, 6 [4] RAA Y,Z, 6 (9) ¬A∧¬B 7, 8 ∧I X,Y, Z (10) ¬¬C 1, 9 [6] RAA X,Y, Z (11) C 10¬¬E For→E we need to show that if X ` ¬(A∧¬B) and Y `A are both deriv- able, then so is X,Y `B. This follows the same pattern as above: X (1) ¬(A∧¬B) proved somehow Y (2) A proved somehow 3 (3) ¬B A Y, 3 (4) A∧¬B 2, 3 ∧I X,Y (5) ¬¬B 1, 4 [3] RAA X,Y (6) B 5¬¬E →I is not so trivial. We really need to appeal to “cut” in the form: if X `A and Y,A `B then X,Y `B. This will not be proved here; it is done by induction on the length of proofs, and is straightforward. Given cut, it is not hard to emulate →I with ∧ and ¬. Suppose X,A `B is derivable. Then: 1 (1) A∧¬B A 1 (2) A 1 ∧E X,A (3) B proved somehow X, 1 (4) B 2, 3 cut 1 (5) ¬B 1 ∧E X (6) ¬(A∧¬B) 4, 5 [1] RAA The analogous proof that the existential quantifier rules can be derived using the universal quantifier and negation is rather similar. For ∃I , suppose that we have a proof of X `Atv. We need to show that it can be extended to a proof of the sequent X ` ¬∀x¬A: Page 10 of 11 – LOGIC – (COMP2620, PHIL2080) X (1) Atv proved somehow 2 (2) ∀x¬A A 2 (3) ¬Atv 2 ∀E X (4) ¬∀x¬A 1, 3 [2] RAA Finally, ∃E on the suggestyed definition reads X ` ¬∀v¬Avm Y,A ` B (m not in B or Y ) ∃E X,Y ` B As before, suppose the two input sequents are provable, and that m does not occur in Y or in B. Then: X (1) ¬∀v¬Avm proved somehow 2 (2) A A Y, 2 (3) B proved somehow 4 (4) ¬B A Y, 4 (5) ¬A 3, 4 [2] RAA Y, 4 (6) ∀v¬Avm 5 ∀I X,Y (7) ¬¬B 1, 7 [4] RAA X,Y (8) B 7¬¬E Page 11 of 11 – LOGIC – (COMP2620, PHIL2080)