国防科学技术大学：《数理逻辑》（英文版）Lecture 5 Predicate Calculus

Logic in Computer Science An Introductory Course for Master Students Wang j iwang@nudt.edu.cn Lecture 5 Predicate Calculus Logic in Computer Science- p 1/23

Logic in Computer Science An Introductory Course for Master Students Wang Ji jiwang@nudt.edu.cn Lecture 5 Predicate Calculus Logic in Computer Science – p.1/23

FORMAL LANGUAGE Logic in Computer Science- p 2/23

Formal Language Logic in Computer Science – p.2/23

The need for a richer language In P, it is not possible to express assertions about elements of a structure First Order logic is a considerably richer logic than propositional logic, but yet enjoys many nice mathematical properties Logic in Computer Science - p 3/23

The need for a richer language • In P, it is not possible to express assertions about elements of a structure. • First Order Logic is a considerably richer logic than propositional logic, but yet enjoys many nice mathematical properties. Logic in Computer Science – p.3/23

Primitive Symbols of F mproper symbols:(),N,V,V Variables Individual variables: 9,2 Function variables: fm,9', h' ropositional variables:p, g, r, Predicate variables: Pn, Qm, R Constants Individual constants Function constants Propositional constants Predicate constants Logic in Computer Science- p 4/23

Primitive Symbols of F Improper symbols : (, ), ∼, ∨, ∀ Variables Individual variables : x, y, z, · · · Function variables : f n, gn, hn, · · · Propositional variables : p, q, r, · · · Predicate variables : Pn, Qn, Rn, · · · Constants Individual constants Function constants Propositional constants Predicate constants Logic in Computer Science – p.4/23

Terms The terms of f are defined inductively by the following formation rules Each individual variable or constant is a term 2. If t1, .. tn are terms and fm is an n-ary function variable or constant, then f'ti,..., tn is a term Q: Formulate the definition of the set of terms rinciple ot Induction the construction of a term Logic in Computer Science - p 5/23

Terms The terms of F are defined inductively by the following formation rules: 1. Each individual variable or constant is a term. 2. If t1, · · · ,tn are terms and f n is an n-ary function variable or constant, then f nt1, · · · ,tn is a term. Q: Formulate the definition of the set of terms. Q: Principle of Induction the Construction of a term. Logic in Computer Science – p.5/23

Wifs The wffs of f are defined inductively by the following formation rules If t1, ... tn are terms and pn is an n-ary redicate variable or constant then pn (t1, .. tr )is a wff. Also each propositional variable or constant is wff.(Wffs of these forms are called atomic wffs) 2. If A is a wff, so is( 3. If A and B are wffs, So is(AV B 4. f a is a wff and is an individual variable then (Va A)is a wff. (wff A is the scope of va) Q: Formulate the definition of the set of wffs Q: Principle of Induction the Construction of ar wffee-p.6/23

Wffs The wffs of F are defined inductively by the following formation rules: 1. If t1, · · · ,tn are terms and Pn is an n-ary predicate variable or constant, then Pn(t1, · · · ,tn) is a wff. Also each propositional variable or constant is wff. (Wffs of these forms are called atomic wffs) 2. If A is a wff, so is (∼ A) 3. If A and B are wffs, so is (A ∨ B) 4. If A is a wff and x is an individual variable, then (∀xA) is a wff. (wff A is the scope of ∀x) Q: Formulate the definition of the set of wffs. Q: Principle of Induction the Construction of a wff. Logic in Computer Science – p.6/23

abbreviations 彐 A stands for~Wx~A (Va E S)A stands for Va (s(a2 a (丑c∈S) A stands for3x(S(x)∧A) Logic in Computer Science - p 7/23

Abbreviations • ∃xA stands fo r ∼ ∀ x ∼ A • ( ∀ x ∈ S ) A stands fo r ∀ x ( S ( x ) ⊃ A ) • ( ∃ x ∈ S ) A stands fo r ∃ x ( S ( x ) ∧ A ) Logic in Computer Science – p.7/23

Free and bound 1. The well formed(wf) parts of b are the consecutive subformulas of B(including B itself) Which are wffs 2. An occurrence of a variable x in a wff b is bound iff it is in a wf part of b of the form VaC. otherwise it is free 3. The bound/ free varibles of a wff are those which have bound/ free occurrences in a wff (at different occurrences) 4. a wff without free individual variables is said to be a closed wff 5. A sentence is a wff without free variables of any type Logic in Computer Science -p 8/23

Free and Bound 1. The well formed(wf) parts of B are the consecutive subformulas of B(including B itself) which are wffs. 2. An occurrence of a variable x in a wff B is bound iff it is in a wf part of B of the form ∀xC; otherwise, it is free. 3. The bound / free varibles of a wff are those which have bound / free occurrences in a wff (at different occurrences). 4. A wff without free individual variables is said to be a closed wff. 5. A sentence is a wff without free variables of any type. Logic in Computer Science – p.8/23

Substitution Let e be s 1.0(A)=St. tn A if A is atomic. (the result of simultaneously substituting ti for wi for Kn at all) 2.6(~B)=~(B) 3. 0(BVC)=0(B)VAC) 4.6xB)= VcA(B ∈{x1 t1,…,t;-1,t b if a Logic in Computer Science - p 9/23

Substitution Let θ be Sx1,···,xn t1,···,tn . 1. θ(A) = Sx1,···,xn t1,···,tn A if A is atomic. (the result of simultaneously substituting ti for xi for 1 ≤ i ≤ n at all) 2. θ(∼ B) =∼ θ(B) 3. θ(B ∨ C) = θ(B) ∨ θ(C) 4. θ(∀xB) =  ∀xθ(B) if y 6∈ {x1, · · · , xn} ∀xSx1,···,xi−1,xi+1,···,xn t1,···,ti−1,ti+1,···,tn B if x = xi Logic in Computer Science – p.9/23

Substitution Let e be s a1, 1.6(A) A if A i if a is AifA=p(1≤i≤m) atomic 2.6(~B)=~B(B 3. A(BVC=A(B)Va(C) 4.6B)=(B) Logic in Computer Science-p.10/23

Substitution Let θ be Sp1,···,pn A1,···,An . 1. θ(A) =  A if A 6∈ {p1, · · · , pn} Ai if A = pi(1 ≤ i ≤ n) if A is atomic. 2. θ(∼ B) =∼ θ(B) 3. θ(B ∨ C) = θ(B) ∨ θ(C) 4. θ(∀xB) = ∀xθ(B) Logic in Computer Science – p.10/23