国防科学技术大学：《数理逻辑》（英文版）Lecture 7 Prenex Normal Form

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

Rectified wffs a wff a is rectified iff 1. A contains no vacuous quantifier 2 No variable occurs both bound and free in a 3. No two quantifier-occurrences in a bind the same variable A wff in prenex normal form must be rectified Logic in Computer Science-p. 6/9

Rectified Wffs A wff A is rectified iff 1. A contains no vacuous quantifier. 2. No variable occurs both bound and free in A. 3. No two quantifier-occurrences in A bind the same variable. A wff in prenex normal form must be rectified. Logic in Computer Science – p.6/9

Compute prenex normal form Let the quantifiers in a be ic ,nin be in the left-to-right order in which they occur in A The prenex normal form of a" is" Q1x1… Qnanb Where 1. B is the wff obtained from a by erasing all quantifiers of A 2.For1<2<m Logic in Computer Science-p. 7/9

Compute prenex normal form Let the quantifiers in A be ∃∀1x1, · · · , ∃∀nxn be in the left-to-right order in which they occur in A. The prenex normal form of A“is” Q1x1 · · · QnxnB where 1. B is the wff obtained from A by erasing all quantifiers of A. 2. For 1 ≤ i ≤ n, Logic in Computer Science – p.7/9

Compute prenex normal form ViCi if ici occurs positively in A Hiai if ii occurs negatively in a Where 彐if玉;=V i玉;=彐 Logic in Computer Science-p. 8/9

Compute prenex normal form Qixi =  ∃∀ixi if ∃∀ixi occurs positively in A ∃˜∀ixi if ∃∀ixi occurs negatively in A where ∃ ˜ ∀i =  ∃ if ∃∀i = ∀ ∀ if ∃∀i = ∃ Logic in Computer Science – p.8/9

Prenex normal form Theorem 1. Every wff has a prenex normal form 2. f a is a rectified wff and b is the prenex normal form of A, then h a= B Proof Sketch: By induction on ny Logic in Computer Science-p. 9/9

Prenex Normal Form Theorem 1. Every wff has a prenex normal form. 2. If A is a rectified wff and B is the prenex normal form of A, then ` A ≡ B. Proof Sketch: By induction on n∃∀. Logic in Computer Science – p.9/9