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 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 Improper symbols : (, ), , _, 8 Variables Individual variables : x;y;z; Function variables : f n ;g n ;h n ; Propositional variables : p;q;r; Predicate variables : P n ;Q n ;R n ; Constants Individual constants Function constants Propositional constants Predicate constants Logic in Computer Science { p.4/23 Terms The terms of F are de ned inductively by the following formation rules: 1. Each individual variable or constant is a term. 2. If t 1 ; ;t n are terms and f n is an n-ary function variable or constant, then f n t 1 ; ;t n is a term. Q: Formulate the de nition of the set of terms. Q: Principle of Induction the Construction of a term. Logic in Computer Science { p.5/23 W s The w s of F are de ned inductively by the following formation rules: 1. If t 1 ; ;t n are terms and P n is an n-ary predicate variable or constant, then P n (t 1 ; ;t n ) is a w . Also each propositional variable or constant is w . (W s of these forms are called atomic w s) 2. If A is a w , so is ( A) 3. If A and B are w s, so is (A_B) 4. If A is a w and x is an individual variable, then (8xA) is a w . (w A is the scope of 8x) Q: Formulate the de nition of the set of w s. Q: Principle of Induction the Construction of a w . Logic in Computer Science { p.6/23 Abbreviations 9xA stands for 8x A (8x 2 S)A stands for 8x(S(x) A) (9x 2 S)A stands for 9x(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 w s. 2. An occurrence of a variable x in a w B is bound i it is in a wf part of B of the form 8xC; otherwise, it is free. 3. The bound / free varibles of a w are those which have bound / free occurrences in a w (at di erent occurrences). 4. A w without free individual variables is said to be a closed w . 5. A sentence is a w without free variables of any type. Logic in Computer Science { p.8/23 Substitution Let be S x 1 ; ;x n t 1 ; ;t n . 1. (A) = S x 1 ; ;x n t 1 ; ;t n A if A is atomic. (the result of simultaneously substituting t i for x i for 1 i n at all) 2. ( B) = (B) 3. (B_C) = (B) _ (C) 4. (8xB) = 8 < : 8x (B) if y 62 fx 1 ; ;x n g 8xS x 1 ; ;x i 1 ;x i+1 ; ;x n t 1 ; ;t i 1 ;t i+1 ; ;t n B if x = x i Logic in Computer Science { p.9/23 Substitution Let be S p 1 ; ;p n A 1 ; ;A n . 1. (A) = 8 < : A if A 62 fp 1 ; ;p n g A i if A = p i (1 i n) if A is atomic. 2. ( B) = (B) 3. (B_C) = (B) _ (C) 4. (8xB) = 8x (B) Logic in Computer Science { p.10/23 t is free for x in A t is free for x in A i no free occurrence of x in A is in a wf part of A of the form 8yB, where y is free variable of t. C is free for p in A i no occurrence of p in A is in a wf part of A of the form 8yB, where y is free variable of C. Logic in Computer Science { p.11/23 Unique Readability De ne a function K on the symbols such that for a symbol s, K(s) = 1 n, where n is the number of terms which must follow s to obtain a term. K(s) = 1 for individual variables or constants K(s) = 1 n for n-ary function variables or constants Extend K to the set of strings by K(s 1 s n ) = K(s 1 ) + +K(s n ) Logic in Computer Science { p.12/23 Unique Readability for Terms 1. For any term t, K(t) = 1 2. Any terminal segment of a term is a concatenation of one or more terms. 3. No proper initial segment of a term is itself a term. 4. The set of terms is freely generated from the set of individual variables and constants by the F f operations. Logic in Computer Science { p.13/23 Unique Readability for W s K(() = 1 K()) = 1 K(8) = 1 K( ) = 0 K(_) = 1 K(P) = 1 n for n-ary predicate variables or constants. 1. For any w A, K(A) = 1 2. For any proper initial segment A 0 of a w A, K(A 0 ) < 1. 3. No proper initial segment of a w is itself a w . 4. The set of w s is freely generated from the set of atomic w s by the the operations , _ and 8. Logic in Computer Science { p.14/23 First Order Theory The elementary theory of additive abelian group G1 8x(x = x) G2 8x8y8z(x = y (x = z y = z)) G3 8x8y8z(x = y x+z = y +z) G4 8x8y8z(x+ (y +z) = (x+y) +z) G5 8x(x+ 0 = x) G6 8x9y(x+y = 0) G7 8x8y(x+y = y +x) Logic in Computer Science { p.15/23 Proof Theory Logic in Computer Science { p.16/23 Axiom Schemata for F Axiom Schema 1 A_A A Axiom Schema 2 A (B_A) Axiom Schema 3 A B (C _A (B _C)) Axiom Schema 4 8xA S x t A where t is a term free for the individual variable x in A Axiom Schema 5 8x(A_B) (A_8xB) provided that x is not free in A Logic in Computer Science { p.17/23 Rules of Inference Modus Ponens (MP) A; A B B Generalization (Gen) A 8xA Logic in Computer Science { p.18/23 Proof A proof in F of a w A is a nite sequence A 1 ;A 2 ; ;A m of w s such that A m is A and for each j(1 j m) at least one the following conditions is satis ed: 1. A j is an axiom; 2. A j is inferred by MP from w s A i and A k , where i<j and k<j; 3. A j is inferred by Gen from A i where i<j. Logic in Computer Science { p.19/23 ‘ ‘A i A has a proof in F. If ‘ P A, then ‘ F A. Logic in Computer Science { p.20/23 Tautologous De nition The w A is a substitution instance of a tautology, or is tautologous i these is a tautology B(of P) such that A = S p 1 p n C1 C n B Rule P 1. If A is tautologous then ‘A. 2. If ‘ A 1 ; ‘ A n , and if A 1 ^ ^A n B is tautologous, then ‘B. Logic in Computer Science { p.21/23 Let (A) be the result of erasing all quanti ers in A and replacing each occurrence of an atomic w in A by the propositional variable p. 1. If A is atomic, (A) = p 2. ( A) = (A) 3. (A_B) = (A) _ (B) 4. (8xA) = (A) Logic in Computer Science { p.22/23 Consistency of E Lemma If ‘A, then j= P (A). Consistency Theorem F is absolutely consistent and consistent with respect to negation. Logic in Computer Science { p.23/23