Discrete Mathematics(ID) Spring 2012 Lecture 9: Deduction from Premises, Compactness, and Applications Lecturer. yil 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 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 luse a set of premises is introduced, we should define a new type of tableau proof system to le the premises If a is a consequence of 2, then any v satisfing 2 should also make a true. The problem can be simplified by considering the case when ai E 2. Then, we can introduce a proposition ai into tableau in the form of ta Definition 1(Tableaux from premises). Let 2 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 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. If T is a finite tableau from 2,P a path in 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 the end of the ath P, then /T is also a finite tableau from 2 厅0,,rn,…,isa( finite or infinite) sequence of finite tableaux 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 2 Similarly, we can redefine tableau proof as following 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∑a To CST, we have the following propertyDiscrete Mathematics (II) Spring 2012 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 satisfing Σ 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 0τ is obtained from τ by adjoining the unique atomic tableau with root entry E to the end of the path P, then 0τ 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 Σ ` α. To CST, we have the following property. 1