Logic in Computer Science An Introductory Course for Master Students Wang j iwang@nudt.edu.cn Lecture 10 Logic in Computer Science- p 1/21
Logic in Computer Science An Introductory Course for Master Students Wang Ji jiwang@nudt.edu.cn Lecture 10 Logic in Computer Science – p.1/21
COMPLETENSS Logic in Computer Science- p 2/21
Completenss Logic in Computer Science – p.2/21
Two forms of Completeness Theorem Let i be a set of wffs. The following parts are equivalent If r a then Th A Ifr is consistent thent is satisfiable Logic in Computer Science - p 3/21
Two forms of Completeness Theorem Let Γ be a set of wffs. The following parts are equivalent. • If Γ |= A then Γ ` A • If Γ is consistent, then Γ is satisfiable. Logic in Computer Science – p.3/21
Sequence of consistent sets of wifs Partially ordered Set a relation on a set s is called partial ordering or partial order if it is reflexive antisymmetric and transitive a set together with a partial ordering r is called a partially ordered set, or poset Totally Ordered Set If is a poset and every two elements of s are comparable s is called a totally ordered set or linearly ordered set. a totally ordered set is also called a chain Lemma Let S 2C(). If is a totally ordered set, and for any TE s, t is consistent hen U s is consistent Logic in Computer Science- p 4/21
Sequence of consistent sets of wffs Partially Ordered Set A relation on a set S is called partial ordering or partial order if it is reflexive, antisymmetric and transitive. A set S together with a partial ordering R is called a partially ordered set, or poset. Totally Ordered Set If is a poset and every two elements of S are comparable, S is called a totally ordered set or linearly ordered set. A totally ordered set is also called a chain. Lemma Let S ⊆ 2L(F). If is a totally ordered set, and for any Γ ∈ S, Γ is consistent, then S S is consistent. Logic in Computer Science – p.4/21
Existence of consistent and maximal set Theorem LetiCl()be consistent. There existsT'EL()such that r∈I",and 2,T is consistent and maximal Zorn's Lemma Let s be a nonempty set such that for any chain Z cs, the set UZE S. Then there is a m e s which is maximal in the sense that it is not a subset of any other element of Logic in Computer Science - p 5/21
Existence of consistent and maximal set Theorem Let Γ ⊆ L(F) be consistent. There exists Γ0 ∈ L(F) such that 1. Γ ⊆ Γ0, and 2. Γ0 is consistent and maximal. Zorn’s Lemma Let S be a nonempty set such that for any chain Z ⊆ S, the set S Z ∈ S. Then there is a m ∈ S which is maximal in the sense that it is not a subset of any other element of S. Logic in Computer Science – p.5/21
Expansion Let i and o be two first order systems 1. If L(FuCL(2), then we say that F2 is an expansion of Fi 2. If L(FCc(F2), then we say that F2 is a proper expansion of F1 3. 2 is an expansion of i iff every constant of F1 is a constant ya Logic in Computer Science p 6/21
Expansion Let F1 and F2 be two first order systems. 1. If L(F1) ⊆ L(F2), then we say that F2 is an expansion of F1. 2. If L(F1) ⊂ L(F2), then we say that F2 is a proper expansion of F1. 3. F2 is an expansion of F1 iff every constant of F1 is a constant F2. Logic in Computer Science – p.6/21
Extension Let i and o be two first order systems T1≌C(万1)andI2SC(F2) 1. If L(FiCC(F2)and Th(F1∪n1)sTh(2∪I2, then we say that F2ur2 is an extension of flury 2. If for every A L(Fi), Iihr A iff T2 HF, A then we say that F2Ur2 is a conservative extension of fFiUr1 Logic in Computer Science p 7/21
Extension Let F1 and F2 be two first order systems. Γ1 ⊆ L(F1) and Γ2 ⊆ L(F2). 1. If L(F1) ⊆ L(F2) and Th(F1 S Γ1) ⊆ Th(F2 S Γ2), then we say that F2 S Γ2 is an extension of F1 S Γ1. 2. If for every A ∈ L(F1), Γ1 `F1 A iff Γ2 `F2 A, then we say that F2 S Γ2 is a conservative extension of F1 S Γ1. Logic in Computer Science – p.7/21
Expansion and Extension 1. If 2 is an expansion of fi, then Th(Fi)c Th(F2) 2.f2UI2 is a conservative extension of升1∪I1, en Th(F1∪I)=Th(F2∪I2)nC(1) Logic in Computer Science - p 8/21
Expansion and Extension 1. If F2 is an expansion of F1, then Th(F1) ⊆ Th(F2). 2. If F2 S Γ2 is a conservative extension of F1 S Γ1, then Th(F1 ∪ Γ1) = Th(F2 ∪ Γ2) ∩ L(F1) Logic in Computer Science – p.8/21
Expansion, Extension and Consistency 1.f2∪2 is a conservative extension of万1UI1, then fiuli is consistent iff f2ut2 is consistent 2. Let Fi and 2 be formulations of f, so that 2 is an expansion of fi obtained by adding additional individual constants to the set of constants of F1. Let CC(i, Then (a) fur is a conservative extension of FlUr, an (b) FiUr is consistent iff F2Ur is consistent Logic in Computer Science - p 9/21
Expansion, Extension and Consistency 1. If F2 S Γ2 is a conservative extension of F1 S Γ1, then F1 S Γ1 is consistent iff F2 S Γ2 is consistent. 2. Let F1 and F2 be formulations of F, so that F2 is an expansion of F1 obtained by adding additional individual constants to the set of constants of F1. Let Γ ⊆ L(F1), Then (a) F2 S Γ is a conservative extension of F1 S Γ, and (b) F1 S Γ is consistent iff F2 S Γ is consistent. Logic in Computer Science – p.9/21
Frugal Interpretation An interpretation D, Lo> for is said to be frugal#D≤#C(F) An interpretation I is said to be a frugal model of r if it is a frugal interpretation of t Logic in Computer Science - p10/21
Frugal Interpretation • An interpretation for F is said to be frugal iff #D ≤ #L(F). • An interpretation I is said to be a frugal model of Γ if it is a frugal interpretation of Γ. Logic in Computer Science – p.10/21