复旦大学：《离散数学 Discrete Mathematics》英文讲稿_13 Atomic tableaux Tableau proof Property of CST

Discrete mathematics Yi Li Software School Fudan University June5,2012

Discrete Mathematics Yi Li Software School Fudan University June 5, 2012 Yi Li (Fudan University) Discrete Mathematics June 5, 2012 1 / 25

Review Semantics: Meaning and Truth Structure o Relation between Predicate Logic and Propositional OgIC Some Application

Review Semantics: Meaning and Truth Structure Relation between Predicate Logic and Propositional Logic Some Application Yi Li (Fudan University) Discrete Mathematics June 5, 2012 2 / 25

utline Atomic tableaux Tableau proof o Property of cst

Outline Atomic tableaux Tableau proof Property of CST Yi Li (Fudan University) Discrete Mathematics June 5, 2012 3 / 25

Tableaux Signed sentence o Entries of a tableaux o How to deal with quantifiers?

Tableaux Signed sentence Entries of a tableaux How to deal with quantifiers? Yi Li (Fudan University) Discrete Mathematics June 5, 2012 4 / 25

Truth efinition(Truth The truth of a sentence yp of L in a structure A in which every a E A is named by a ground term of L is defined by induction ●AF3vg(v)兮 for some ground term t,Ag(t) O AHVvp(v)+ for all ground term t, AFp(t)

Truth Definition (Truth) The truth of a sentence ϕ of L in a structure A in which every a ∈ A is named by a ground term of L is defined by induction. 7 A |= ∃vϕ(v ) ⇔ for some ground term t, A |= ϕ(t). 8 A |= ∀vϕ(v ) ⇔ for all ground term t, A |= ϕ(t). Yi Li (Fudan University) Discrete Mathematics June 5, 2012 5 / 25

Quantifiers: Atomic Tableaux AFavp(v)+ for some ground term t, AFp(t) 7(彐x)y( T( for a new constant c

Quantifiers: Atomic Tableaux A |= ∃vϕ(v ) ⇔ for some ground term t, A |= ϕ(t). T(∃x)ϕ(x) Tϕ(c) for a new constant c Yi Li (Fudan University) Discrete Mathematics June 5, 2012 6 / 25

Quantifiers: Atomic Tableaux AVp(v)+ for all ground term t, AFp(t) T(Vxp( for any ground term t of cc

Quantifiers: Atomic Tableaux A |= ∀vϕ(v ) ⇔ for all ground term t, A |= ϕ(t). T(∀x)ϕ(x) Tϕ(t) for any ground term t of LC Yi Li (Fudan University) Discrete Mathematics June 5, 2012 7 / 25

Quantifiers: Atomic Tableaux F(xp(x) F(彐x)y(x) for a new constant c for any ground term t of lc

Quantifiers: Atomic Tableaux F(∀x)ϕ(x) Fϕ(c) for a new constant c F(∃x)ϕ(x) Fϕ(t) for any ground term t of LC Yi Li (Fudan University) Discrete Mathematics June 5, 2012 8 / 25

Tableaux: definition We define tableaux as binary trees labeled with signed sentence( of Cc) called entries by induction Base step All atomic tableaux are tableaux o In cases 7b and 8a, c is new simply means that c is one of the constants c; added on to l to get Cc(which therefore does not appear in p

Tableaux: definition We define tableaux as binary trees labeled with signed sentence( of LC) called entries by induction. Base step: All atomic tableaux are tableaux. In cases 7b and 8a, c is new simply means that c is one of the constants ci added on to L to get LC(which therefore does not appear in ϕ ). Yi Li (Fudan University) Discrete Mathematics June 5, 2012 9 / 25

Tableaux: definition Induction step if T is a finite tableau, P a path on t, e and entry of T occurring on P TI is obtained from T by adjoining an atomic tableau with root entry e to t at the end of the path P, then Tl is also a tableau o Here the requirement that c be new in Case 7b and Ba means that it is one of the ci that do not appear in any entries on P o In actual practice it is simpler in terms of bookkeeping to choose one not appearing at any nod ot t

Tableaux: definition Induction step: if τ is a finite tableau, P a path on τ , E and entry of τ occurring on P. τ ′ is obtained from τ by adjoining an atomic tableau with root entry E to τ at the end of the path P, then τ ′ is also a tableau. Here the requirement that c be new in Case 7b and 8a means that it is one of the ci that do not appear in any entries on P. In actual practice it is simpler in terms of bookkeeping to choose one not appearing at any nod of τ . Yi Li (Fudan University) Discrete Mathematics June 5, 2012 10 / 25