Axiom.pdf

1

Propositional Logic - Axioms and Inference Rules

Axioms Axiom 1.1 [Commutativity] (p ∧ q) (p ∨ q) (p = q)

= = =

(q ∧ p) (q ∨ p) (q = p)

Axiom 1.2 [Associativity] p ∧ (q ∧ r) p ∨ (q ∨ r)

= =

(p ∧ q) ∧ r (p ∨ q) ∨ r

Axiom 1.3 [Distributivity] p ∨ (q ∧ r) p ∧ (q ∨ r)

= =

(p ∨ q) ∧ (p ∨ r) (p ∧ q) ∨ (p ∧ r)

Axiom 1.4 [De Morgan] ¬(p ∧ q) ¬(p ∨ q)

¬p ∨ ¬q ¬p ∧ ¬q

= =

Axiom 1.5 [Negation] ¬¬p

=

p

Axiom 1.6 [Excluded Middle] p ∨ ¬p

=

T

1

Axiom 1.7 [Contradiction] p ∧ ¬p

=

F

Axiom 1.8 [Implication] p ⇒ q

=

¬p ∨ q

Axiom 1.9 [Equality] (p = q)

=

(p ⇒ q) ∧ (q ⇒ p)

Axiom 1.10 [or-simplification] p ∨ p p ∨ T p ∨ F p ∨ (p ∧ q)

= = = =

p T p p

Axiom 1.11 [and-simplification] p ∧ p p ∧ T p ∧ F p ∧ (p ∨ q)

= = = =

p p F p

Axiom 1.12 [Identity] p

=

p

2

Inference Rules p1 = p2 , p2 = p3 p1 = p3

Transitivity

p1 = p2 E(p1 ) = E(p2 ) , E(p2 ) = E(p1 )

Substitution

q1 , q2 , . . . , qn , q1 ∧ q2 ∧ . . . ∧ qn ⇒ (p1 = p2 ) E(p1 ) = E(p2 ) , E(p2 ) = E(p1 )

3

Conditional Substitution

2

Propositional Logic - Derived Theorems

Equivalence and Truth Theorem 2.1 [Associativity of = ] ((p = q) = r)

=

(p = (q = r))

Theorem 2.2 [Identity of = ] (T = p)

=

p

Theorem 2.3 [Truth] T

Negation, Inequivalence, and False Theorem 2.4 [Definition of F ] F

=

¬T

Theorem 2.5 [Distributivity of ¬ over = ] ¬(p = q) (¬p = q)

= =

(¬p = q) (p = ¬q)

Theorem 2.6 [Negation of F ] ¬F

=

T

4

Theorem 2.7 [Definition of ¬] (¬p = p) ¬p

= =

F (p = F )

Disjunction Theorem 2.8 [Distributivity of ∨ over = ] (p ∨ (q = r)) ((p ∨ (q = r)) = (p ∨ q))

= =

((p ∨ q) = (p ∨ r)) (p ∨ r)

Theorem 2.9 [Distributivity of ∨ over ∨ ] p ∨ (q ∨ r) = (p ∨ q) ∨ (p ∨ r)

Conjunction Theorem 2.10 [Mutual definition of ∧ and ∨ ] (p ∧ q) (p ∧ q) ((p ∧ q) = p) ((p ∧ q) = (p = q)) (((p ∧ q) = p) = q)

= = = = =

(p = (q = (p ∨ q))) ((p = q) = (p ∨ q)) (q = (p ∨ q)) (p ∨ q) (p ∨ q)

Theorem 2.11 [Distributivity of ∧ over ∧ ] p ∧ (q ∧ r) = (p ∧ q) ∧ (p ∧ r)

5

Theorem 2.12 [Absorption] p ∧ (¬p ∨ q) = p ∧ q p ∨ (¬p ∧ q) = p ∨ q Theorem 2.13 [Distributivity of ∧ over = ] (p ∧ q) ((p ∧ q) = (p ∧ ¬q)) p ∧ (q = p)

= = =

((p ∧ ¬q) = ¬p) ¬p (p ∧ q)

Theorem 2.14 [Replacement] (p = q) ∧ (r = p)

(p = q) ∧ (r = q)

=

Theorem 2.15 [Definition of = ] (p = q)

=

(p ∧ q) ∨ (¬p ∧ ¬q)

Theorem 2.16 [Exclusive or] ¬(p = q)

=

(¬p ∧ q) ∨ (p ∧ ¬q)

Implication Theorem 2.17 [Definition of Implication] (p ((p ⇒ q) = (p (p ((p ⇒ q) = (p

⇒ q) ∨ q)) ⇒ q) ∧ q))

