Deductions from premises How to construct CsT from premises Definition(Tableaux from premises) Let 2 be(possibly infinite)set of propositions. We define the finite tableaux with premises from 2 by induction: | t is a finite tableau from∑anda∈∑, then the tableau formed by putting Ta at the end of every noncontradictory path not containing it is also a finite tableau from∑
Deductions from Premises How to construct CST from premises? . Definition (Tableaux from premises) . . Let Σ be (possibly infinite) set of propositions. We define the finite tableaux with premises from Σ by induction: 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 Σ. Yi Li (Fudan University) Discrete Mathematics April 23, 2013 6 / 25
Tableau proof Definition 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 2 and write it as ∑卜a
Tableau proof . Definition . . 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 Σ ⊢ α. Yi Li (Fudan University) Discrete Mathematics April 23, 2013 7 / 25
Property of CST Theorem Every CST from a set of premises is finished
Property of CST . Theorem . .Every CST from a set of premises is finished. Yi Li (Fudan University) Discrete Mathematics April 23, 2013 8 / 25
Soundness of deductions from premises 「 Theorem If there is a tableau proof of a from a set of premises 2 then a is a consequence of∑,ie.∑}a→∑ha
Soundness of deductions from premises . Theorem . . If there is a tableau proof of α from a set of premises Σ, then α is a consequence of Σ, i.e. Σ ⊢ α ⇒ Σ ⊨ α. Yi Li (Fudan University) Discrete Mathematics April 23, 2013 9 / 25