Fudan University 复旦大学 2012-2013学年第二学期考试试卷 课程名称:离散数学(I) 课程代码:SOFT130040 开课院系:软件学院 考试形式:开卷 姓名 学号 专业 题 89—10总分 得分‖ DIRECTION: There are totally two pages of examination paper. You must write all your answers, include your name and student number clearly, on a specific answersheet. You have 2 hours to solve all the questi REMARK: All solutions are only for reference. Because there may be more than one method to solve a problem 1. Define a binary connective A e B whose truth table is given in Table 1. Answer the ABAb TTF Table 1: Truth table of e following questions (7 marks) (a)Prove or disprove that (,e) is adequate (2 marks (b)Add the atomic tableau of e into atomic tableaux (2 marks) ()Discuss the validity of (Ae B)+(Av-B by using tableau proof. 3 marks) Solution.(a) First A V B can be represented as A e-B.(1 mark) Hence (V, is adequate. , e) is also adequate. (1 mark (b)The tableau is shown in Figure 1. F and T each has 1 mark (c)The tableau is shown in Figure 2 It is a tableau proof. So the sentence/proposition valid 2. Give the following statements
Fudan University 复旦大学 2012-2013 学年第二学期考试试卷 课程名称: 离散数学 (II) 课程代码: SOFT130040.01 开课院系: 软件学院 考试形式: 开卷 姓名: 学号: 专业: 题目 1 2 3 4 5 6 7 8 9 10 总分 得分 Direction: There are totally two pages of examination paper. You must write all your answers, include your name and student number clearly, on a specific answersheet. You have 2 hours to solve all the questions. Remark: All solutions are only for reference. Because there may be more than one method to solve a problem. 1. Define a binary connective A ⊖ B whose truth table is given in Table 1. Answer the A B A ⊖ B T T T T F T F T F F F T Table 1: Truth table of ⊖ following questions. (7 marks) (a) Prove or disprove that {¬, ⊖} is adequate. (2 marks) (b) Add the atomic tableau of ⊖ into atomic tableaux. (2 marks) (c) Discuss the validity of (A ⊖ B) → (A ∨ ¬B) by using tableau proof. (3 marks) Solution. (a) First A ∨ B can be represented as A ⊖ ¬B. (1 mark) Hence {∨, ¬} is adequate. {¬, ⊖} is also adequate. (1 mark) (b) The tableau is shown in Figure 1. F and T each has 1 mark. (c) The tableau is shown in Figure 2 It is a tableau proof. So the sentence/proposition is valid. 2. Give the following statements: 1
FAeB T AeB FA TA FB T B Figure 1: Atomic tableau of e F(AeB)→(AV=B) T(AeB F(AV-B FA F-B T B T (AeB TA F B Figure 2: Tableau proof (a) The attack will succeed only if the enemy is taken by surprise or the position is weakly defended (b)The enemy will not be taken by surprise unless he is overconfident (c) The enemy will not be overconfident if the position is weakly defended (d)Therefore, the attack will not succeed Answer the following questions (7 marks (a) Translate the argument into propositions (4 marks) b) Use tableau proof to determine whether the argument is logically valid. 3 marks) Solution.(a)The proposition letters and its corresponding represented statement are as fo i. A: The attack will succeed B: The enemy is taken by surprise iii. C: The position is weakly defended iv. D: He is overconfident Then the statements can be represented as following: (each 0.5 mark) i.A→(BVC)
F A ⊖ B F A T B T A ⊖ B T A F B Figure 1: Atomic tableau of ⊖ F (A ⊖ B) → (A ∨ ¬B) T (A ⊖ B) F (A ∨ ¬B) F A F ¬B T B T (A ⊖ B) T A F B ⊗ ⊗ Figure 2: Tableau proof (a) The attack will succeed only if the enemy is taken by surprise or the position is weakly defended. (b) The enemy will not be taken by surprise unless he is overconfident. (c) The enemy will not be overconfident if the position is weakly defended. (d) Therefore, the attack will not succeed. Answer the following questions: (7 marks) (a) Translate the argument into propositions. (4 marks) (b) Use tableau proof to determine whether the argument is logically valid. (3 marks) Solution. (a) The proposition letters and its corresponding represented statement are as following:(each 0.5 mark) i. A: The attack will succeed. ii. B: The enemy is taken by surprise. iii. C: The position is weakly defended. iv. D: He is overconfident. Then the statements can be represented as following:(each 0.5 mark) i. A → (B ∨ C). 2
i.→D→-B. i.C→ iv, - A (b) The result is -A. The tableau proof is shown in Figure 3.(2 marks) F(=A) T A TA→(BVC) FA T(BVC) 6 TB TC TC→-D FC T-D Figure 3: Tableau proof As Figure 3 shown, there is at least a noncontradictory path. So the argument is not logically valid. (1 marks 3. Given a formula (, y, a)=(v)()va(a, y, a)),p(a, y, a), where a, 3, z are free variables. Answer the following questions (8m (a) Show which occurrence of every variable is free. If it is bound, show which quantifier bounds it (b)Given a function f(t, a) and t does not occurs in Is y/f(t, a) substitutable in p(a, y, a)? Show your reason. (2 marks (c) Discuss its truth of (a, y, 2). If it is not valid, give a model made it false. (3 marks) Solution.(a)The third occurrence of the second occurrence of z and both occurrences of y are free. (1 mark) The first two a is bounded by(Vr).(1 mark)The first z is bounded by 3z. (1 mark (b) The second substitution of y is substitutable for z, t in f is still free. However the first one is not for z is bounded by 3x(1 mark) Then it is not substitutable. (1 mark) (c) It is not a sentence. We first represent it as the V-closure form. It is valid. It could be proved by a tableau proof shown in Figure 4. Obviously, the tableau noncontradictory. (2 marks)So it is not valid. The counterexample is very simple Let A=co, C1, c21,v=(co1, p =0.(1 mark
ii. ¬D → ¬B. iii. C → ¬D. iv. ¬A. (b) The result is ¬A. The tableau proof is shown in Figure 3.(2 marks) F (¬A) T A T A → (B ∨ C) F A T (B ∨ C) ⊗ T B T C . . . T C → ¬D F C T¬D ⊗ F D Figure 3: Tableau proof As Figure 3 shown, there is at least a noncontradictory path. So the argument is not logically valid.(1 marks) 3. Given a formula Φ(x, y, z) = (∀x)(ψ(x)∨(∃z)φ(x, y, z)) → φ(x, y, z), where x, y, z are free variables. Answer the following questions. (8 marks) (a) Show which occurrence of every variable is free. If it is bound, show which quantifier bounds it. (3 marks) (b) Given a function f(t, z) and t does not occurs in Φ. Is y/f(t, z) substitutable in Φ(x, y, z)? Show your reason. (2 marks) (c) Discuss its truth of Φ(x, y, z).If it is not valid, give a model made it false. (3 marks) Solution. (a) The third occurrence of x, the second occurrence of z and both occurrences of y are free.(1 mark) The first two x is bounded by (∀x). (1 mark) The first z is bounded by ∃z.(1 mark) (b) The second substitution of y is substitutable for z, t in f is still free. However the first one is not for z is bounded by ∃z.(1 mark) Then it is not substitutable. (1 mark) (c) It is not a sentence. We first represent it as the ∀-closure form. It is valid. It could be proved by a tableau proof shown in Figure 4. Obviously, the tableau is noncontradictory.(2 marks) So it is not valid. The counterexample is very simple. Let A = {c0, c1, c2}, ψ = {c0}, φ = ∅. (1 mark) 3
Fⅵ arayA(x)(v(x)∨(彐zy(x,y,z)→φ(x,孙,z) F VyVz((va)((r)vxp(a, y, z))-+P(c0, 9, a)), new co F Vz(Va)((a)v a(a, c1, 2))->p(c0, C1, a)), new cl F(a)(v(a)v(xp(a, c1, a))->p(c0, C1, C2), new C2 T (V(v(a)Vz(a, c1, z)) Fpc T(Vr)(v(r)vxo(a, c1, z)) T v(co)V zy(co, c1, z)) T al(co) T 3xp(co, C1, z) Figure 4: Tableau proof 4. Prove or disprove the following statements. If it is false, a counterexample should be described (9 marks) a){A→B,B→C,=C} (3 marks (b)彐x(o(x)→v(x)→(xo(x)→彐(x) (c)3.cVyVw(o(a/)Vv),3rVy(Vzv v). where o and ol are any formulas with free variables a, yand z. w is a variable not appearing in and y (3 marks Solution. (a) The tableau is show in Figure 5.(2 ks)As it is contradictory, so ac- e assertion Is d (1 mark (b) The tableau is show in Figure 6. As it is noncontradictory, so the sentence is not valid. (2 marks) Along the left path, we can construct a counterexample. Let A=co, c1,o {co},=0 (c) There are free variables. It should be transformed into its -closure form as Vz rvyVw(o(e, y, w)v v(a, y, a))-3rvy(Vap(a, y, a)Vv (a, y, a)).(1 mark) The tableau is shown in Figure 7. It is contradictory. So it is valid.(2 marks) 5. Give two sentences a= 3x(P(a)>Q)and B=(VrP(a)Q) (a) Prove that B a in semantics approach (b) Prove it by using tableau proof (2 marks (c) If a is free in Q, discuss the truth of the following assertion 3r(P(a),Q(r))H (Va P()+Q(a)). If is wrong, you should give a counterexample (3 marks
F ∀x∀y∀z((∀x)(ψ(x) ∨ (∃zφ(x, y, z)) → φ(x, y, z)) F ∀y∀z((∀x)(ψ(x) ∨ (∃zφ(x, y, z)) → φ(c0, y, z)), new c0 F ∀z((∀x)(ψ(x) ∨ (∃zφ(x, c1, z)) → φ(c0, c1, z)), new c1 F (∀x)(ψ(x) ∨ (∃zφ(x, c1, z)) → φ(c0, c1, c2), new c2 T (∀x)(ψ(x) ∨ (∃zφ(x, c1, z)) F φ(c0, c1, c2) T (∀x)(ψ(x) ∨ (∃zφ(x, c1, z)) T ψ(c0) ∨ (∃zφ(c0, c1, z)) T ψ(c0) T ∃zφ(c0, c1, z) . . . Figure 4: Tableau proof 4. Prove or disprove the following statements. If it is false, a counterexample should be described: (9 marks) (a) {A → B, B → C, ¬C} |= ¬A. (3 marks) (b) ∃x(ϕ(x) → ψ(x)) → (∃xϕ(x) → ∃xψ(x)). (3 marks) (c) ∃x∀y∀w(ϕ(z/w) ∨ ψ) → ∃x∀y(∀zϕ ∨ ψ). where ϕ and ψ are any formulas with free variables x, yand z. w is a variable not appearing in ϕ and ψ. (3 marks) Solution. (a) The tableau is show in Figure 5.(2 marks) As it is contradictory, so according to soundness theorem, the assertion is valid.(1 mark) (b) The tableau is show in Figure 6.As it is noncontradictory, so the sentence is not valid.(2 marks) Along the left path, we can construct a counterexample. Let A = {c0, c1}, ϕ = {c0}, ψ = ∅. (c) There are free variables. It should be transformed into its ∀-closure form as ∀z(∃x∀y∀w(ϕ(x, y, w)∨ ψ(x, y, z)) → ∃x∀y(∀zϕ(x, y, z)∨ψ(x, y, z))).(1 mark) The tableau is shown in Figure 7. It is contradictory. So it is valid. (2 marks) 5. Give two sentences α = ∃x(P(x) → Q) and β = (∀xP(x) → Q). (9 marks) (a) Prove that β |= α in semantics approach. (4 marks) (b) Prove it by using tableau proof. (2 marks) (c) If x is free in Q, discuss the truth of the following assertion ∃x(P(x) → Q(x)) ⊢ (∀xP(x) → Q(x)). If is wrong, you should give a counterexample. (3 marks) 4
T A T-C F C TB→C FB TC TA→B⑧ FAT B 5: Tableau of 4.( a) Solution.(a) If Va P(r) Q is true, then Var P() is false or Q is true. (1 mark) If Va P(r)is false, there is at least a ground term t make P(t) false. We have -P(t)or Q(1 mark)So there is a ground term t make P(t),Q(1 mark) Finally we have r(P(x)→Q)(1mark (b) We first give the tableau proof as Figure8. The tableau is contradictory. It means BHa. By soundness theorem, we have BEa (c There is a formula. It is to prove 3 r(P()Q())H Vr(va P(a)>Q(a).(I mark Its tableau proof is given in Figure 9.(1 mark) The right branch is noncontradictory. We can construct a model A with A=co, C1, P=co, C1, Q=c1 such that A make the assertion wrong. (1 mark 6. Construct a set of sentences S subject to the following properties (5 marks (a) Every finite subset of S has only finite model (b)It has only infinite model (3 marks You should prove why the property holds.(Hints: there is no size limit on S) Solution. Define a sentence as n=3c1..in A11.(1 m (a)Consider any finite subset Si=oil, .. oin], where i1 N, which can't be satisfied. So the model can only be infinite.(2 marks)
F ¬A T A T ¬C F C T B → C F B T C T A → B ⊗ F A T B ⊗ ⊗ Figure 5: Tableau of 4.(a) Solution. (a) If ∀xP(x) → Q is true, then ∀xP(x) is false or Q is true.(1 mark) If ∀xP(x) is false, there is at least a ground term t make P(t) false. We have ¬P(t) or Q.(1 mark) So there is a ground term t make P(t) → Q.(1 mark) Finally we have ∃x(P(x) → Q).(1 mark) (b) We first give the tableau proof as Figure 8. The tableau is contradictory. It means β ⊢ α. By soundness theorem, we have β |= α. (c) There is a formula. It is to prove ∃x(P(x) → Q(x)) ⊢ ∀x(∀xP(x) → Q(x)). (1 mark) Its tableau proof is given in Figure 9. (1 mark) The right branch is noncontradictory. We can construct a model A with A = {c0, c1}, P = {c0, c1}, Q = {c1} such that A make the assertion wrong. (1 mark) 6. Construct a set of sentences S subject to the following properties: (5 marks) (a) Every finite subset of S has only finite model. (2 marks) (b) It has only infinite model. (3 marks) You should prove why the property holds. (Hints: there is no size limit on S.) Solution. Define a sentence as ϕn = ∃x1 . . . ∃xn ∧ 1≤i̸=j≤n ¬(xi = xj ). Then we can form a set of sentences S = {ϕi |i ≥ 1}. (1 mark) (a) Consider any finite subset Si = {ϕi1 , . . . , ϕik }, where i1 N, which can’t be satisfied. So the model can only be infinite. (2 marks) 5
F彐r(o(x)→v(x))→(彐ro(x)→v(x) T彐x(o(x)→v(x) F彐ro(x) T彐ro(x) F彐x(x) T彐ro(x) T o(co), new constant co T彐x(o(x)→v(x) T o(c1)v(c1), new constant c1 Fo(c1) F彐rp(x) Fw(c1) F v(c1) Figure 6: Tableau of 4.(b) 7. Given a language L, T is the theory and o is a sentence of L. T is finitely satisfiable if every finite subset of T is satisfiable. Answer the following question (a) If T is finitely satisfiable, prove that either TUo or TU no is finite satisfiable (4 marks) (b)If T is general, prove or disprove the result in(a) (2 marks Solution. (a) Suppose that TU o is not finitely satisfiable. (1 mark) Then, there is a finite A C Tsuch that A FT.(1 mark) We claim that TU o is finitely satisfiable Let∑ be a finite subset of t. Because△u∑ is satisfiable and△U∑-,∑U{o is satisfiable. (2 mark) Thus TU( o is finitely satisfiable (b)Given a general T, if T is satisfiable, then its every finite subset is also satisfiable. (1 mark)Then it also holds. (1 mark 8. In 1977 it was proved that every planar map can be colored with four colors(Of course there are only finite countries on map). If two countries are adjacent, they must be colore with two different colors
F ∃x(ϕ(x) → ψ(x)) → (∃xϕ(x) → ∃xψ(x)) T ∃x(ϕ(x) → ψ(x)) F ∃xϕ(x) → ∃xψ(x) T ∃xϕ(x) F ∃xψ(x) T ∃xϕ(x) T ϕ(c0), new constant c0 T ∃x(ϕ(x) → ψ(x)) T ϕ(c1) → ψ(c1), new constant c1 F ϕ(c1) T ψ(c1) F ∃xψ(x) F ψ(c1) ⊗ F ∃xψ(x) F ψ(c1) . . . Figure 6: Tableau of 4.(b) 7. Given a language L, T is the theory and ϕ is a sentence of L. T is finitely satisfiable if every finite subset of T is satisfiable. Answer the following question: (6 marks) (a) If T is finitely satisfiable, prove that either T ∪ {ϕ} or T ∪ {¬ϕ} is finite satisfiable. (4 marks) (b) If T is general, prove or disprove the result in (a). (2 marks) Solution. (a) Suppose that T ∪ {ϕ} is not finitely satisfiable.(1 mark) Then, there is a finite ∆ ⊂ T such that ∆ |= T. (1 mark) We claim that T ∪{¬ϕ} is finitely satisfiable. Let Σ be a finite subset of T. Because ∆ ∪ Σ is satisfiable and ∆ ∪ Σ |= ¬ϕ, Σ ∪ {ϕ} is satisfiable.(2 mark) Thus T ∪ {¬ϕ} is finitely satisfiable. (b) Given a general T, if T is satisfiable, then its every finite subset is also satisfiable.(1 mark) Then it also holds.(1 mark) 8. In 1977 it was proved that every planar map can be colored with four colors(Of course there are only finite countries on map). If two countries are adjacent, they must be colored with two different colors. 6
Generally, a planar map can be modeled as a planar graph. Every country is a member of vertices (u1, u2,..., if two countries vi and u; are adjacent, then there is a edge(ui, Uj) between them. Answer the following questions (9 marks (a) Formalize 4-clolorable problem with predicate logic sentences marks (b) Prove that an infinite map can be still colored with four colors Solution. This is only a reference solution. There are many describing approaches. A grap can be represented as GE (a) Let co, C1, C2, c3 be constant to represent 4 colors. (a, c) means a is colored with c.(l mark)E(a, y) means vertices a and y has a edge. is a set of sentences like E(Ui,Ui),vi, UjEV.(1 mark)We can formulate a graph which is 4-colorable with the following sentences i. 1= Va(P(a, co)v P(, c1)v P(a, c2)v P(, c3)). It means that every vertex can be colored with one of 4 colors. (1 mark i.=Vx(∧si≠j≤3-(P(x,C)AP(x,c). A vertex can only be colored with one color. (1 mark i.3= V.iVy(E(x,y)→-(∧o≤κ<3-(P(x,c1)∧P(3,cG)). It means if two vertex are adjacent, they cannot be colored with the same color. (1 mark) (b)2=EUla1, 2, 03) is an infinite set.(1 mark) Consider any finite subset Eo. We an extract vertices Vo from it and construct a set s which describe the graph Go generated by Vo (1 mark) For every finite subgraph is 4-colorable, S is satisfiable Eo must be satisfiable. (I mark) According to compactness theorem, E is satisfiable which means the graph is 4-colorable. (1 mark
Generally, a planar map can be modeled as a planar graph. Every country is a member of vertices {v1, v2, . . .}, if two countries vi and vj are adjacent, then there is a edge (vi , vj ) between them. Answer the following questions. (9 marks) (a) Formalize 4-clolorable problem with predicate logic sentences. (5 marks) (b) Prove that an infinite map can be still colored with four colors. (4 marks) Solution. This is only a reference solution. There are many describing approaches. A grap can be represented as G =. (a) Let c0, c1, c2, c3 be constant to represent 4 colors. ϕ(x, c) means x is colored with c. (1 mark) E(x, y) means vertices x and y has a edge. E is a set of sentences like E(vi , vj ), vi , vj ∈ V . (1 mark) We can formulate a graph which is 4-colorable with the following sentences: i. ψ1 = ∀x(P(x, c0) ∨ P(x, c1) ∨ P(x, c2) ∨ P(x, c3)). It means that every vertex can be colored with one of 4 colors. (1 mark) ii. ψ2 = ∀x( ∧ 0≤i̸=j≤3 ¬(P(x, ci) ∧ P(x, cj )). A vertex can only be colored with one color.(1 mark) iii. ψ3 = ∀x∀y(E(x, y) → ¬( ∧ 0≤i≤3 ¬(P(x, ci) ∧ P(y, ci)))). It means if two vertex are adjacent, they cannot be colored with the same color.(1 mark) (b) Σ = E ∪ {ψ1, ψ2, ψ3} is an infinite set. (1 mark) Consider any finite subset Σ0. We can extract vertices V0 from it and construct a set S which describe the graph G0 generated by V0.(1 mark) For every finite subgraph is 4-colorable, S is satisfiable. Σ0 must be satisfiable. (1 mark) According to compactness theorem, Σ is satisfiable which means the graph is 4-colorable. (1 mark) 7
F VzrVyVw(o(a, y, w)Vv(a, y, a))->3. Vy (Vzo(a, y, 2)Vy(, y, a))) F彐 roy Vu(叭(x,y,t)∨v(x,y,co)→彐rvy(zo(x,y,z)Vp(x,y,co), new constant co T 3xVyVw(o(a, y, a)Vy(a, y, co)) F 3rvy(Vap(a, y, a)Vv(a, y, co)) T 3cVyVu(o(c, y, w)V v(a, g, co)) T Vyw(o(c1, y, w)V a(c1, y, co)), new constant Cl F 3rvy(Vap(a, y, a)Vv(a, y, co)) F Vy (Vzo(c1, 3, 2)Vy(c1, y, co)) F Vzo(c1, c2, z)V(c1, c2, co), new constant c2 F V2o(c1, c2, 2) F v(c1, C2, co) F Vzo(c1, c2, z) Fo(C1, C2, C3), new constant C3 T VyVu(o(c1, y, w)V a(c1, y, co)) T Vw(o(c1, c2, w)V a(cl, c2, co)) T o(c1, C2, c3)Vv(c T o(c1, c2, c3) T w(c1, c2, co) Figure 7: Tableau of 4.(c
F ∀z(∃x∀y∀w(ϕ(x, y, w) ∨ ψ(x, y, z)) → ∃x∀y(∀zϕ(x, y, z) ∨ ψ(x, y, z))) F ∃x∀y∀w(ϕ(x, y, w) ∨ ψ(x, y, c0)) → ∃x∀y(∀zϕ(x, y, z) ∨ ψ(x, y, c0)), new constant c0 T ∃x∀y∀w(ϕ(x, y, w) ∨ ψ(x, y, c0)) F ∃x∀y(∀zϕ(x, y, z) ∨ ψ(x, y, c0)) T ∃x∀y∀w(ϕ(x, y, w) ∨ ψ(x, y, c0)) T ∀y∀w(ϕ(c1, y, w) ∨ ψ(c1, y, c0)), new constant c1 F ∃x∀y(∀zϕ(x, y, z) ∨ ψ(x, y, c0)) F ∀y(∀zϕ(c1, y, z) ∨ ψ(c1, y, c0)) F ∀zϕ(c1, c2, z) ∨ ψ(c1, c2, c0), new constant c2 F ∀zϕ(c1, c2, z) F ψ(c1, c2, c0) F ∀zϕ(c1, c2, z) F ϕ(c1, c2, c3), new constant c3 T ∀y∀w(ϕ(c1, y, w) ∨ ψ(c1, y, c0)) T ∀w(ϕ(c1, c2, w) ∨ ψ(c1, c2, c0)) T ϕ(c1, c2, c3) ∨ ψ(c1, c2, c0) T ϕ(c1, c2, c3) T ψ(c1, c2, c0) ⊗ ⊗ Figure 7: Tableau of 4.(c) 8
Fr(P(x)→Q) Q F P(c), new constant c F彐x(P(x)→Q) F彐r(P(x)→Q) F P(t)>Q, for a ground term t P(c) T P(t) T P(c) F Q F Q Figure 8: Tableau proof of 5.(b) Fvr(vrP(x)→Q(x)) F Vc P(a)Q(co), new constant co T Va P(az) Q(co) T丑x(P(x)→Q(x) T P(c1))Q(c1), new constant cI F P(c1) T Q(c1) VaP(r) Var P() T P(c1) T P(co) F proof of 5.(c)
F ∃x(P(x) → Q) T ∀xP(x) → Q F ∀xP(x) T Q F P(c), new constant c F ∃x(P(x) → Q) F P(c) → Q T P(c) F Q ⊗ F ∃x(P(x) → Q) F P(t) → Q, for a ground term t T P(t) F Q ⊗ Figure 8: Tableau proof of 5.(b) F ∀x(∀xP(x) → Q(x)) F ∀xP(x) → Q(c0), new constant c0 T ∀xP(x) F Q(c0) T ∃x(P(x) → Q(x)) T P(c1) → Q(c1), new constant c1 F P(c1) T Q(c1) T ∀xP(x) T P(c1) ⊗ T ∀xP(x) T P(c0) . . . Figure 9: Tableau proof of 5.(c) 9