Discrete Mathematics(ID) Spring 2013 Lecture 14: Tableau proof of predicate logic 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 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 (Var)p(ar)= 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(a)p(a) F(a)p(a) F rp(a) T(V)p(r) T(t) Fp(c) Fp(t) T y(c) for any ground fo term t of Lc constant c term t of Lo constant c Figure 1: Atomic Tableaux with Quantifiers V-style and the other two 3-style According to the definition of truth of Vxy(), 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 e need treat it specially when we define what entry is reduced. It will be introduced late Definition 1. We define tableaux as binary trees labeled with signed sentence(of Lc) called entries by indi action 1. All atomic tableau are tableaux. The requirement that c be new in Cases 7b and 8a here simply means that c is one of the constants ci added on to L to get Cc(which therefore does not appear in pDiscrete Mathematics (II) Spring 2013 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. Definition 1. We define tableaux as binary trees labeled with signed sentence( of LC) called entries by induction. 1. All atomic tableaux are tableaux. The requirement that c be new in Cases 7b and 8a here simply means that c is one of the constants ci added on to L to get LC(which therefore does not appear in φ ). 1