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