Discrete mathematics Software school Fudan University April 23, 2013
. . Discrete Mathematics Yi Li Software School Fudan University April 23, 2013 Yi Li (Fudan University) Discrete Mathematics April 23, 2013 1 / 25
Review o Soundness o Completeness
Review Soundness Completeness Yi Li (Fudan University) Discrete Mathematics April 23, 2013 2 / 25
utline o Deduction from premises o Compactness Applications
Outline Deduction from premises Compactness Applications Yi Li (Fudan University) Discrete Mathematics April 23, 2013 3 / 25
C onsequence Definition Let 2 be a(possibly infinite)set of propositions. We say that o is a consequence of∑( and write as∑ha), for any valuation v (D()= T for allT∈∑)→()=T
Consequence . Definition . . Let Σ be a (possibly infinite) set of propositions. We say that σ is a consequence of Σ (and write as Σ |= σ) if, for any valuation V, (V(τ ) = T for all τ ∈ Σ) ⇒ V(σ) = T. Yi Li (Fudan University) Discrete Mathematics April 23, 2013 4 / 25
C onsequence am dle oLet∑={A,=AVB}, we have∑hB oLet∑={A,A→B}, we have∑hB o Let 2={-A}, we have∑h(A→B)
Consequence . Example . . 1. Let Σ = {A, ¬A ∨ B}, we have Σ |= B. 2. Let Σ = {A, A → B}, we have Σ |= B. 3. Let Σ = {¬A}, we have Σ |= (A → B). Yi Li (Fudan University) Discrete Mathematics April 23, 2013 5 / 25
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
Completeness of deduction from premises Theorem If a is consequence of a set 2 of premises, then there is a tableau deduction of a from∑,ie.,∑a→∑卜a
Completeness of deduction from premises . Theorem . . If α is consequence of a set Σ of premises, then there is a tableau deduction of α from Σ, i.e., Σ ⊨ α ⇒ Σ ⊢ α. Yi Li (Fudan University) Discrete Mathematics April 23, 2013 10 / 25