Discrete Mathematics(II) Spring 2013 Lecture 7: Tableau proof system 1 Overview In last lecture, we have defined consequence, the relationship between a proposition and a set of propositions, on side of semantics. we prove the validity of a proposition semantically, according to truth table. This lecture will consider how to prove the validity of a tautology. But the validity would be guaranteed in the next lecture 2 Atomic tableaux For a given proposition, we can guess it true or false. In order to show our guess, we just associate it with a sign T or F in front of it. A string like Fa and Ta is called signed proposition In preceding lectures, we have known that a compound proposition is constructed by some simpler ones and the truth valuation between them must obey truth table. Because of the Adequacy Theorem, all connective function can be represent by ,A, V. For convenience, there are totall five connectives in proposition logic We first figure out 12 atomic tableaux according to truth table as shown in Figure 1. We just take (a-B)as the example. If a truth valuation V make(a-B)true, we must have either a is false or B is true. Otherwise, we have a true or B false simultaneously. Vividly, we can use a branch to represent“ or"and a chain to represent“both…and With these atomic tableaux, we can expand a given proposition with a sign following this way Definition 1(Tableaux). A finite tableau is a binary tree, labeled with signed propositions called entries. such that 1. All atomic tableaux are finite tableaux 2. If T is a finite tableau, P a path on T,E an entry of T occurring on P and It is obtained from T by adjoining the unique atomic tableau with root entry e to t at the end of the path P, then /T is also a finite tableau If To, T1,..., Tn,... is a(finite or infinite) sequence of the finite tableaux such that, for each n 0, Tn+1 is constructed from Tn by an application of(2), then T= UTn is a tableau Example 1. A tableau with the signed proposition F(((a-B)v(va))A(avB)) In order to characterize a tableaux, we define the following terms Definition 2. Let t be a tableau, P a path on T and e an entry occurring on P.Discrete Mathematics (II) Spring 2013 Lecture 7: Tableau Proof System Lecturer: Yi Li 1 Overview In last lecture, we have defined consequence, the relationship between a proposition and a set of propositions, on side of semantics. we prove the validity of a proposition semantically, according to truth table. This lecture will consider how to prove the validity of a tautology. But the validity would be guaranteed in the next lecture. 2 Atomic tableaux For a given proposition, we can guess it true or false. In order to show our guess, we just associate it with a sign T or F in front of it. A string like F α and T α is called signed proposition. In preceding lectures, we have known that a compound proposition is constructed by some simpler ones and the truth valuation between them must obey truth table. Because of the Adequacy Theorem, all connective function can be represent by {¬, ∧, ∨}. For convenience, there are totally five connectives in proposition logic. We first figure out 12 atomic tableaux according to truth table as shown in Figure 1. We just take (α → β) as the example. If a truth valuation V make (α → β) true, we must have either α is false or β is true. Otherwise, we have α true or β false simultaneously. Vividly, we can use a branch to represent “or” and a chain to represent “both ... and ...”. With these atomic tableaux, we can expand a given proposition with a sign following this way: Definition 1 (Tableaux). A finite tableau is a binary tree, labeled with signed propositions called entries, such that: 1. All atomic tableaux are finite tableaux. 2. If τ is a finite tableau, P a path on τ , E an entry of τ occurring on P and ′τ is obtained from τ by adjoining the unique atomic tableau with root entry E to τ at the end of the path P, then ′τ is also a finite tableau. If τ0, τ1, . . . , τn, . . . is a (finite or infinite) sequence of the finite tableaux such that, for each n ≥ 0, τn+1 is constructed from τn by an application of (2), then τ = ∪τn is a tableau. Example 1. A tableau with the signed proposition F(((α → β) ∨ (γ ∨ δ)) ∧ (α ∨ β)). In order to characterize a tableaux, we define the following terms: Definition 2. Let τ be a tableau, P a path on τ and E an entry occurring on P. 1