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
Substitutivity of Implication D sub Let 91, W/k be a list including all distinct individual variables which occur free in m or N If M is positive in A, then 9…(M>N)(AAx 2. If M is negative in a, the en Hyr …9(M>N)(ANA 3. If M is positive in a and hMoN, then A→AN 4. If M is negative in a and hmon, then A→A Logic in Computer Science - p 6/27
Substitutivity of Implication ⊃ Sub Let y1, · · · , yk be a list including all distinct individual variables which occur free in M or N. 1. If M is positive in A, then ` ∀y1 · · · yk(M ⊃ N) ⊃ (A ⊃ AMN ) 2. If M is negative in A, then ` ∀y1 · · · yk(M ⊃ N) ⊃ (AMN ⊃ A) 3. If M is positive in A and ` M ⊃ N, then ` A ⊃ AMN 4. If M is negative in A and ` M ⊃ N, then ` AMN ⊃ A Logic in Computer Science – p.6/27
Substitutivity of Equivalence= sub 1.}y (M=N)(=AN) 2. FhM=N. then a= am 3.fHM≡Nand+A, then a Theorems 1.+x(A≡B)(A≡wB) 2.m(A≡B)(丑mA≡3xB) Logic in Computer Science - p 7/27
Substitutivity of Equivalence≡ Sub 1. ` ∀y1 · · · yk(M ≡ N) ⊃ (A ≡ AMN ) 2. If ` M ≡ N, then ` A ≡ AMN 3. If ` M ≡ N and ` A, then ` AMN Theorems 1. ` ∀x(A ≡ B) ⊃ (∀xA ≡ ∀xB) 2. ` ∀x(A ≡ B) ⊃ (∃xA ≡ ∃xB) Logic in Computer Science – p.7/27
FVrC= Vy Sa c Theorem yxc≡ySC, y, provided that y is not free in C and y is free for c in C (1)+mC→SmC AS4 (2)H V.) VySa C 3)h ySCD SSac AS4 (4)F ViSCo VaC (3)>y (5)Fp(p3q)∧(q3p)3(D≡q (6H rC=VySC Logic in Computer Science -p 8/27
` ∀xC ≡ ∀ySxyC? Theorem ` ∀xC ≡ ∀ySxy C, provided that y is not free in C and y is free for x in C. (1) ` ∀xC ⊃ Sxy C AS4 (2) ` ∀xC ⊃ ∀ySxy C (1) ⊃ ∀ (3) ` ∀ySxy C ⊃ SyxSxy C AS4 (4) ` ∀ySxy C ⊃ ∀xC (3) ⊃ ∀ (5) |=P (p ⊃ q) ∧ (q ⊃ p) ⊃ (p ≡ q) (6) ` ∀xC ≡ ∀ySxy C Logic in Computer Science – p.8/27
aB rule Let a, c be wffs and y be individual variables. If 1.y is not free in c 2. y is free for in c 3.A Then Vxc Logic in Computer Science - p 9/27
αβ Rule Let A, C be wffs and x, y be individual variables. If 1. y is not free in C 2. y is free for x in C 3. ` A Then ` A∀xC ∀ySxy C Logic in Computer Science – p.9/27
Proof from Hypotheses Let i be a finite set of wffs. a proof of a wff A from T is a finite sequence such that Logic in Computer Science-p.10/27
Proof from Hypotheses Let Γ be a finite set of wffs. A proof of a wff A from Γ is a finite sequence A0, · · · , Am such that Logic in Computer Science – p.10/27