Logic in Computer Science An Introductory Course for Master Students Wang j iwang@nudt.edu.cn ecture Propositional Calculus( Cont'd) Logic in Computer Science- p 1/19
Logic in Computer Science An Introductory Course for Master Students Wang Ji jiwang@nudt.edu.cn Lecture 4 Propositional Calculus(Cont’d) Logic in Computer Science – p.1/19
PROPOSITIONAL CONNECTIVES Logic in Computer Science- p 2/19
Propositional Connectives Logic in Computer Science – p.2/19
Substitutivity of equivalence Let A, m and n be wffs and let an be the result replacing M by N at zero or more occurrences Henceforth called designate occurrences) of M in A 1. AN is a wff 2. IfFM=N then FA=An If H M=n then F A=An Logic in Computer Science -p 3/19
Substitutivity of Equivalence Let A,M and N be wffs and let AMN be the result of replacing M by N at zero or more occurrences (henceforth called designate occurrences) of M in A. 1. AMN is a wff. 2. If |= M ≡ N then |= A ≡ AMN . (≡ sub) If ` M ≡ N then ` A ≡ AMN Logic in Computer Science – p.3/19
Propositional connectives An n-ary truth function is a function from ples of truth values to truth values n-tuples A propositional connective is a symbol of a formalized language which in the intend interpretation, denotes a truth function How to lift a wff to be a truth function? Logic in Computer Science -p 4/19
Propositional Connectives • An n-ary truth function is a function from n-tuples of truth values to truth values. • A propositional connective is a symbol of a formalized language which, in the intend interpretation, denotes a truth function. • How to lift a wff to be a truth function? Logic in Computer Science – p.4/19
入 Abstraction If p1,... Pn are distinct propositional variables including all variables in A, let Ap1…入pn]A:{T,F}→{T,F} where 1 n)=0(A) and(p)=;forl0≤i≤m Obviously.Ap1…入pA=Ap1… n B iff A≡B Logic in Computer Science-p.5/19
λ Abstraction If p1, · · · , pn are distinct propositional variables including all variables in A, let [λp1 · · · λpn]A : {T, F}n → {T, F} where [λp1 · · · λpn]A(x1, · · · , xn) = φ(A) and φ(pi) = xi for all 0 ≤ i ≤ n. Obviously, [λp1 · · · λpn]A = [λp1 · · · λpn]B iff A ≡ B Logic in Computer Science – p.5/19
Normal form A literal is a wff of the form p or of the form a p a wff is in disjunctive normal form iff it is a disjunction of conjunctions of literals m70 ∨∧ A wff is in conjunctive normal form iff it is a conjunction of disjunctions of literals p Logic in Computer Science -p6/19
Normal Form • A literal is a wff of the form p or of the form ∼ p • A wff is in disjunctive normal form iff it is a disjunction of conjunctions of literals. _ m i=1 ^ ni j=1 pij • A wff is in conjunctive normal form iff it is a conjunction of disjunctions of literals. ^ m i=1 _ ni j=1 pij Logic in Computer Science – p.6/19
Disjunctive Normal Form Theorem 1. Let h be any truth function with n arguments where n>l, and let p1, ...,pn be distinct propositional variables. Then there is a wff a in disjunctive normal form such that h=Ap1…入nA 2. For every wff b of propositional calculus there is a wff a in disjunctive normal form such that b is equivalent A Logic in Computer Science-p. 7/19
Disjunctive Normal Form Theorem 1. Let h be any truth function with n arguments, where n ≥ 1, and let p1, · · · , pn be distinct propositional variables. Then there is a wff A in disjunctive normal form such that h = [λp1 · · · λpn]A. 2. For every wff B of propositional calculus there is a wff A in disjunctive normal form such that B is equivalent A. Logic in Computer Science – p.7/19
Completeness of Propositional Connectives A set T of propositional connectives is complete iff for each integer m> l and for each truth function h of n arguments there is a wff a in which only connectives of f occur such that h=DAp1…~pA iN,vi is complete Logic in Computer Science -p8/19
Completeness of Propositional Connectives • A set Υ of propositional connectives is complete iff for each integer n ≥ 1 and for each truth function h of n arguments, there is a wff A in which only connectives of Υ occur such that h = [λp1 · · · λpn]A • {∼,∨} is complete. Logic in Computer Science – p.8/19
Negation Normal Form A wff of propositional calculus is in negation normal form iff it contains no propositional connectives other than∧,∨Vand~, and the scope ot each occurrence ot N is a propositional variable Get nne get rid of≡and, leaving just∧,∨and 2. push negations in, using law of double negation and de le Morgan s law (AVB)≡~A∧~B (A∧B) A∨~B Logic in Computer Science-p.9/19
Negation Normal Form • A wff of propositional calculus is in negation normal form iff it contains no propositional connectives other than ∧, ∨ and ∼, and the scope of each occurrence of ∼ is a propositional variable. • Get NNF 1. get rid of ≡ and ⊃, leaving just ∧, ∨ and ∼ 2. push negations in, using law of double negation and de Morgan’s law ∼∼ A ≡ A ∼ (A ∨ B) ≡ ∼ A∧ ∼ B ∼ (A ∧ B) ≡ ∼ A∨ ∼ B Logic in Computer Science – p.9/19
Conjuncts of NNF For each wff A in negation normal form define a set C(A)of conjuncts of A by induction as follows If A is a literal, C(A=AJ If a has the form bVC, C(A=C(BUC(C If a has the form b∧C, CA)={D∧ED∈C(B)andE∈C(C Logic in Computer Science- p10/19
Conjuncts of NNF For each wff A in negation normal form, define a set C(A) of conjuncts of A by induction as follows • If A is a literal, C(A) = {A} • If A has the form B ∨ C, C(A) = C(B) ∪ C(C) • If A has the form B ∧ C, C(A) = {D ∧ E|D ∈ C(B) and E ∈ C(C)} Logic in Computer Science – p.10/19