Discrete Mathematics(II) Spring 2013 Lecture 9: Deduction from Premises, Compactness, and Applications 1 Overview In lecture 7, we introduce a tableau proof system to prove the validity of a proposition. But we should handle whether a is a logic consequence of 2 or not. Here, 2 is called a set of premises Mathematical Logic is a corner stone of modern computer science. In this lecture, we also show you how to apply propositional logic to other problems 2 Deduction from premises Because a set of premises is introduced, we should define a new type of tableau proof system to handle the premises If a is a consequence of 2, then any v satisfying 2 should also make a true roblem can be simplified by considering the case when ai E 2. Then, we can introduce a proposition ai into tableau in the form of Tai Definition 1(Tableaux from premises). Let E be(possibly infinite) set of propositions. We define the finite tableaux with premises from 2 by induction: 1. Every atomic tableau is a finite tableau from 2 If r is a finite tableau from 2 and a E 2, then the tableau formed by putting Ta at the end of every noncontradictory path not containing it is also a finite tableau from 2 3. Ift is a finite tableau from 2,p a path in T, E an entry of T occurring on P and /T is obtained from T by adjoining the unique atomic tableau with root entry e to the end of the path P, then it is also a finite tableau from 2 J0,…,,Tn,…, is a (finite or infinite) sequence of finite tableau from∑ such that, for each n≥ 0, Tn+1 is constructed from Tn by an application of(2)and(3), then T=UTn is a tableau from X y, we can redefine tableau proof as followin Definition 2. A tableau proof of a proposition a from 2 is a tableau from 2 with root entry Fa that is contradictory, that is, one in which every path is contradictory. If there is such a proof we say that a is provable from∑ and write it as∑ha. Because of 2, it is important when a ai E 2 should be introduced. generally, we can count the step m to extend a tableau. When m is even, we next just reduce a entry Otherwise Ci 2 introduced. To CSt, we have the following property.Discrete Mathematics (II) Spring 2013 Lecture 9: Deduction from Premises,Compactness, and Applications Lecturer: Yi Li 1 Overview In lecture 7, we introduce a tableau proof system to prove the validity of a proposition. But we should handle whether α is a logic consequence of Σ or not. Here, Σ is called a set of premises. Mathematical Logic is a corner stone of modern computer science. In this lecture, we also show you how to apply propositional logic to other problems. 2 Deduction from Premises Because a set of premises is introduced, we should define a new type of tableau proof system to handle the premises. If α is a consequence of Σ, then any V satisfying Σ should also make α true. The problem can be simplified by considering the case when αi ∈ Σ. Then, we can introduce a proposition αi into tableau in the form of T αi . Definition 1 (Tableaux from premises). Let Σ be (possibly infinite) set of propositions. We define the finite tableaux with premises from Σ by induction: 1. Every atomic tableau is a finite tableau from Σ 2. If τ is a finite tableau from Σ and α ∈ Σ, then the tableau formed by putting T α at the end of every noncontradictory path not containing it is also a finite tableau from Σ. 3. If τ is a finite tableau from Σ, P a path in τ , E an entry of τ occurring on P and ′τ is obtained from τ by adjoining the unique atomic tableau with root entry E to the end of the path P, then ′τ is also a finite tableau from Σ. If τ0, . . . , τn, . . . is a (finite or infinite) sequence of finite tableaux from Σ such that, for each n ≥ 0, τn+1 is constructed from τn by an application of (2) and (3), then τ = ∪τn is a tableau from Σ. Similarly, we can redefine tableau proof as following: Definition 2. A tableau proof of a proposition α from Σ is a tableau from Σ with root entry F α that is contradictory, that is, one in which every path is contradictory. If there is such a proof we say that α is provable from Σ and write it as Σ ⊢ α. Because of Σ, it is important when a αi ∈ Σ should be introduced. Generally, we can count the step m to extend a tableau. When m is even, we next just reduce a entry Otherwise αi ∈ Σ is introduced. To CST, we have the following property. 1