Logic in Computer Science An Introductory Course for Master Students Wang j iwang@nudt.edu.cn Lecture 7 Prenex normal form Logic in Computer Science-p. 1 /9
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
The primitive symbols of are those of f, plus the symbol 3. The formation Rules of 8 are those of F plus the following If b is a wff of and a is an individual variable then彐 cB is a wff of8 The axiom schemata of are those of f plus 彐cA三~Wm~A Logic in Computer Science-p. 2/9
E The primitive symbols of E are those of F, plus the symbol ∃. The formation Rules of E are those of F, plus the following • If B is a wff of E and x is an individual variable, then ∃xB is a wff of E. The axiom schemata of E are those of F plus ∃xA ≡∼ ∀x ∼ A Logic in Computer Science – p.2/9
Concepts An occurrence of a quantifier Vc or d.c is vacuous if its variable has no free occurrence n its scope i i occurs positively/negatively in a iff EiiC is a positive/negative wf part of A Logic in Computer Science-p. 3/9
Concepts • An occurrence of a quantifier ∀x or ∃x is vacuous if its variable x has no free occurrence in its scope. • ∃∀ixi occurs positively /negatively in A iff ∃∀ixiC is a positive /negative wf part of A. Logic in Computer Science – p.3/9
Prenex normal form A wff a of 8 is in prenex normal form iff 1. no vacuous quantifier occurs in A, and 2. no quantifier 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 wff A of E is in prenex normal form iff 1. no vacuous quantifier occurs in A, and 2. no quantifier 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 wff A in prenex normal form is of the form nwnm B Where 1. B is quantifier free 2.玉∈{V,}(1≤≤m)andx1,…, an are distinct individual variables 3. For each 1<i<nm. occurs in B Logic in Computer Science-p.5/9
Prenex Normal Form A wff A in prenex normal form is of the form ∃∀1x1 · · · ∃∀nxnB where 1. B is quantifier free. 2. ∃∀i ∈ {∀, ∃}(1 ≤ i ≤ n) and x1, · · · , xn are distinct individual variables. 3. For each 1 ≤ i ≤ n, xi occurs in B. Logic in Computer Science – p.5/9