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 24, 2012 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 24, 2012 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 24, 2012 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 24, 2012 9 / 25