Logic in Computer Science An Introductory Course for Master Students Wang Ji jiwang@nudt.edu.cn Lecture 7 Prenex Normal Form Logic in Computer Science { p.1/9 E The primitive symbols of E are those of F, plus the symbol 9. The formation Rules of E are those of F, plus the following If B is a w of E and x is an individual variable, then 9xB is a w of E. The axiom schemata of E are those of F plus 9xA 8x A Logic in Computer Science { p.2/9 Concepts An occurrence of a quanti er 8x or 9x is vacuous if its variable x has no free occurrence in its scope. 98 i x i occurs positively /negatively in A i 98 i x i C is a positive /negative wf part of A. Logic in Computer Science { p.3/9 Prenex Normal Form A w A of E is in prenex normal form i 1. no vacuous quanti er occurs in A, and 2. no quanti er in A occurs in the scope of a propositional connective of A. If B is in prenex normal form such that ‘ A B, we shall say that B is a prenex normal form of A. Logic in Computer Science { p.4/9 Prenex Normal Form A w A in prenex normal form is of the form 98 1 x 1 98 n x n B where 1. B is quanti er free. 2. 98 i 2 f8;9g(1 i n) and x 1 ; ; x n are distinct individual variables. 3. For each 1 i n, x i occurs in B. Logic in Computer Science { p.5/9 Recti ed W s A w A is recti ed i 1. A contains no vacuous quanti er. 2. No variable occurs both bound and free in A. 3. No two quanti er-occurrences in A bind the same variable. A w in prenex normal form must be recti ed. Logic in Computer Science { p.6/9 Compute prenex normal form Let the quanti ers in A be 98 1 x 1 ; ;98 n x n be in the left-to-right order in which they occur in A. The prenex normal form of A\is" Q 1 x 1 Q n x n B where 1. B is the w obtained from A by erasing all quanti ers of A. 2. For 1 i n, Logic in Computer Science { p.7/9 Compute prenex normal form Q i x i = 8 < : 98 i x i if 98 i x i occurs positively in A ~ 98 i x i if 98 i x i occurs negatively in A where ~ 98 i = 8 < : 9 if 98 i = 8 8 if 98 i = 9 Logic in Computer Science { p.8/9 Prenex Normal Form Theorem 1. Every w has a prenex normal form. 2. If A is a recti ed w and B is the prenex normal form of A, then ‘ A B. Proof Sketch: By induction on n 98 . Logic in Computer Science { p.9/9