复旦大学：《离散数学 Discrete Mathematics》英文讲稿_09 Deduction from premises Compactness Applications

Discrete mathematics Yi li Software sc Fudan unive April 24, 2012

Discrete Mathematics Yi Li Software School Fudan University April 24, 2012 Yi Li (Fudan University) Discrete Mathematics April 24, 2012 1 / 25

Review Soundness o Completeness

Review Soundness Completeness Yi Li (Fudan University) Discrete Mathematics April 24, 2012 2 / 25

utline o Deduction from premises o Compactness Applications

Outline Deduction from premises Compactness Applications Yi Li (Fudan University) Discrete Mathematics April 24, 2012 3 / 25

C onsequence Definition Let 2 be a(possibly infinite)set of propositions. We say that o is a consequence of 2(and write as 2h o) if, 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 24, 2012 4 / 25

C onsequence am dle oLet∑={A,=AVB}, we have∑hB oLet={A,A→B}, we have∑hB oLet∑={-A}, we have∑(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 24, 2012 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 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

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