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