= = = =

((p ∨ q) = q) q ((p ∧ q) = p) p

6

Theorem 2.18 [Contrapositive] (p ⇒ q)

=

(¬q ⇒ ¬p)

Theorem 2.19 [Distributivity of ⇒ over = ] p ⇒ (q = r)

((p ⇒ q) = (p ⇒ r))

=

Theorem 2.20 [Shunting] p ∧ q ⇒ r

=

p ⇒ (q ⇒ r)

Theorem 2.21 [Elimination/Introduction of ⇒ ] p p p p (p ∨ q)

∧ (p ⇒ q) ∧ (q ⇒ p) ∨ (p ⇒ q) ∨ (q ⇒ p) ⇒ (p ∧ q) p ⇒ F F ⇒ p

= = = = = = =

p ∧ q p T ¬q ∨ p (p = q) ¬p T

Theorem 2.22 [Right Zero of ⇒ ] (p ⇒ T )

=

T

Theorem 2.23 [Left Identity of ⇒ ] (T ⇒ p)

= p

7

Theorem 2.24 [Weakening/Strengthening] p p ∧ q p ∧ q p ∨ (q ∧ r) p ∧ q

⇒ ⇒ ⇒ ⇒ ⇒

p p p p p

∨ q ∨ q ∨ q ∧ (q ∨ r)

Theorem 2.25 [Modus Ponens] p ∧ (p ⇒ q)

⇒

q

Theorem 2.26 [Proof by Cases] (p ⇒ r) ∧ (q ⇒ r) (p ⇒ r) ∧ (¬p ⇒ r)

= =

(p ∨ q ⇒ r) r

Theorem 2.27 [Mutual Implication] (p ⇒ q) ∧ (q ⇒ p)

=

(p = q)

Theorem 2.28 [Antisymmetry] (p ⇒ q) ∧ (q ⇒ p)

⇒

(p = q)

Theorem 2.29 [Transitivity] (p ⇒ q) ∧ (q ⇒ r) (p = q) ∧ (q ⇒ r) (p ⇒ q) ∧ (q = r)

⇒ ⇒ ⇒

(p ⇒ r) (p ⇒ r) (p ⇒ r)

Theorem 2.30 [Monotonicity of ∨ ] (p ⇒ q)

⇒

(p ∨ r ⇒ q ∨ r)

8

Theorem 2.31 [Monotonicity of ∧ ] (p ⇒ q)

⇒

(p ∧ r ⇒ q ∧ r)

Substitution Theorem 2.32 [Leibniz] (e = f )

⇒

(E(e) = E(f ))

Theorem 2.33 [Substitution] (e = f ) ∧ E(e) (e = f ) ⇒ E(e) q ∧ (e = f ) ⇒ E(e)

= = =

(e = f ) ∧ E(f ) (e = f ) ⇒ E(f ) q ∧ (e = f ) ⇒ E(f )

Theorem 2.34 [Replace by T ] p ∧ E(p) p ⇒ E(p) q ∧ p ⇒ E(p)

= = =

p ∧ E(T ) p ⇒ E(T ) q ∧ p ⇒ E(T )

Theorem 2.35 [Replace by F ] p ∨ E(p) E(p) ⇒ p E(p) ⇒ p ∨ q

= = =

p ∨ E(F ) E(F ) ⇒ p E(F ) ⇒ p ∨ q

Theorem 2.36 [Shannon] E(p)

=

(p ∧ E(T )) ∨ (¬p ∧ E(F ))

9

3

Propositional Logic - Examples and Exercises

10

4

Predicate Logic - Axioms

Axiom 4.1 [Definition of ∃]   ∃i : m ≤ i < n : pi  = (m ≥ n) ⇒  F  (m < n)

⇒

∃i : m ≤ i < n : pi  =     ∃i : m ≤ i < n − 1 : pi     ∨ pn−1

     

Axiom 4.2 [Definition of ∀]   ∀i : m ≤ i < n : pi  = (m ≥ n) ⇒  T  (m < n)

⇒

∀i : m ≤ i < n : pi  =     ∀i : m ≤ i < n − 1 : p i     ∧ pn−1

11

     

Axiom 4.3 [Range Split]   (m1 ≤ m2 ≤ m3 )

⇒

  ∀i : m1 ≤ i < m2 : pi     ∧     ∀i : m ≤ i < m : p 2 3 i     = ∀i : m1 ≤ i < m3 : pi  

(m1 ≤ m2 ) ∧ (n1 ≥ n2 )

