Logic in Computer Science An Introductory Course for Master Students Wang j iwang@nudt.edu.cn Lecture 6 Reasoning in Predicate calculus Logic in Computer Science- p 1/27
Logic in Computer Science An Introductory Course for Master Students Wang Ji jiwang@nudt.edu.cn Lecture 6 Reasoning in Predicate Calculus Logic in Computer Science – p.1/27
Axiom Schemata for F Axiom schema1A∨A2A Axiom schema2A(B∨A) Axiom Schema 3 AOBD(CVAD(BVC) Axiom Schema 4 V xAD Si a where t is a term free for the individual variable in a Axiom Schema 5 Vr(AVB)(AvVcB) provided that a is not free in A Logic in Computer Science- p 2/27
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 ∀xA ⊃ Sxt A where t is a term free for the individual variable x in A Axiom Schema 5 ∀x(A ∨ B) ⊃ (A ∨ ∀xB) provided that x is not free in A Logic in Computer Science – p.2/27
Derived rules Trans fFA1A2,…,AnAn+,then A1→A +1 IfF A)(A15 A2) andFA)(B13 B2),then A(A1B1→A2∨B2 ∧→ A∧ BC iffF a(BC) Theorem va1…VxnA>A Logic in Computer Science - p 3/27
Derived Rules Trans If ` A1 ⊃ A2, · · · , ` An ⊃ An+1, then ` A1 ⊃ An+1. ∨ ⊃ ∨ If ` A ⊃ (A1 ⊃ A2) and ` A ⊃ (B1 ⊃ B2), then ` A ⊃ (A1 ∨ B1 ⊃ A2 ∨ B2) ∧ ⊃ ` A ∧ B ⊃ C iff ` A ⊃ (B ⊃ C) Theorem ` ∀x1 · · · ∀xnA ⊃ A Logic in Computer Science – p.3/27
If f ab and is not free in A, then had VcB (1)}+~AVB (2)+W(~A∨B) )Gen (3H Vc( avb)oo avv cb as5 (4)+A→wmB Theorem F Vr(A) B))(aA) v B) Theorem A)B)(BDo A Theorem FN ADNB2(B) A Logic in Computer Science- p 4/27
⊃ ∀ If ` A ⊃ B and x is not free in A, then ` A ⊃ ∀xB. (1) ` ∼ A ∨ B given (2) ` ∀x(∼ A ∨ B) (1)Gen (3) ` ∀x(∼ A ∨ B) ⊃∼ A ∨ ∀xB AS5 (4) ` A ⊃ ∀xB Theorem ` ∀x(A ⊃ B) ⊃ (∀xA ⊃ ∀xB) Theorem ` A ⊃ B ⊃ (∼ B ⊃∼ A) Theorem `∼ A ⊃∼ B ⊃ (B ⊃ A) Logic in Computer Science – p.4/27
Positive/ Negative Occurrence Let M be a wf part of A. an occurrence of M in A is positive/ negative in A iff that occurrence is in the scope of an even/odd number of occurrences of in a M is positive/ negative in A iff the designated occurrences of M are all positive/ negative in A Let(al,,, an+1) be a designated occurrence of M in a alvA 72+1 Logic in Computer Science - p 5/27
Positive / Negative Occurrence • Let M be a wf part of A. An occurrence of M in A is positive / negative in A iff that occurrence is in the scope of an even / odd number of occurrences of ∼ in A. • M is positive / negative in A iff the designated occurrences of M are all positive / negative in A. • Let (α1, · · · , αn+1) be a designated occurrence of M in A, AMN = α1Nα2 · · · αnNαn+1 Logic in Computer Science – p.5/27