复旦大学：《离散数学》习题课讲义（李弋）13 Atomic tableaux Tableau proof Property of CST

Discrete mathematics Software school Fudan University May28,2013

. . Discrete Mathematics Yi Li Software School Fudan University May 28, 2013 Yi Li (Fudan University) Discrete Mathematics May 28, 2013 1 / 24

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

Review Semantics: Meaning and Truth Structure Relation between Predicate Logic and Propositional Logic Some Application Yi Li (Fudan University) Discrete Mathematics May 28, 2013 2 / 24

utline o Atomic tableaux Tableau proof ● Property of CsT

Outline Atomic tableaux Tableau proof Property of CST Yi Li (Fudan University) Discrete Mathematics May 28, 2013 3 / 24

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

Tableaux Signed sentence Entries of a tableaux How to deal with quantifiers? Yi Li (Fudan University) Discrete Mathematics May 28, 2013 4 / 24

Truth Definition(Truth The truth of a sentence p of L in a structure A in which every a E A is named by a ground term of l is defined by induction

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 May 28, 2013 5 / 24

Truth Definition(Truth The truth of a sentence p of L in a structure A in which every a E A is named by a ground term of l is defined by induction A=彐vg(y)分 for some ground term t,AFg(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 May 28, 2013 5 / 24

Truth Definition(Truth The truth of a sentence p of L in a structure A in which every a E A is named by a ground term of l is defined by induction AH Evo(v)+ for some ground term t, AFp(t) AEVvo(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 May 28, 2013 5 / 24

Quantifiers: Atomic Tableaux AF=彐vyp(v)兮 for some ground term t,A=y(t) T(彐x)y2(x) Tplc) 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 May 28, 2013 6 / 24

Quantifiers: Atomic Tableaux AH Vvo(v)+ for all ground term t, AFp(t) T(Vxp(x) 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 May 28, 2013 7 / 24

Quantifiers: Atomic Tableaux F(Vxp(X F(xp(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 May 28, 2013 8 / 24