⇒

  ∀i : m1 ≤ i < n1 : pi     ∧     ∀i : m2 ≤ i < n2 : pi     = ∀i : m1 ≤ i < n1 : pi  

(m1 ≤ m2 ≤ m3 )

⇒

  ∃i : m1 ≤ i < m2 : pi     ∨     ∃i : m ≤ i < m : p 2 3 i     = ∃i : m1 ≤ i < m3 : pi  

(m1 ≤ m2 ) ∧ (n1 ≥ n2 )

⇒

  ∃i : m1 ≤ i < n1 : pi     ∨     ∃i : m ≤ i < n : p 2 2 i     = ∃i : m1 ≤ i < n1 : pi

Axiom 4.4 [Interchange of Dummies] ∀i : m1 ≤ i < n1 : (∀j : m2 ≤ j < n2 : pi,j ) = ∀j : m2 ≤ j < n2 : (∀i : m1 ≤ i < n1 : pi,j ) ∃i : m1 ≤ i < n1 : (∃j : m2 ≤ j < n2 : pi,j ) = ∃j : m2 ≤ j < n2 : (∃i : m1 ≤ i < n1 : pi,j )

12

Axiom 4.5 [Dummy Renaming] ∀i : m ≤ i < n : pi = ∀j : m ≤ j < n : pj Axiom 4.6 [Distributivity of ∨ over ∀ ] (p ∨ (∀i : m ≤ i < n : qi )) = ∀i : m ≤ i < n : (p ∨ qi ) Axiom 4.7 [Distributivity of ∧ over ∀ ]   p ∧ (∀i : m ≤ i < n : qi )  = (m < n) ⇒  ∀i : m ≤ i < n : p ∧ qi 

 ∀i : m ≤ i < n : pi   ∧ ∀i : m ≤ i < n : qi

=

∀i : m ≤ i < n : (pi ∧ qi )

Axiom 4.8 [Distributivity of ∧ over ∃ ] (p ∧ (∃i : m ≤ i < n : qi )) = ∃i : m ≤ i < n : (p ∧ qi ) Axiom 4.9 [Distributivity of ∨ over ∃ ]   p ∨ (∃i : m ≤ i < n : qi )  = (m < n) ⇒  ∃i : m ≤ i < n : (p ∨ qi ) 

 ∃i : m ≤ i < n : pi   ∨ ∃i : m ≤ i < n : qi

=

∃i : m ≤ i < n : (pi ∨ qi )

Axiom 4.10 [Universality of T ] ∀i : m ≤ i < n : T = T

13

Axiom 4.11 [Existence of F ] ∃i : m ≤ i < n : F = F Axiom 4.12 [Generalized De Morgan] ¬ (∃i : m ≤ i < n : pi ) ¬ (∀i : m ≤ i < n : pi )

= =

∀i : m ≤ i < n : ¬pi ∃i : m ≤ i < n : ¬pi

Axiom 4.13 [Trading] (m ≤ i < n) ⇒ pi (m ≤ i < n) ∧ pi

= ⇒

∀i : m ≤ i < n : pi ∃i : m ≤ i < n : pi

Axiom 4.14 [Definition of Numerical Quantification]   N i : m ≤ i < n : pi  (m ≥ n) ⇒  = 0 (m < n) ∧ ¬pn−1

⇒



 N i : m ≤ i < n : pi   = N i : m ≤ i < n − 1 : pi 

(m < n) ∧ pn−1

⇒

N i : m ≤ i < n : pi  =     N i : m ≤ i < n − 1 : p i     + 1

14

     

Axiom 4.15 [Definition of Σ]   Σi : m ≤ i < n : ei  = (m ≥ n) ⇒  0  (m < n)

⇒

Σi : m ≤ i < n : ei  =     Σi : m ≤ i < n − 1 : ei     + en−1

     

Axiom 4.16 [Definition of Π]   Πi : m ≤ i < n : ei  = (m ≥ n) ⇒  1  (m < n)

⇒

Πi : m ≤ i < n : ei  =     Πi : m ≤ i < n − 1 : e i     ∗ en−1

15

     

5

Predicate Logic - Derived Theorems

Theorem 5.1 [Definition of ∃]   ∃i : m < i ≤ n : pi  = (m ≥ n) ⇒  F  (m < n)

⇒

∃i : m < i ≤ n : pi  =     ∃i : m + 1 < i ≤ n : pi     ∨ pm+1

     

Theorem 5.2 [Definition of ∀]

(m ≥ n)

⇒



 ∀i : m < i ≤ n : pi   = T 

(m < n)

⇒

∀i : m < i ≤ n : pi  =     ∀i : m + 1 < i ≤ n : p i     ∧ pm+1

