Example 1. Is the sentence y(R(y, y)VP(, y))AVaR(a, r)) invalid? Solution. If a sentence op is invalid, then mop must be valid. So we can have the tableau proof in gure T y(R(y, y)v P(y, y))A VaR(r, a)) T Ey(R(, y)vP(y, y)) V r(e T GR(co, co)V P(co, co)), new constant co VcR(a T R(co, co) T-R(co, co) T P(co, co) F R(c T R(t1, t1) T VaR(a, r) T R(t2, t2) re 1: An example of au proof The tableau is not contradictory. So the sentence is not invalid. We can construct a model along the non-contradictory path. Let domain A=co, t1, t2, R=I(co, co), (t1, t1),(t2, t2), P=(co, co)1 This is a model of the sentence Here, we should be careful about the termination of a tableau proof. In practice, we always reduce B-style first if possible and try to leads contradiction by reducing V-style. The detail argument of when the proof is terminable. Please refer to the phrase in our text book on the page 115 bele 4 Size of model Given a language L, we can construct a model A(structure) which interprets constants, functions, and predicates. As we have shown that L could have infinite constants, which means L is infinite and A is also infiniteExample 1. Is the sentence (∃y(¬R(y, y) ∨ P(y, y)) ∧ ∀xR(x, x)) invalid? Solution. If a sentence φ is invalid, then ¬φ must be valid. So we can have the tableau proof in figure 1. T (∃y(¬R(y, y) ∨ P(y, y)) ∧ ∀xR(x, x)) T ∃y(¬R(y, y) ∨ P(y, y)) T ∀xR(x, x) T (¬R(c0, c0) ∨ P(c0, c0)), new constant c0 T ∀xR(x, x) T R(c0, c0) T ¬R(c0, c0) T P(c0, c0) F R(c0, c0) ⊗ T ∀xR(x, x) T R(t1, t1) T ∀xR(x, x) T R(t2, t2) . . . Figure 1: An example of tableau proof The tableau is not contradictory. So the sentence is not invalid. We can construct a model along the non-contradictory path. Let domain A = {c0, t1, t2}, R = {(c0, c0),(t1, t1),(t2, t2)}, P = {(c0, c0)}. This is a model of the sentence. Here, we should be careful about the termination of a tableau proof. In practice, we always reduce ∃-style first if possible and try to leads contradiction by reducing ∀-style. The detail argument of when the proof is terminable. Please refer to the phrase in our text book on the page 115 below Figure 33. 4 Size of model Given a language L, we can construct a model A(structure) which interprets constants, functions, and predicates. As we have shown that L could have infinite constants, which means L is infinite and A is also infinite. 3