Discrete Mathematics(Il) Spring 2012 Lecture 14: Tableau proof of predicate logic Lecturer. YiL 1 Overview n this lecture, we will show you how to prove the validity of sentences of predicate logic ndle quantifiers, we introduce new atomic tableau. In this lecture, we focus on how to handle quantifiers 2 Atomic tableau In predicate logic, we have introduced variables and two quantifiers 3 and V. All sentences without quantifiers are handled in the same way as propositions in propositional logic, we just consider the cases with quantifiers As we have done in propositional logic, we introduce the atomic tableaux according to their se- mantics. In previous lecture, we already have -(Vr)p(a)=x)mp(ar). We have the following new tomic tableaux as in Figure 1. For convenience, we call the tableaux with" for all ground term t T(V)p(a) F(r)p(a) F r)p( T(Va)p(a) Tφ(t) Fo(c Fp(t) for any ground for a new for any ground term t of Lc constant c term t of c tant c Figure 1: Atomic Tableaux with Quantifiers V-style and the other two 3-style. According to the definition of truth of Vr(a), all elements in domain of a given structure should be referred as a witness. For V-style, we use for any ground term t. However, once we fix it for some special element in a domain in a tableau, it can not name some others. Then we must duplicate the reducing node in order to guarantee that we can make sure every ground term is its witness We need treat it specially when we define what entry is reduced. It will be introduced late For 3-style, we always introduce new constant which does not occur before along the path which it is in. If the constant is not new to this language, it should name a specified element. So when different structure is concerned, c could not just be that witness. However, if it is a new constant it can be interpreted as your wish. Then we would not be in trouble in this way. Simply, we can relax to a constant is not in current tableauDiscrete Mathematics (II) Spring 2012 Lecture 14: Tableau Proof of Predicate Logic Lecturer: Yi Li 1 Overview In this lecture, we will show you how to prove the validity of sentences of predicate logic. To handle quantifiers, we introduce new atomic tableau. In this lecture, we focus on how to handle quantifiers. 2 Atomic tableau In predicate logic, we have introduced variables and two quantifiers ∃ and ∀. All sentences without quantifiers are handled in the same way as propositions in propositional logic, we just consider the cases with quantifiers. As we have done in propositional logic, we introduce the atomic tableaux according to their se￾mantics. In previous lecture, we already have ¬(∀x)ϕ(x) ≡ (∃x)¬ϕ(x).We have the following new atomic tableaux as in Figure 1. For convenience, we call the tableaux with ”for all ground term t” T (∀x)ϕ(x) T ϕ(t) for any ground term t of LC F (∀x)ϕ(x) F ϕ(c) for a new constant c F (∃x)ϕ(x) F ϕ(t) for any ground term t of LC T (∀x)ϕ(x) T ϕ(c) for a new constant c Figure 1: Atomic Tableaux with Quantifiers ∀-style and the other two ∃-style. According to the definition of truth of ∀xϕ(x), all elements in domain of a given structure should be referred as a witness. For ∀-style, we use for any ground term t. However, once we fix it for some special element in a domain in a tableau, it can not name some others. Then we must duplicate the reducing node in order to guarantee that we can make sure every ground term is its witness. We need treat it specially when we define what entry is reduced. It will be introduced late. For ∃-style, we always introduce new constant which does not occur before along the path which it is in. If the constant is not new to this language, it should name a specified element. So when different structure is concerned, c could not just be that witness. However, if it is a new constant, it can be interpreted as your wish. Then we would not be in trouble in this way. Simply, we can relax to a constant is not in current tableau. 1