# 辅导案例-COMP2620

Final Examination, Semester 1 2018
LOGIC
(COMP2620 and PHIL2080)
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 
(10) 9
(11) 1, 6 , 10 
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  →I
2 (10) p∨ (r→s) 9 vI
1 (11) p∨ (r→s) 1, 6 , 10  ∨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  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  ∃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  ∃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  ∃E
1, 2 (16) ∃xHx 1, 9 , 15  ∨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 , 9  ∨E
1, 2 (11) Gf(f(a))→Ga 10  →I
1 (12) Fa→(Gf(f(a))→Ga) 11  →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 , 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  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.
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  RAA
Z, 6 (8) ¬B 5, 6  RAA
Y,Z, 6 (9) ¬A∧¬B 7, 8 ∧I
X,Y, Z (10) ¬¬C 1, 9  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  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  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  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  RAA
Y, 4 (6) ∀v¬Avm 5 ∀I
X,Y (7) ¬¬B 1, 7  RAA
X,Y (8) B 7¬¬E
Page 11 of 11 – LOGIC – (COMP2620, PHIL2080)  Email:51zuoyejun

@gmail.com