16

     

Theorem 5.3 [Definition of Σ]   Σi : m < i ≤ n : ei  = (m ≥ n) ⇒  0  (m < n)

⇒

Σi : m < i ≤ n : ei  =     Σi : m + 1 < i ≤ n : ei     + em+1

     

Theorem 5.4 [Definition of Π]

(m ≥ n)

⇒



 Πi : m < i ≤ n : ei   = 1 

(m < n)

⇒

Πi : m < i ≤ n : ei  =     Πi : m + 1 < i ≤ n : e i     ∗ em+1

17

     

6

Some Simple Laws of Arithmetic

Throughout this compendium, we assume the validity of all “simple” arithmetic rules. Examples of such rules are all simplification rules, e.g. = 2+3 = 5 x+x = 2∗x x+y−y =x (x/3) ∗ 3 = x 0∗x = 0 1∗x = x x ∗ x = x2 0x = 0 1x = 1 (2 ∗ x + 10 = 20) = (x = 5) (x + y < 2 ∗ y) = (x < y) (x + y = x + z) = (y = z) x ∗ (y + 1) − (x + z) = (x ∗ y − z) Following is a collection of theorems that might be used. The list is not exhaustive but intend to show the level of complexity that you can specify theorems on.

18

Theorems on < and ≤ (x < y) (x < y) (x < y) (x < y) (x < y) ∧ (y ≤ z) (x ≤ y) (x ≤ x) (x ≤ y) ∧ (y ≤ z) (x ≤ y) ∧ (y < z) (x ≤ y) ∧ ¬(x < y) (x ≤ y − 1) (x ≤ y) ∨ (y ≤ x) (x ≤ y) ∨ (y < x) (x ≤ y)

= ⇒ ⇒ = ⇒ = = ⇒ ⇒ ⇒ = = = =

(y > x) ¬(y = x) ∧ ¬(y < x) (x ≤ y) (x ≤ y) ∧ (x 6= y) (x < z) ¬(x > y) T (x ≤ z) (x < z) (x < y) (x < y) T T (x < y) ∨ (x = y)

Theorems on properties about + and − (x < y) (x < y + 1) (x < y) (0 < x) (x − 1 < x) (x ≤ y − 1) (x ≤ y) (x1 < y1 ) ∧ (x2 < y2 ) (x1 ≤ y1 ) ∧ (x2 ≤ y2 )

⇒ = ⇒ = = = = ⇒ ⇒

19

(x < y + 1) (x ≤ y) (z − y < z − x) (−x < 0) T (x < y) (x − 1 < y) (x1 + x2 < y1 + y2 ) (x1 + x2 ≤ y1 + y2 )

Theorems on properties about ∗ and / (0 < x) (0 < x) (0 < x) (0 ≤ x/2) (x = 0) 2 ∗ (x/2)

= = = = ⇒ =

(0 < 2 ∗ x) (x < 2 ∗ x) (x ÷ 2 < x) (0 ≤ x) (x ∗ y = 0) x

Theorems on equivalence relation (x = x) (x = y)

= =

T (x ≤ y) ∧ (y ≤ x)

Theorems about odd(n) and even(n) odd(x) even(x) odd(x + 2 ∗ y) even(x + 2 ∗ y) odd(x) odd(x) odd(x) ∧ (x = 0)

⇒ ⇒ = = = ⇒ =

((x − 1) ÷ 2 = (x − 1)/2) (x ÷ 2 = x/2) odd(x) even(x) ¬even(x) ((x ≥ 1) = (x ≥ 0)) F

20

7

Predicate Logic - Examples and Exercises

21

8 8.1

Arrays - Axioms Axioms

Axiom 8.1 [Assignment to Array Element]   (i = j) ⇒ (e = f )  ∧ ((b; i : e) [j] = f ) =  (i 6= j) ⇒ (b[j] = f ) Axiom 8.2 [Definition of Arithmetic Relations] (b[i : j] = x) (b[i : j] < x) (b[i : j] > x) (b[i : j] ≤ x) (b[i : j] ≥ x) (b[i : j] 6= x) x ∈ b[i : j]

= = = = = = =

(∀k (∀k (∀k (∀k (∀k (∀k (∃k

: : : : : : :

i≤k i≤k i≤k i≤k i≤k i≤k i≤k

<j+1 <j+1 <j+1 <j+1 <j+1 <j+1 <j+1

22

: : : : : : :

b[k] = x) b[k] < x) b[k] > x) b[k] ≤ x) b[k] ≥ x) b[k] 6= x) x = b[k])