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