ALADM Set Theory Cheat Sheet

(1) Notation 1 : Set Enumeration
List elements between \(\{\) and \(\}\)
eg: \(\{ 0,2,4,6,8 \}\)

(2) Notation 2: Set Comprehension
\(\{ list-of-dummies:type\ |\ Predicate\ :\ Expression \}\) yields the set of elements that result from evaluating \( E[\ list-of-dummies\ :=\ v\ ]\) in a state for each value of \(v\) in type \(t\) such that \(R[\ list-of-dummies\ :=\ v\ ]\) holds in that state.

e.g: \(\{x:\mathbb{Z}\ |\ 0 \leq x \leq 5\ :\ x+2\}\)

If E has type t, the set comprehension has a type = set-of(t)

(3) Equality of Set Enumeration and Set Comprehension

\(\{ e_0,e_1,\ldots e_n \} = \{x\ |\ x=e_0 \vee x=e_1\vee \dots \vee x=e_n\ :\ x \}\)

(4) Universe: The collection of elements from which sets are constructed is called the domain of discourse or Universe and denoted by \(\mathbb{U}\). The Universe can be thought of as the type of every *set* variable in the theory. Eg: if the universe is \(set-of(\mathbb{Z})\), then every set variable v has type \(set-of(\mathbb{Z})\)

(move this to the beginning of the EQ doc)
Propositional Calculus permits reasoning about formulae constructed from boolean variables and boolean operators. Therefore the expressiveness of the logic is restricted to sentences that can be modeled using boolean expressions.

A predicate calculus formula is a boolean expression in which some boolean variables have been replaced by
(1) predicates - applications of boolean functions whose arguments may have types other than \(\mathbb{B}\).

e.g: equal(x,y), Less-than(x,y) etc.

The *names* of such functions are called predicate symbols and maybe notated as infix where appropriate. e.g: (x > y).

The *arguments* of predicates are *expressions* whose types maybe other than \(\mathbb{B}\) and are called terms.

(2) Universal or Existential Quantifications.

In the pure predicate calculus, the function symbols are uninterpreted (except for =), so the logic provides no specific rules to manipulate them. Since function symbols are uninterpreted,

***we can develop general rules for manipulation that are sound no matter what meanings we ascribe to the function symbols. Thus the pure predicate calculus is sound in all domains that maybe of interest.***

We get a theory by adding axioms that assign meanings to some of the uninterpreted symbols.

Example 1: The theory of integers consists of the pure predicate calculus together with axioms for manipulating the operators (i.e the functions) +, - , <, > etc. These axioms state (for example) that + is commutative and has the identity 0.

Example 2: The theory of Sets consists of the pure predicate calculus together with axioms for manipulating operators like \(\in\, \cup,\cap\) etc

*The core of all such theories however is the core predicate calculus, and provides the basic machinery for reasoning about. or providing proofs about *all* domains of interest.*

Set Theory Resumes

(5) Notation: For an expression e:t and a set valued expression S:set(t)

\(e \in s \equiv \) " e is a member of s" and \(e \not \in S \equiv \neg (e \in S) \)

(6) Axiom: Set Membership

\( F \in \{x:t \mid R\ :\ E:t\} \equiv (\exists x:t \mid R\ :\ F = E) \)

(7) Axiom: Extensionality
\( S = T \equiv (\forall x:t \mid R\ \:\ x \in S \equiv x \in S)\)
Note: This converts a set comprehension into an existential quantification, at which point all the quantification laws can be applied. Existential quantifications with an equality in the Predicate can be converted into a set comprehension by going in the reverse direction.

(8) Theorem: \( \{ x \mid false : E \} = \{\} = \emptyset \)
\((\forall e,E \mid : e \in \{ x \mid false : E \} \equiv e \in \{\} \equiv false )\)

(9) Theorem: \( \{ x \mid x=e : x\} \), not-occurs-free(x,e), yields a singleton set containing the value of e

(10) Since \(\vee\) is symmetric, order of the elements in a set enumeration is irrelevant
e.g: \(\{1,3\} \equiv \{x \mid x=1 \vee x=3 : x\} \equiv \{x \mid x=3 \vee x=1 : x\}\)

(11) Since \(\vee\) is idempotent, repetition of elements in a set enumeration has no significance \(\{ 1,3,3 \} = \{ 1,3 \} \) Duplicates may arise when expressions are used to designate elements. eg:\(\{ b,c \}\) when evaluated in state where \(b \not= c \) yields two elements, but yields one element when \(b=c\).

(12) Conversion from traditional format

\(\{m^2 \mid 0 \leq m \leq 3\} = \{m \mid 0 \leq m \leq 3 : m^2\}\)

However there could be ambiguity in this conversion depending on which variables are considered bound (so dummies) and which free.

e.g \( \{x+y \mid x = y + 1\} \) could equal \( \{x \mid x = y + 1: x+y\} = \{2y + 1\}\) or \( \{y \mid x = y + 1: x+y\} = \{2x - 1\}\) or \( \{x,y \mid x = y + 1: x+y\} = \) set of odd integers

(13) Conversion to traditional format
\(\{x \mid R : E \} = \{y \mid ( \exists x \mid R : y=E) \} \)

(14) Set-Predicate Theorem
(a) \( x \in \{x \mid R \} \equiv x \in \{x \mid R : x\} \equiv R\)
(b) \( E_x \in \{x \mid R : E\} \equiv R \)
(c) \( y \in \{x \mid R \} \equiv y \in \{x \mid R : x\} \equiv R[x := y]\), not-occurs-free (y,R)
(d) \( E_y \in \{x \mid R : E\} \equiv R[x := y]\) , not-occurs-free (y,R)
(e)\( E[x := y] \in \{x \mid R : E\} \equiv R[x := y]\) , not-occurs-free (y,R)

(15) Principle of Comprehension and characteristic predicate
For each predicate R, there corresponds a set comprehension \( \{x:t \mid R : x\}\) which contains the objects in t that satisfy R

eg: consider \( R \equiv x=3 \vee x=5 \) .
The corresponding set comprehension is \( S = \{x\mid x=3 \vee x=5 :x \} \).
R is called the characteristic predicate of set comprehension S.

(16) Theorem: \(\{x \mid R\} = \{x \mid S\} \equiv (\forall x \mid : R \equiv S)\)

(17) Theorem: (\(\{x \mid R\} = \{x \mid S\}\) is valid) \(\equiv\) (\(R \equiv S\) is valid)

(18) Methods to prove that M = N
(a) Directly use Leibniz
(b) Use axiom extensionality i.e prove \((\forall x \mid : x \in M \equiv x \in N)\)
(c) Prove that \( R \equiv S \) and conclude \(\{x \mid R\} = \{x \mid S\}\)

(19) Axiom: Cardinality: \(\# S = (\sum x \mid x \in S : 1 ) \)

(20) Axiom: Subset: \( S \subseteq T \equiv (\forall x \mid x \in S : x \in T ) \)

(21) Axiom: Proper Subset: \( S \subset T \equiv (\forall x \mid x \in S : x \in T ) \wedge S \neq T \)

(22) Axiom: Superset: \( S \supseteq T \equiv T \subseteq S \)

(23) Axiom: Proper Superset: \( S \supset T \equiv T \subset S\)

(24) Axiom: Complement \( v \in S^c \equiv v \in \mathbb{U} \wedge v \notin S \)

(25) Theorem: \( v \in S^c \equiv v \notin S\) (assuming \( v \in \mathbb{U}) \)

(26) Theorem: \( S^{c^c} \equiv S \)

(27) Axiom: Union \( v \in S \cup T \equiv (v \in S) \vee (v \in T) \)

(28) Axiom: Intersection \( v \in S \cap T \equiv (v \in S) \wedge (v \in T) \)

(29) Axiom: Difference \( v \in S - T \equiv (v \in S) \wedge (v \notin T) \)

(30) Axiom: Disjoint S and T are disjoint \( \equiv S \cap T \neq \emptyset \)

(31) Axiom: \( T \in \mathcal{P}(S) \equiv T \subseteq S \)

(32) Definition of 'set expression' and 'corresponding predicate calculus expression'

A 'set expression' is an expression constructed from set variables (of type set-of(t)), \(\emptyset\), \(\mathbb{U}\) ( a universe for all set variables in question), ,Complement \(\ ^c\), union \(\cup\) and intersection \(\cap\).

Let \(E_s\) be a set expression. The 'corresponding predicate calculus expression' \(E_p\) is constructed from \(E_s\) by replacing \(\emptyset\) with false, \(\mathbb{U}\) with true, \(\ ^c\) with \(\neg\), \(\cup\) with \(\vee\), and \(\cap\) with \(\wedge\).

This construction is reversible. ie, \(E_s\) can be constructed from \(E_p\).

(33) Metatheorem For any two set expressions \(E_s\) and \(F_s\)

(a) \( E_s = F_s \) is valid \(\equiv\) \( E_p \equiv F_p \) is valid
(b) \( E_s \subseteq F_s \) is valid \(\equiv\) \( E_p \Rightarrow F_p \) is valid
(c) \( E_s = \mathbb{U} \) is valid \(\equiv\) \( E_p \) is valid

(a) + (b) + (c) + 32 mean that implications, equivalences and in general axioms and proved theorems in predicate calculus can be converted into Set Theory theorems *without proving with Set Theory proofs.

(d) Convert \( E_p \equiv E'_{p}\) to \( (E_p \Rightarrow E'_{p}) \wedge (E'_p \Rightarrow E_{p})\)
(e) Convert \( E_p \Rightarrow E'_{p}\) to \(\neg E_p \vee E'_p \)

(d) + (e) + 32 implies that any boolean expression is equivalent to some expression \(E_p\) for which \(E_p\) can be constructed. The meta theorem does not mention

(f) \(E_s - F_s\) can be rewritten as \(E_s \cap F_s^c \)

(34) The metatheorem tremendously reduces the amount of work we need to prove theorems in Set Theory. (Already proved) predicate logic theorems can be converted to Set Theory theorems by using the meta theorem.

e.g: we already proved DeMorgan's law

\(\neg(s \vee t) \equiv \neg s \wedge \neg t\)
\(\hspace{0.2 cm} = \) Applying metatheorem we get
\(( S \cup T)^c \equiv S^c \cap T^c \)

which we don't have to prove using Set Theory axioms etc.

(35) Theorem: \((\forall x \mid : P \Rightarrow Q \equiv \{x \mid P\} \subseteq \{x \mid Q\} \)


Properties of Subset

(36) Theorem: Anti-Symmetry: \( S \subseteq T \wedge T \subseteq S \equiv S = T \)

(37) Theorem: Reflexivity: \( S \subseteq S\)

(38) Theorem: Transitivity: \( S \subseteq T \wedge T \subseteq U \Rightarrow S \subseteq U \)

(39) Theorem: \( \emptyset \subseteq S\)

(40) Theorem: \( S \subset T \equiv S \subseteq T \wedge \neg (T \subseteq S) \)

(41) Theorem: \( S \subset T \equiv S \subseteq T \wedge (\exists x \mid x \in T : x \notin S)\)

(42) Theorem: \( S \subseteq T \equiv S \subset T \vee S = T \)

(43) Theorem: \( S \not\subset S\)

(44) Theorem: \( S \subset T \Rightarrow S \subseteq T \)

(45) Theorem: \( S \subset T \Rightarrow T \nsubseteq S \)

(46) Theorem: \( S \subseteq T \Rightarrow T \not\subset S \)

(47) Theorem: \( S \subseteq T \wedge \neg(U \subseteq T) \Rightarrow \neg(U \subseteq S) \)

(48) Theorem: \((\exists x \mid x \in S : x \notin T) \Rightarrow S \neq T \)

(49) Theorem: Transitivity 1: \( S \subseteq T \wedge T \subset U \Rightarrow S \subset U \)

(50) Theorem: Transitivity 1: \( S \subset T \wedge T \subseteq U \Rightarrow S \subset U \)

(51) Theorem: Transitivity 2: \( S \subset T \wedge T \subset U \Rightarrow S \subset U \)

Power Set Theorems

(52)Theorem: \(\mathcal{P}(\emptyset) = \{ \emptyset \} \)

(53) Theorem: \( S \in \mathcal{P}(S) \)

(54)Theorem: \( \# (\mathcal{P}(S)) = 2^{\#S} \) for finite S

(55) Union and Intersection as quantifiers

Union is symmetric, associative, idempotent and has an identity \( \emptyset \)

Intersection is symmetric, associative, idempotent and has an identity \( \mathbb{U} \)

Therefore these can both be considered binary operators which can substitute for the \(\star\) in the Generalized Quantification axioms and theorems.

(56) Partition of Sets.

A set S *of sets* is called a partition of another set T if every element of T is in *exactly* one of the elements of S.
Alternatively, S partitions T if (a) the sets in S are pairwise disjoint and (b) the union of the elements of S is T

Formally,

S partitions T \(\equiv (\forall U,V \mid U \in S \wedge V \in S \wedge U \neq V : U \cap V = \emptyset ) \wedge (\bigcup X \mid X \in S : X ) = T \)

(57) Axiom of Choice.

Analogy: Given a bag of candy you can reach in and pick a piece. Likewise, we expect to be able to choose an arbitrary element from a non-empty set. We postulate this ability as

Axiom: For t a type, there exists a function f: set-of(t) -> t such that for a non-empty set S, f.s \(\in\) S.

Note 1 : a more general version was formulated by Zermelo.

Note 2 : The axiom merely states the *existence* of a function. Does not say how to obtain the function.

Note 3: This axiom is problematic for infinite sets.

EQ 15 Equivalence and True

(1) Axiom: Associativity of \(\equiv\): p \(\equiv\) (q \(\equiv\) r) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) (p \(\equiv\) q ) \(\equiv\) r

(2) Axiom: Symmetry of \(\equiv\): p \(\equiv\) q \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) q \(\equiv\) p

(3) Axiom: Identity of \(\equiv\): true \(\equiv\) q \(\equiv \) q

(4) Theorem: true

(5) Reflexivity of \(\equiv\): p \(\equiv\) p

EQ 14 Negation, Inequivalence, False

(1) Axiom: Definition of false: false \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) \(\neg\) true

(2) Axiom: Distributivity of \(\frac{\neg}{\equiv}\): \(\neg\) (p \(\equiv\) q) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) \(\neg\)p \(\equiv\) q

(3) Axiom: Definition \(\not\equiv\): (p \(\not\equiv\) q) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) \(\neg\)(p \(\equiv\) q)

(4) Theorem: \(\neg\)p \(\equiv\) q \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) p \(\equiv\) \(\neg\)q

(5) Theorem: Double Negation: \(\neg\)\(\neg\)p \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) p

(6) Theorem: Negation of false: \(\neg\)false \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) true

(7) Theorem: (p \(\not\equiv\) q) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) \(\neg\)p \(\equiv\) q

(8) Theorem: \(\neg\)p\(\equiv\)p\(\equiv\)false

(9) Theorem: Symmetry of \(\not\equiv\): p \(\not\equiv\) q \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) q \(\not\equiv\) p

(10) Theorem: Associativity of \(\not\equiv\): (p \(\not\equiv\) (q \(\not\equiv\) r)) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) ((p \(\not\equiv\) q ) \(\not\equiv\) r)

(11) Mutual Associativity: (p \(\not\equiv\) (q \(\equiv\) r)) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) ((p \(\not\equiv\) q ) \(\equiv\) r)

(12) Mutual Interchangability: p \(\not\equiv\) q \(\equiv\) r \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) p \(\equiv\) q \(\not\equiv\) r

EQ 13 Disjunction

(1) Axiom Symmetry of \(\vee\): p \(\vee\) q \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) q \(\vee\) p

(2) Axiom Associativity of \(\vee\): p \(\vee\) (q \(\vee\) r) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) (p \(\vee\) q ) \(\vee\) r

(3) Axiom Idempotency of \(\vee\): p \(\vee\) p \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) p

(4) Axiom Distributivity of \(\frac{\vee}{\equiv}\): p \(\vee\) ( q \(\equiv\) r) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) (p \(\vee\) q) \(\equiv\) (p \(\vee\) r)

(5) Axiom Excluded Middle p \(\vee\) \(\neg\)p

(6) Theorem Zero of \(\vee\): p \(\vee\) true \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) true

(7) Theorem Identity of \(\vee\) p \(\vee\) false \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) p

(8) Theorem Distributivity of \(\frac{\vee}{\vee}\): p \(\vee\) ( q \(\vee\) r) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) (p \(\vee\) q) \(\vee\) (p \(\vee\) r)

(9) Theorem p \(\vee\) q \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) p \(\vee\) \(\neg\)q \(\equiv\) p

EQ 12 Conjunction

(1) Axiom: Golden Rule: p \(\wedge\) q \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) p \(\vee\) q \(\equiv\) p \(\equiv\) q

(2) Theorem Symmetry of \(\wedge\): p \(\wedge\) q \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) q \(\wedge\) p

(3) Theorem Associativity of \(\wedge\): p \(\wedge\) ( q \(\wedge\) r) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) (p \(\wedge\) q) \(\wedge\) r

(4) Theorem Idempotency of \(\wedge\): p \(\wedge\) p \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) p


(5) Theorem Identity of \(\wedge\): p \(\wedge\) true \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) p


(6) Theorem Zero of \(\wedge\): p \(\wedge\) false \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) false


(7) Theorem Distributivity of \(\frac{\wedge}{\wedge}\): p \(\wedge\) ( q \(\wedge\) r) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) (p \(\wedge\) q) \(\wedge\) (p \(\wedge\) r)

(8) Theorem Contradiction: p \(\wedge\) \(\neg\)p \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) false

(9) Theorem Absorption 1: p \(\wedge\) ( p \(\vee\) q) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) p


(10) Theorem Absorption 2: p \(\wedge\) (\(\neg\) p \(\vee\) q) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) p \(\wedge\) q

(11) Theorem Absorption 3: p \(\vee\) ( p \(\wedge\) q) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) p

(12) Theorem Absorption 4: p \(\vee\) (\(\neg\) p \(\wedge\) q) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) p \(\vee\) q

(13) Theorem Distributivity of \(\frac{\wedge}{\vee}\): p \(\wedge\) ( q \(\vee\) r) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) (p \(\wedge\) q) \(\vee\) (p \(\wedge\) r)

(14) Theorem Distributivity of \(\frac{\vee}{\wedge}\): p \(\vee\) ( q \(\wedge\) r) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) (p \(\vee\) q) \(\wedge\) (p \(\vee\) r)

(15) Theorem De Morgan 1 \(\neg\) (p \(\wedge\) q) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) (\(\neg\)p \(\vee\)\(\neg\) q)

(16) Theorem De Morgan 2 \(\neg\) (p \(\vee\) q) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) (\(\neg\)p \(\wedge\)\(\neg\) q)

(17) Theorem p \(\wedge\) q \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) p \(\wedge\) \(\neg\)q \(\equiv\)\(\neg\) p

(18) Theorem p \(\wedge\) ( q \(\equiv\) r) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) p \(\wedge\) q \(\equiv\) p \(\wedge\) r \(\equiv\) p

(19) Theorem p \(\wedge\) ( q \(\equiv\) p) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) p \(\wedge\) q

(20) Theorem Replacement ( p \(\equiv\) q) \(\wedge\) ( r \(\equiv\) p) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) ( p \(\equiv\) q) \(\wedge\) ( r \(\equiv\) q)

(21) Theorem Definition of \(\equiv\): ( p \(\equiv\) q) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) ( p \(\wedge\) q) \(\vee\) (\(\neg\) p \(\wedge\) \(\neg\)q)

(22) Theorem Exclusive Or: ( p \(\not\equiv\) q) \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) ( p \(\wedge\) \(\neg\)q) \(\vee\) (\(\neg\) p \(\wedge\) q)


(23) Theorem (p \(\wedge\) q) \(\wedge\) r \( \hspace{0.2 cm} \equiv \hspace{0.2 cm} \) p \(\equiv\) q \(\equiv\) r \(\equiv\) p \(\vee\) q \(\equiv\) q \(\vee\) r \(\equiv\) p \(\vee\) r \(\equiv\) p \(\vee\) q \(\vee\) r

EQ 11 Existential Quantification

(0) Notation (\(\vee\) x | R : P ) \(\hspace{0.5 cm} \equiv \hspace{0.5 cm}\) (\(\exists\) x | R : P )

(1) Axiom: Generalized deMorgan: (\(\exists\) x | R : P) \(\hspace{0.5 cm} \equiv \hspace{0.5 cm}\) \(\neg\)( \(\forall\) x | R : \(\neg\) P)

(2) Theorem: Generalized deMorgan 1 : \(\neg\) (\(\exists\) x | R : \(\neg\)P) \(\hspace{0.5 cm} \equiv \hspace{0.5 cm}\) ( \(\forall\) x | R : P)

(3) Theorem: Generalized deMorgan 2 : \(\neg\) (\(\exists\) x | R : P) \(\hspace{0.5 cm} \equiv \hspace{0.5 cm}\) ( \(\forall\) x | R : \(\neg\) P)

(4) Theorem: Generalized deMorgan 3 : (\(\exists\) x | R : \(\neg\) P) \(\hspace{0.5 cm} \equiv \hspace{0.5 cm}\) \(\neg\) ( \(\forall\) x | R : P)

(5) Theorem: Trading 1: (\(\exists\) x | R : P) \(\hspace{0.5 cm} \equiv \hspace{0.5 cm}\) ( \(\exists\) x | : R \(\wedge\) P)

(6) Theorem: Trading 2: (\(\exists\) x | S \(\wedge\) R : P) \(\hspace{0.5 cm} \equiv \hspace{0.5 cm}\) ( \(\exists\) x | S : R \(\wedge\) P)

(7) Theorem: Distributivity \(\frac{\wedge}{\exists}\) (\(\exists\) x | R : P) \(\wedge\) Q \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\exists\) x | R : P \(\wedge\) Q)
not-occurs-free(x,Q)

(8) Theorem: (\(\exists\) x | R : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\exists\) x |: R ) \(\wedge\) P
not-occurs-free(x,P)

(9) Theorem: Distributivity \(\frac{\vee}{\exists}\) (\(\exists\)x |:R) \( \Rightarrow \) [(\(\exists\) x | R : P \(\vee\) Q)] \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\exists\) x | R : P) \(\vee\) Q]
not-occurs-free(x,Q)

(10) Theorem: (\(\exists\) x | R : false) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) false

(11) Theorem: Range Weakening: (\(\exists\) x | R : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\exists\) x | R \(\vee\) S : P)

(12) Theorem: Body Weakening: (\(\exists\) x | R : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\exists\) x | R : P \(\vee\) Q)

(13) Theorem: Monotonicity of \(\exists\)
\(\exists\) is monotonic in both body and range
(a) (\(\forall\) x | R : A \( \Rightarrow \) B ) \(\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}\) [ (\(\exists\) x | A : P) \( \Rightarrow \) (\(\exists\) x | B : P)]
(b) (\(\forall\) x | R : A \( \Rightarrow \) B ) \(\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}\) [ (\(\exists\) x | R : A) \( \Rightarrow \) (\(\exists\) x | R : B)]

(14) Theorem: P[ x := e] \(\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}\) (\(\exists\) x |: P)

(15) Theorem: Interchange of Quantifications
(\(\exists\) x | R (\(\forall\) y | S : P)) \(\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}\) (\(\forall\) y | S (\(\exists\) x | R : P))
not-occurs-free (x,S) \(\wedge\) not-occurs-free(y, R)

Note: only when \(\exists\) encloses \(\forall\). The implication doesn't hold the other way.

(16) Meta Theorem Witness:
(\(\exists\) x | R : P) \(\Rightarrow\) Q is a theorem \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (R \(\wedge\) P)[\(x\) := \(\hat{x}\)] \(\Rightarrow\) Q is a theorem,
not-occurs-free(\(\hat{x}\), [P,Q,R])
(a) often used when (\(\exists\) x | R : P) is known and need to prove Q.
(b) with multiple statements, use distinct witnesses

EQ 10 Universal Quantification

(0) Notation: (\(\wedge\) x | R : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x | R : P)

(1) Axiom: Trading: (\(\forall\) x | R : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x |: R \(\Rightarrow\) P)

Trading Theorems

(2) Theorem (\(\forall\) x | R : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x |: \(\neg\)R \(\vee\) P)

(3)Theorem (\(\forall\) x | R : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x |: R \(\vee\) P \(\equiv\) P)

(4)Theorem (\(\forall\) x | R : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x |: R \(\wedge\) P \(\equiv\) R)

(5) Theorem (\(\forall\) x | R \(\wedge\) S : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x | S : R \(\Rightarrow\) P)

(6) Theorem (\(\forall\) x | R \(\wedge\) S : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x | S : \(\neg\)R \(\vee\) P)

(7)Theorem (\(\forall\) x | R \(\wedge\) S : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x | S : R \(\vee\) P \(\equiv\) P)

(8)Theorem (\(\forall\) x | R \(\wedge\) S: P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x | S : R \(\wedge\) P \(\equiv\) R)

(9) Axiom: Distributivity \(\frac{\vee}{\forall}\) Q \(\vee\) (\(\forall\) x | R : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x | R : P \(\vee\) Q)
not-occurs-free(x,Q)

(10)Theorem: (\(\forall\) x | R :P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x |: \( \neg \)R) \(\vee\) P
not-occurs-free(x,P)

(11) Theorem: Distributivity \(\frac{\wedge}{\forall}\) (\(\exists\)x |:R) \( \Rightarrow \) [(\(\forall\) x | R : P \(\wedge\) Q)] \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x | R : P) \(\wedge\) Q]
not-occurs-free(x,Q)

Be careful using this theorem. A conjunct can be moved outside the scope of the quantification only if the Range is not everywhere false

(12) Theorem: (\( \forall \) x | R : true) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) true

(13) Theorem: (\( \forall \) x | R : P \(\equiv\) Q) \(\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}\) [(\( \forall \) x | R : P ) \(\Rightarrow\) (\( \forall \) x | R : Q ) ]

(14) Theorem: Range Weakening/Strengthening (\( \forall \) x | R \(\vee\) S : P ) \(\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}\) (\( \forall \) x | R : P )

(15) Theorem: Body Weakening/Strengthening (\( \forall \) x | R : P \(\wedge\) Q ) \(\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}\) (\( \forall \) x | R : P )

(16) Theorem: Monotonicity of \(\forall\):
(a) \(\forall\) is antimonotonic in its range: (\(\forall\) x | R : A \(\Rightarrow\) B ) \(\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}\) [(\(\forall\) x | A : P ) \(\Leftarrow\) (\(\forall\) x | B : P)]
(b) \(\forall\) is monotonic in its body: (\(\forall\) x | R : A \(\Rightarrow\) B ) \(\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}\) [(\(\forall\) x | R : A ) \(\Rightarrow\) (\(\forall\) x | R : B)]

(17) Instantiation (\( \forall \) x |: P) \(\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}\) P [x := e]

(18) MetaTheorem: P is a theorem \( \equiv \) (\(\forall\) x |: P) is a theorem

EQ 9 Quantification

(1) Monoids And Abelian Monoids

Binary Operator \( \star \) is associative and has an identity \( \equiv \) it is a monoid. If it is also symmetric, it is an abelian monoid.

In the following the \( \star \) represents an operator that is an abelian monoid. All theorems don't strictly need the "abelian-ness", but the operators we deal with are all abelian, so the assumption does no harm.

(2) General Form of Quantification

( \( \star \) x:type1, y:type2 ..) | Range:\( \mathcal{B} \) : Predicate:type3)

x,y,... are bound variables or 'dummmies'
the Predicate is also known as the "body".

(3) Definition of 'free'

(a) The *occurrence* of i, in an expression i is free
(b) If an occurrence of a variable i in expression E is free, then so is the occurrence in (E), function application arguments f(....E...) [note: binary operators are considered function applications)[, (\( \star \)x|E:P) and (\( \star \)x|R:E) (as long as i is not one of the variables in the dummy list x.)

(4) Definition of 'bound'

(a) If an occurrence of a variable i in expression E is free, then that occurrence is bound to dummy i in (\( \star \)x|E:P) and ( \(\star \)x|R:E) if i occurs in dummy list x.

(b) If an occurrence of i is bound in expression E, then it is also bound to the same dummy in (E), function application arguments f(....E...) [note: binary operators are considered function applications)], (\( \star \)x|E:P) and (\( \star \)x|R:E)

(5) Definition of occurs-free and not-occurs-free

occurs-free(v,e) is defined to mean that at least one variable from the list-of-variables v occurs free in at least one expression in list of expressions v

not-occurs-free(v,e) \( \equiv \) \( \neg \)occurs-free(v,e) \( \equiv \) no variable in list-of-variables v occurs free in any of the expressions in list-of-expressions e

(6) Textual Substitution

Extending textual substitution to quantified statements

( \(\star\) x | R : P)[y := F] \( \hspace{0.2 cm}\equiv\hspace{0.2 cm} \) \( (\star\) x | R[y := F] : P[y := F]),

given not-occurs-free(x,[y,F])), iow none of the bound variables is free on either side of the := . If a bound variable does occur free on either side of :=, replace *the bound variable* with a fresh variable j. This ensures that a free variable in the textual substitution y := F does not become bound.

Extending Leibniz inference rule to handle substitution of either side of an equality into a quantified statement

(7) Leibniz 1

\( \frac{A\hspace{0.2 cm}=\hspace{0.2 cm}B}{(\star x |R [z:=A]: P ) \hspace{0.2 cm}=\hspace{0.2 cm} (\star x |R [z:=B]: P )} \)

(8) Leibniz 2

\( \frac{R\hspace{0.2 cm}\Rightarrow\hspace{0.2 cm}A\hspace{0.2 cm}=\hspace{0.2 cm}B}{(\star x |R : P[z:=A] ) \hspace{0.2 cm}=\hspace{0.2 cm} (\star x |R : P [z:=B])} \)

(9) Axiom: Empty Range: ( \(\star\) x | false : P ) \(\hspace{0.2 cm} \equiv\hspace{0.2 cm} \) u (the identity of \( \star \))

(10) Axiom: One Point Range: ( \(\star\) x | x = E : P ) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) P[ x := E ]
provided not-occurs-free (x,E)

(11) Axiom: Distributivity: ( \(\star\) x | R : P ) \(\star\) ( \(\star\) x | R : Q ) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) ( \(\star\) x | R : P \(\star\) Q )
provided each quantification is defined (quantifications with finite ranges are always defined as are quantifications with \(\star\) being either \(\wedge\) or \(\vee\). if \(\star\) is +, then you have to check for convergence of the summation, etc)

(12) Axiom: Range Split 1: ( \(\star\) x | R \(\vee\) S: P ) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) ( \(\star\) x | R : P ) \(\star\) ( \(\star\) x | S : P )
provided (R \(\wedge\) S) is false \(\wedge\) each quantification is defined

(13) Axiom: Range Split 2: ( \(\star\) x | R \(\vee\) S: P ) \( \star\) ( \(\star\) x | R \(\wedge\) S: P ) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) ( \(\star\) x | R : P ) \(\star\) ( \(\star\) x | S : P )
provided each quantification is defined

(14) Axiom: Range Split 3: ( \(\star\) x | R \(\vee\) S: P ) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) ( \(\star\) x | R : P ) \(\star\) ( \(\star\) x | S : P )
provided \(\star\) is idempotent \(\wedge\) each quantification is defined

Note: Definition of idempotent: \(\star\) is idempotent \( \equiv\) ( a \(\star\) a \(\equiv\) a)

(15) Axiom: Interchange of Dummies: ( \(\star\) x | R :( \(\star\) y | S : P) ) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) ( \(\star\) y | S :( \(\star\) x| R : P) )
provided not-occurs-free(x,S) \(\wedge\) not-occurs-free(y,R) \(\wedge\) each quantification is defined

iow "nested quantifications with the same operator can be interchanged"

(16) Axiom: Dummy Nesting: (\(\star\) x,y | R \(\wedge\) S : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) ( \(\star\) x | R :( \(\star\) y | S : P) )
provided not-occurs-free(y,R)

iow " a single quantification over a list of dummies can be viewed as nested quantification"

(17) Axiom: Dummy Renaming: (\(\star\)x | R : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\star\)y | R[x := y] : P[x := y])
provided not-occurs-free (y, [R,P])

iow "one dummy can be replaced consistently by another dummy"

(18) Theorem: Change of Dummy (Generalization of Dummy Renaming) (\(\star\)x | R : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\star\)x | R [x := f.y] : P[x := f.y])

provided not-occurs-free (y,[R,P]) \(\wedge\) f is an invertible function such that x = \(f.y\) and y = \(f^{-1}.x\)

Example: Consider (+ \(i\) | 2 \(\leq\) \(i\) \(\leq\) 10 : \(i^2\) ) and we need to have a range starting with zero

the reqd range is (2 - 0) \(\leq\) \(i - 2 \) \(\leq\) (10 - 2)

let k = (i - 2) this is new dummy expressed in terms of old = \(f^{-1}.i\) = k = i - 2

so i = k + 2 this is old dummy expressed in terms of new = \(f.k\) = i = k + 2

\(\hspace{2 cm}\)(+ \(i\) | 2 \(\leq\) \(i\) \(\leq\) 10 : \(i^2\) )
= \(\hspace{0.5 cm}\) Dummy Renaming Theorem. Rename the dummy from i to k with i = f.k = k - 2
\(\hspace{2 cm}\)(+ \(k\) | 2 \(\leq\) \(k+2\) \(\leq\) 10 : \((k+2)^2\) )
= \(\hspace{0.5 cm}\) arithmetic a \(\leq\) b \(\leq\) c \( \equiv \) a-2 \(\leq\) b-2 \(\leq\) c-2
\(\hspace{2 cm}\)(+ \(k\) | 0 \(\leq\) \(k\) \(\leq\) 8 : \((k+2)^2\) )

(19) Theorem: Split off term 1
(\(\star i\) | \(0 \leq i \lt n+1\) : P) \( \equiv \) (\(\star i\) | \(0 \leq i \lt n\) : P) \(\star\) P[i := n ]

(20) Theorem: Split off term 2
(\(\star i\) | \(0 \leq i \lt n+1\) : P) \( \equiv \) P[i := 0 ] \(\star\) (\(\star i\) | \(0 \lt i \lt n + 1\) : P)

EQ 8 Proof By Induction

(1) Axiom: Mathematical Induction Over \( \mathcal{N} \). Form 1

( \( \forall \) n:\( \mathcal{N} \) |: ( \( \forall \)i | 0 \( \leq \) i \( \lt \) n: \(P_i\)) \( \Rightarrow \) \(P_n\) ) \( \Rightarrow\) ( \( \forall \) n : \( \mathcal{N} \) : \(P_n\))

used to prove Universal Quantification By Induction


(2) Theorem: Mathematical Induction Over \( \mathcal{N} \). Form 2

( \( \forall \) n:\( \mathcal{N} \) |: ( \( \forall \)i | 0 \( \leq \) i \( \lt \) n: \(P_i\)) \( \Rightarrow \) \(P_n\) ) \( \equiv\) ( \( \forall \) n : \( \mathcal{N} \) : \(P_n\))

used to prove properties of Induction

(3) Theorem: Mathematical Induction Over \( \mathcal{N} \). Form 3

\( P_0\) \( \wedge \) ( \( \forall \) n:\( \mathcal{N} \) |: ( \( \forall \)i | 0 \( \leq \) i \( \leq \) n: \( P_i\) ) \( \Rightarrow \) \( P_{n+1} \) ) \( \Rightarrow\) ( \( \forall \) n : \( \mathcal{N} \) : \(P_n\))

restatement of (1) used for inductive proofs

(4) Parts of Mathematical Induction axiom

\( P_0\) is the base case

( \( \forall \) n:\( \mathcal{N} \) |: ( \( \forall \)i | 0 \( \leq \) i \( \leq \) n: \( P_i\) ) \( \Rightarrow \) \( P_{n+1} \) ) \( \Rightarrow\) ( \( \forall \) n : \( \mathcal{N} \) : \(P_n\)) is the inductive case

( \( \forall \) n:\( \mathcal{N} \) |: ( \( \forall \)i | 0 \( \leq \) i \( \leq \) n: \( P_i\) ) \( \Rightarrow \) \( P_{n+1} \) ) is the inductive hypothesis

(5) Normal Proof Method

(1) Prove Base Case. \( P_0 \)

(2) Assume arbitrary n \( \ge \) 0

(3) Assume Inductive Case ( \( \forall \)i | 0 \( \leq \) i \( \leq \) n: \( P_i\) )

(4) Prove \( P_{n+1} \)


(6) Induction starting at other integers

Let a sequence of integers start at \( n_0 \) Then Inductive Theorem is

\( P_{n_0}\) \( \wedge \) ( \( \forall \) n:\(n_0 \leq n \)|: ( \( \forall \)i | \(n_0 \leq \) i \( \leq \) n: \( P_i\) ) \( \Rightarrow \) \( P_{n+1} \) ) \( \Rightarrow\) ( \( \forall \) n : \(n_0 \leq n \) : \(P_n\))

EQ 7: Leibniz Axiom and Theorems

(1) Axiom, Leibniz: (e = f) \( \Rightarrow \) \( E_e^z = E_f^z \)

Note 1: difference between Leibniz Inference Rule and the Leibniz Axiom.

The inference rule states that if X = Y in all states then \( E_X^z = E_Y^z\) in all states.

The axiom states that if (x = y) in one state then \(E_x^z = E_y^z \) in that state.

Note 2: the implication is one way. iow \( E_e^z = E_f^z \) \( \nRightarrow \) (e = f)

e.g: Let E \( \equiv \) false \( \wedge \) zee . Here \( E_e^z = E_f^z \) but e \( \neq \) f

Substitution Theorems:

If an equality conjuncts or implies, or a conjunction with an equality as a conjunct implies , an Expression E containing one side of the equality, you can replace that part of E with the other side of the equality.

(2) Theorem: Substitution 1: (e = f) \( \wedge\) \( E_e^z \equiv \) (e = f) \( \wedge\) \( E_f^z \)

(3) Theorem: Substitution 2: (e = f) \( \Rightarrow\) \( E_e^z \equiv \) (e = f) \( \Rightarrow\) \( E_f^z \)

(4) Theorem: Substitution 3: q \( \wedge \) (e = f) \( \Rightarrow\) \( E_e^z \equiv \) q \( \wedge \) (e = f) \( \Rightarrow\) \( E_f^z \)

Replace By True Theorems:

If a variable conjuncts or implies, or a conjunction with a variable as a conjunct implies an expression E containing that variable, the occurences of the variable in the expression can be replaced by true

(5) Theorem Replace by true 1: p \( \wedge\) \( E_p^z \equiv \) p \( \wedge\) \( E_{true}^z \)

(6) Theorem: Replace by true 2: p \( \Rightarrow \) \( E_p^z \equiv \) p \( \Rightarrow \) \( E_{true}^z \)

(7) Theorem: Replace by true 3: q \( \wedge \) p \( \Rightarrow \) \( E_p^z \equiv \) q \( \wedge \) p \( \Rightarrow \) \( E_{true}^z \)

Example:

Prove p \( \wedge \) q \( \Rightarrow \) ( p \( \equiv \) q)

\( \hspace{2 cm }\) p \( \wedge \) q \( \Rightarrow \) ( p \( \equiv \) q)

=\( \hspace{0.5 cm } \) recognize pattern. conjunction with a variable (p) on one side implying an expression containing the same variable
\( \hspace{0.5 cm } \) invoke Theorem (6) above, replace p in expression by true

\( \hspace{2 cm }\) p \( \wedge \) q \( \Rightarrow \) ( true \( \equiv \) q)

=\( \hspace{0.5 cm } \) recognize pattern. conjunction with a variable (q) on one side implying an expression containing the same variable
\( \hspace{0.5 cm } \) invoke Theorem (6) above, replace q in expression by true

\( \hspace{2 cm }\) p \( \wedge \) q \( \Rightarrow \) ( true \( \equiv \) true)

=\( \hspace{0.5 cm } \) Theorem: true is the identity of \( \equiv \), m \( \equiv \) m \( \equiv \) true

\( \hspace{2 cm }\) p \( \wedge \) q \( \Rightarrow \) true

=\( \hspace{0.5 cm } \) Theorem: true is the Right Zero of \( \Rightarrow \), m \( \Rightarrow \) true \( \equiv \) true

\( \hspace{2 cm }\) true

Replace By False Theorems:

If an Expression E containing a variable p disjuncts p, implies p or implies a disjunction with p on one side,p can be replaced by false in the expression

(8) Theorem: Replace by False 1: \( E_p^z\) \( \vee \) p \( \equiv \) \( E_{false}^z\) \( \vee \) p

(9) Theorem: Replace by False 2: \( E_p^z\) \( \Rightarrow \) p \( \equiv \) \( E_{false}^z\) \( \Rightarrow \) p

(10) Theorem: Replace by False 2: \( E_p^z\) \( \Rightarrow \) p \(\vee\) q \( \equiv \) \( E_{false}^z\) \( \Rightarrow \) p \(\vee\) q

(11) Theorem: Shannon: \( E_p^z\) \( \equiv \) ( p \(\wedge\) \( E_{true}^z\) ) \(\vee\) ( \( \neg \) p \(\wedge\) \( E_{false}^z\) )

EQ 6: Monotonicity

(a) Definition.

A function f is monotonic in its argument \( \equiv \) (x \( \Rightarrow \) y) \( \hspace{0.2 cm } \Rightarrow \hspace{0.2 cm } \) (f.x \( \Rightarrow \) f.y)

Note: The textual substitution approach in the Inference Rules provided below are a better way to work out monotonicity etc than a 'function' approach using above idea.

A function is anti-monotonic in its argument \( \equiv \) (x \( \Rightarrow \) y) \( \hspace{0.2 cm } \Rightarrow \hspace{0.2 cm } \) (f.x \( \Leftarrow \) f.y)

(b) Monotonicity of Logical Operators

\( \hspace{0.5 cm } \vee \) Monotonic. (p \( \Rightarrow \) q) \( \hspace{0.2 cm } \Rightarrow \hspace{0.2 cm } \) (p \( \vee \) r) \( \Rightarrow \) (q \( \vee \) r )

\( \hspace{0.5 cm } \wedge \) Monotonic. (p \( \Rightarrow \) q) \( \hspace{0.2 cm } \Rightarrow \hspace{0.2 cm } \) (p \( \wedge \) r) \( \Rightarrow \) (q \( \wedge \) r )

\( \hspace{0.5 cm } \neg \) Antimonotonic. (p \( \Rightarrow \) q) \( \hspace{0.2 cm } \Rightarrow \hspace{0.2 cm } \) ( \( \neg \) p \( \Leftarrow \) \( \neg \) q )

\( \hspace{0.5 cm } \Rightarrow \) Antimonotonic Antecedent. (p \( \Rightarrow \) q) \( \hspace{0.2 cm }\) \( \Rightarrow \) \( \hspace{0.2 cm }\) ( (p \( \Rightarrow \) r) \( \Leftarrow \) (q \( \Rightarrow \) r) )

\( \hspace{0.5 cm } \Rightarrow \) Monotonic Consequent. (p \( \Rightarrow \) q) \( \hspace{0.2 cm }\) \( \Rightarrow \) \( \hspace{0.2 cm }\) ( (r \( \Rightarrow \) p) \( \Rightarrow \) (r \( \Rightarrow \) q) )

\( \hspace{0.5 cm } \forall \) Antimonotonic Range. (a \( \Rightarrow \) b) \( \hspace{0.2 cm }\) \( \Rightarrow \) \( \hspace{0.2 cm }\) ( ( \( \forall \)x | a : P) \( \Leftarrow \) ( \( \forall \)x | b : P))

\( \hspace{0.5 cm } \forall \) Monotonic Body. (a \( \Rightarrow \) b) \( \hspace{0.2 cm }\) \( \Rightarrow \) \( \hspace{0.2 cm }\) ( ( \( \forall \)x | R : a) \( \Rightarrow \) ( \( \forall \)x | R : b))

\( \hspace{0.5 cm } \exists \) Monotonic Range. (a \( \Rightarrow \) b) \( \hspace{0.2 cm }\) \( \Rightarrow \) \( \hspace{0.2 cm }\) ( ( \( \exists \)x | a : P) \( \Rightarrow \) ( \( \exists \)x | b : P))

\( \hspace{0.5 cm } \exists \) Monotonic Body. (a \( \Rightarrow \) b) \( \hspace{0.2 cm }\) \( \Rightarrow \) \( \hspace{0.2 cm }\) ( ( \( \exists \)x | R : a) \( \Rightarrow \) ( \( \exists \)x | R : b))

(c) Capture Avoiding Substitution

( E[z := P ] denotes capture-avoiding substitution: E[z := P ] is a copy of expression E in which all occurrences of *free* variable z have been replaced by expression P , with names of dummies (bound variables) being first replaced to avoid capture.) (Note: best way to avoid this in practice is to have no names in common, bound or not, between P and E. If programming this substitution, then better to rename only bound vars)

(d) Monotonic and Antimonotonic Positions

Consider an occurrence of free variable z in a formula E (but not within an operand of \( \equiv \) ). The *position* of z within E is called monotonic if it is nested within an even number of negations, antecedents, or ranges of universal quantifications; otherwise, it is antimonotonic.

(e) Detailed Method for determining the monotonicity of a position

(1) Replace ( \( \forall \)x | \( F_1 \) : \( F_2 \) ) \( \hspace{0.2 cm }\) by \( \hspace{0.2 cm }\) \( \neg \)( \( \exists \)x | \( F_1 \) : \(\neg F_2 \) )

(2) Replace ( \( \exists \)x | \( F_1 \) : \( F_2 \) ) \( \hspace{0.2 cm }\) by \( \hspace{0.2 cm }\) ( \( \exists \)x |: \( F_1 \wedge F_2 \) )

(3) Replace ( \( F_1 \nLeftarrow F_2 \) ) \( \hspace{0.2 cm }\) by \( \hspace{0.2 cm }\) \( \neg \)( \( F_1 \Leftarrow F_2 \) )

(4) Replace ( \( F_1 \nRightarrow F_2 \) ) \( \hspace{0.2 cm }\) by \( \hspace{0.2 cm }\) \( \neg \)( \( F_1 \Rightarrow F_2 \) )

(5) Replace ( \( F_1 \Leftarrow F_2 \) ) \( \hspace{0.2 cm }\) by \( \hspace{0.2 cm }\) ( \( F_2 \Rightarrow F_1 \) )

(6) Replace ( \( F_1 \Rightarrow F_2 \) ) \( \hspace{0.2 cm }\) by\( \hspace{0.2 cm }\) ( \( \neg F_1 \vee F_2 \) )

(7) Replace ( \( F_1 \wedge F_2 \) ) \( \hspace{0.2 cm }\) by\( \hspace{0.2 cm }\) ( \( \neg (\neg F_1 \vee \neg F_2) \) )

(8) If z is in the second operand \( F_2 \) of ( \( F_1 \vee F_2 \) ), replace ( \( F_1 \vee F_2 \) ) by ( \( F_2 \vee F_1 \) )

(9) Count the number of \( \neg \)s in enclosing z. (the enclosing \( \forall \)s and \( \Rightarrow \)s have been transformed away by steps 1 through 8). If the number is even then positonOf(z) is monotonic and if odd then positionOf(z) is antimonotonic.

(e) MetaTheorem Monotonicity

Suppose P \( \Rightarrow \) Q is a theorem. Let E contain exactly one occurrence of free variable z (but not within an operand of \( \equiv \) ). Then

(a)If postionOf(z) is monotonic, then E[ z := P ] \( \Rightarrow \) E[ z := Q ]
(b)If postionOf(z) is monotonic, then E[ z := P ] \( \Leftarrow \) E[ z := Q ]

This also works if there are multiple occurrences of z, but they all have either monotonic xor antimonotonic positions

(f) Expressing Metatheorem Monotonicity as inference rules

(1) \( \frac{P \Rightarrow Q \hspace{0.2 cm} \wedge \hspace{0.2 cm } position \hspace{0.2 cm } of \hspace{0.2 cm } z \hspace{0.2 cm } is \hspace{0.2 cm } monotonic}{E[ z := P ] \hspace{0.2 cm } \Rightarrow \hspace{0.2 cm } E[ z := Q ]} \)


(2) \( \frac{P \Rightarrow Q \hspace{0.2 cm} \wedge \hspace{0.2 cm } position \hspace{0.2 cm } of \hspace{0.2 cm } z \hspace{0.2 cm } is \hspace{0.2 cm } antimonotonic}{E[ z := P ] \hspace{0.2 cm } \Leftarrow \hspace{0.2 cm } E[ z := Q ]} \)

(g) Convention for citing monotonicity in proofs

\( \hspace{2 cm } (\forall x |: P \wedge R) \)
\( \Rightarrow \hspace{0.5 cm } \) Monotonicity, weakening P \( \Rightarrow \) P \( \vee \) Q
\( \hspace{2 cm } (\forall x |: (P \vee Q) \wedge R) \)

Explanation: Consider \( ( \forall x |: P \wedge R) \) to be E \( \equiv \) \( (\forall x |: z \wedge R) \) and use P \( \Rightarrow \) P \( \vee \) Q as the implication in the Monotonicity Metatheorem. (the position of z is monotonic since it is the body position of a \( \forall \) )

(h) Examples

(1) Given One Point Rule, ie, ( \( \forall \) x | x = E : P) \( \equiv \) P [x := E ] and x does not occur free in E , prove Instantiation theorem, ie, Prove \( (\forall x |: P) \Rightarrow P [ x := E ] \)

Old proof, without monotonicity

LHS \( \hspace{2 cm } (\forall x |: P) \)

= \( \hspace{0.5 cm } \) notation expansion

\( \hspace{2 cm } (\forall x | true : P) \)

= \( \hspace{0.5 cm } \) true \( \equiv a \vee \neg a \)

\( \hspace{2 cm } (\forall x | (x = E) \vee (x \neq E) : P) \)

= \( \hspace{0.5 cm } \) Axiom: Range Split \( (\star | R \vee S: P) \equiv (\star | R : P) \star (\star | S : P) \) here \( \star = \wedge. \) notated as \( \forall \)


\( \hspace{2 cm } (\forall x | (x = E) : P) \wedge (\forall x | (x \neq E) : P) \)

\( \Rightarrow \hspace{0.5 cm } Theorem: a \wedge b \Rightarrow a \)

\( \hspace{2 cm } (\forall x | (x = E) : P) \)

= \( \hspace{0.5 cm } \) Single Point Axiom \( (\star y | (y = F) : Q) \equiv \) Q [ y := F ]

\( \hspace{2 cm } \) P [ x := E ] = RHS.
QED

new proof (using monotonicity)

LHS \( \hspace{2 cm } (\forall x |: P) \)

= \( \hspace{0.5 cm } \) notation expansion

\( \hspace{2 cm } (\forall x | true : P) \)

= \( \hspace{0.5 cm } \) Dummy Renaming ( \( \star \) x | R : P) \( \equiv \) ( \( \star \) y | R[x := y] : P [x := y]) , given y does not occur free in R or P, choose a variable m such that not occurs-free(m, [R, P])

\( \hspace{2 cm } \) ( \( \forall \) m | true : P[x := m])

\( \Rightarrow \hspace{0.5 cm } \) Monotonicity, Right Zero of \( \Rightarrow \) a \( \Rightarrow \) true \( \equiv \) true for any a . Let a = ( m = E) . position of true is anti monotonic

\( \hspace{2 cm }\) ( \(\forall\) m | (m = E) : P[x := m])

= \( \hspace{0.5 cm } \) Single Point theorem, given.

\( \hspace{2 cm }\) P[x := m][m := E]

= \( \hspace{0.5 cm } \) Successive textual replacement

\( \hspace{2 cm } \) P[x := E] QED

Note: implications with true or false in them are useful.

Example 2: All men are mortal, Socrates is a man. Therefore Socrates is mortal.

step 1: establish notation.

man.m : person m is a man
mortal.m : person m is a mortal
S : Socrates

step 2: formalize English to logic

( \( \forall \) m |: man.m \( \Rightarrow \) mortal.m) \( \wedge \) man.S \( \Rightarrow \) mortal.S

step 3: prove

LHS \( \hspace{2 cm } \) ( \( \forall \) m |: man.m \( \Rightarrow \) mortal.m) \( \wedge \) man.S \( \Rightarrow \) mortal.S

\( \Rightarrow \hspace{0.5 cm } \) Monotonicity, Instantiation \( (\forall x |: P) \Rightarrow P [ x := e ] \), e = S, \( \wedge \) is monotonic in both arguments

\( \hspace{2 cm } \) (man.S \( \Rightarrow \) mortal.S) \( \wedge \) man.S

\( \Rightarrow \hspace{0.5 cm } \) Modus Ponens

\( \hspace{2 cm } \) mortal.S QED

Example 3

Prove

None but those with hearts can love. Some liars are heartless. Some liars cannot love

Step 1:Establish notation

hh.p = p has a heart
cl.p = p can love
li.p = p is a liar

Step 2: Translate English to logic
( \( \forall \) p|: \( \neg \)hh.p \( \Rightarrow \) \( \neg \) cl.p ) \( \wedge \) ( \( \exists \)x |: li.x \( \wedge \) \( \neg \) hh.x ) \( \Rightarrow \) ( \( \exists \) y |: li.y \( \wedge \neg\) cl.y)

Step 3 Prove

LHS \( \hspace{2 cm } \) ( \( \forall \) p|: \( \neg \)hh.p \( \Rightarrow \) \( \neg \) cl.p ) \( \wedge \) ( \( \exists \)x |: li.x \( \wedge \) \( \neg \) hh.x )

= \( \hspace{0.5 cm } \) Theorem: Contrapositive p \( \Rightarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) \( \neg \)q \( \Rightarrow \) \( \neg \) p

\( \hspace{2 cm } \) ( \( \forall \) p|: cl.p \( \Rightarrow \) hh.p ) \( \wedge \) ( \( \exists \)x |: li.x \( \wedge \) \( \neg \) hh.x )

= \( \hspace{0.5 cm } \) Theorem Distribution of \( \wedge \) over \( \exists \), P \( \wedge \) ( \( \exists \) x | R : Q ) \( \equiv \) ( \( \exists \) x | R : P \( \wedge \) Q )

\( \hspace{2 cm } \) ( \( \exists \)x |: ( \( \forall \) p|: cl.p \( \Rightarrow \) hh.p ) \( \wedge \) li.x \( \wedge \) \( \neg \) hh.x )



= \( \hspace{0.5 cm } \) Monotonicity, Instantiation with (p = x), \( \wedge \) is monotonic in both arguments

\( \hspace{2 cm } \) ( \( \exists \) x|: (cl.x \( \Rightarrow \) hh.x) \( \wedge \) li.x \( \wedge \) \( \neg \) hh.x )

= \( \hspace{0.5 cm } \) Theorem: Contrapositive p \( \Rightarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) \( \neg \)q \( \Rightarrow \) \( \neg \) p

\( \hspace{2 cm } \) ( \( \exists \) x |: (\( \neg \) hh.x \( \Rightarrow \) \( \neg \) cl.x) \( \wedge \) li.x \( \wedge \) \( \neg \) hh.x )

\( \hspace{0.5 cm } \) \( \Rightarrow \hspace{0.5 cm } \) Modus Ponens

\( \hspace{2 cm } \) ( \( \exists \) x |: \( \neg \) cl.x \( \wedge \) li.x)

= \( \hspace{0.5 cm } \) Translate to English

\( \hspace{2 cm } \) There exists some people who are liars and also can't love = Some liars can't love QED

EQ 5 Implication Axioms and Theorems

(1) Axiom: Definition of Implication: p \( \Rightarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p \( \vee \) q \( \equiv \) q

(2) Axiom: Consequence p \( \Leftarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) q \( \Rightarrow \) p

(3) Theorem: Definition of Implication p \( \Rightarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm }\) \( \neg \)p \( \vee \) q

(4) Theorem: Definition of Implication: p \( \Rightarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p \( \wedge \) q \( \equiv \) p

(5) Theorem: Contrapositive p \( \Rightarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) \( \neg \)q \( \Rightarrow \) \( \neg \) p

(6) Theorem: p \( \Rightarrow \) (q \( \equiv \) r)\( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p \( \wedge\) q \( \equiv \) p \( \wedge \) r

(7) Theorem: Distributivity \( \frac{\Rightarrow}{\equiv} \) p \( \Rightarrow \) (q \( \equiv \) r) \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p \( \Rightarrow \) q \( \equiv \) p \( \Rightarrow \) r

(8) Theorem: Distributivity \( \frac{\Rightarrow}{\Rightarrow} \) p \( \Rightarrow \) (q \( \Rightarrow \) r) \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) (p \( \Rightarrow \) q) \( \Rightarrow \) (p \( \Rightarrow \) r)

(9) Theorem: Shunting p \( \wedge \) q \( \Rightarrow \) r \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p \( \Rightarrow \) (q \( \Rightarrow \) r )

(10) Theorem: p \( \wedge \) ( p \( \Rightarrow \) q ) \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p \( \wedge \) q

(11) Theorem: p \( \wedge \) ( q \( \Rightarrow \) p) \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p

(12) Theorem: p \( \vee \) ( p \( \Rightarrow \) q ) \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) true

(13) Theorem: p \( \vee \) ( q \( \Rightarrow \) p) \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) q \( \Rightarrow \) p

(14) Theorem: p \( \vee \) q \( \hspace{0.2 cm } \)\( \Rightarrow \)\( \hspace{0.2 cm } \) p \( \wedge \) q \( \equiv \) p \( \equiv \) q

(15) Reflexivity of \( \Rightarrow \) : p \( \Rightarrow \) p \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) true

(16) Theorem: Right Zero of \( \Rightarrow \) : p \( \Rightarrow \) true \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) true

(17) Theorem: Left Identity of \( \Rightarrow \) : true \( \Rightarrow \) p \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p

(18) Theorem: p \( \Rightarrow \) false \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) \( \neg \)p


(19) Theorem: false \( \Rightarrow \) p \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) true

Weakening and Strengthening Theorems

(20) Theorem: p \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) p \( \vee \) q

(21) Theorem: p \( \wedge \) q \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) p

(22) Theorem: p \( \wedge \) q \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) p \( \vee \) q

(23) Theorem: p \( \wedge \) q \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) p \( \wedge \) (q \( \vee \) r)

(24) Theorem: p \( \vee \) (q \( \wedge \) r) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) p \( \vee \) q




(25) Theorem: Modus Ponens p \( \wedge \) ( p \( \Rightarrow \) q) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) q

(26) Theorem : (p \( \Rightarrow \) r) \( \wedge \) (q \( \Rightarrow \) r) \( \hspace{0.2 cm } \) \( \equiv \) \( \hspace{0.2 cm } \) ( p \( \vee \) q \( \Rightarrow \) r)

(27) Theorem : (p \( \Rightarrow \) r) \( \wedge \) ( \( \neg \)p \( \Rightarrow \) r) \( \hspace{0.2 cm } \) \( \equiv \) \( \hspace{0.2 cm } \) r

(28) Theorem: Mutual Implication (p \( \Rightarrow \) q) \( \wedge \) (q \( \Rightarrow \) p) \( \hspace{0.2 cm } \) \( \equiv \) \( \hspace{0.2 cm } \) ( p \( \equiv \) q)

(29) Theorem: Anti-Symmetry (p \( \Rightarrow \) q) \( \wedge \) (q \( \Rightarrow \) p) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) ( p \( \equiv \) q)

(30) Theorem: Transitivity (1) (p \( \Rightarrow \) q) \( \wedge \) (q \( \Rightarrow \) r) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) (p \( \Rightarrow \) r)

(31) Theorem: Transitivity (2) (p \( \equiv \) q) \( \wedge \) (q \( \Rightarrow \) r) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) (p \( \Rightarrow \) r)

(32) Theorem: Transitivity (3) (p \( \Rightarrow \) q) \( \wedge \) (q \( \equiv \) r) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) (p \( \Rightarrow \) r)

Other useful Implication Theorems

(33) Theorem: p \( \Rightarrow \) ( q \( \Rightarrow \) p) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) true

(34) Theorem (p \( \Rightarrow \) q) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) (p \( \wedge \) r) \( \Rightarrow \) (q \( \wedge \) r)

(35) Theorem (p \( \Rightarrow \) q) \( \wedge \) (r \( \Rightarrow \) s) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) (p \( \vee \) r) \( \Rightarrow \) (q \( \vee \) s)

(36) Theorem (p \( \Rightarrow \) q) \( \wedge \) (r \( \Rightarrow \) s) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) (p \( \wedge \) r) \( \Rightarrow \) (q \( \wedge \) s)

(37) Theorem a \( \Rightarrow \) \( \neg \)b \( \hspace{0.2 cm } \) \( \equiv \) \( \hspace{0.2 cm } \) a \( \Rightarrow \) b \( \equiv \) \( \neg \)a

(38) Theorem \( \neg \)a \( \Rightarrow \) b \( \hspace{0.2 cm } \) \( \equiv \) \( \hspace{0.2 cm } \) a \( \Rightarrow \) b \( \equiv \) b

EQ 4 Equality vs Equivalence

b \( \equiv\) c is evaluated the same as b = c (in terms of truth tables) except that \( \equiv \) is allowed only when b and c are booleans.

Definition of Conjunctional

If \( \circ \) and \( \star \) are conjunctional operators, b \( \circ \) c \( \star \) d is equivalent to b \( \circ \) c \( \wedge \) c \( \star \) d.

From the precedence table, all operators on line 10 are conjunctional, ie = < > \( \epsilon \) \( \subset \) \( \subseteq \) \( \supset \) \( \supseteq \) | are all conjunctional

Definition of Associative

Binary Operator \( \circ \) is associative \( \equiv \) ((b \( \circ \) c) \( \circ \) d) = (b \( \circ \) ( c \( \circ \) d ))

Key 1: \( \equiv \) is associative, = is conjunctional
Key 2: Conjunctional use of = (and other conjunctional operators ) are syntactic sugar.

Conversion back and forth:


\( \hspace{2 cm }\) b \( \equiv \) c \( \equiv \) d

= \( \hspace{0.5 cm } \) parenthesize

\( \hspace{2 cm }\) (b \( \equiv \) c ) \( \equiv \) d

= \( \hspace{0.5 cm } \) replace operator

\( \hspace{2 cm } \) (b = c) = d

and

\( \hspace{2 cm }\) b = c = d
= \( \hspace{0.5 cm } \) remove conjunctional syntactic sugar
\( \hspace{2 cm }\) b = c \( \wedge \) c = d
= \( \hspace{0.5 cm } \) parenthesize
\( \hspace{2 cm }\) (b = c) \( \wedge \) (c = d)
= \( \hspace{0.5 cm } \) replace operator
\( \hspace{2 cm }\) (b \( \equiv \) c) \( \wedge \) (c \( \equiv \) d)

EQ 3: Inference Rules

The logic EQ has four inference rules

(1) Substitution

\( \frac{E}{E[v := F]} \)

where E is an expression, v is a list of variables and F is a corresponding list of expressions.

Iow, if E is a theorem, so is E with all the variables in V replaced by the corresponding expressions in F.

E.g: Let E be 2.x/2 = x be a theorem.

Then by substitution, so is 2.(j + 5) / 2 = j + 5 where v=x and E = j+5


(2) Leibniz

\( \frac{X=Y}{E[z:=X]=E[z:=Y]} \)

NB: z is a variable, NOT an expression.

Two ways of looking at Leibniz


(A) Given an equality X = Y and an expression E,

(1) Choose a variable z within E
(2) Replace the equality with a new equality with z replaced by X on one side and Y on the other

(B) Given E,

(1) spot an *expression X* (NOT variable ) within E that needs replacement
(2) Find an equality X = Y
(3) consider the given expression E to be actually E [z := X]
(4) Use Leibniz with the equality (from (2) ) to get E [z := Y]

this is written as
\( \hspace{2 cm } E[z:=X] \)
= \( \hspace{0.5 cm } \) Leibniz. z is z. X = Y
\( \hspace{2 cm } E[z:=Y \)

eg:

Given m = 2j (note: this is the equality X = Y) and E is m/2 = 2.(j - 1) prove that 2j/2 = 2(j-1)

Leibniz usage B: m on the LHS of E needs to be replaced with 2j, so we look for an equality with m on the left side, which we find in the given equality. If we consider the LHS of E to be E[z := m], then

\( \hspace{2 cm } m/2 = 2(j - 1) \)
= \( \hspace{0.5 cm } \) Leibniz. z is m, m = 2j
\( \hspace{2 cm } 2j/2 = 2(j - 1) \)




(C) Combined use of Substitution and Leibniz

Strictly speaking, Substitution and Leibniz are distinct inference rules and the two should be used distinctly



Given we know that 2x/2 = x (note: this is the equality X=Y)

let E be 2j/2 = 2(j+1). prove j = 2(j-1 )

(separate use of Substitution and Leibniz)
\( \hspace{2 cm }E \equiv \) 2j/2 = 2(j - 1)
= \( \hspace{0.5 cm } \) Substitution j := x
\( \hspace{2 cm }\) 2x/2 = 2(x - 1)
= \( \hspace{0.5 cm } \) Leibniz z is 2x/2 with equality 2x/2 = x
\( \hspace{2 cm } \) x = 2(x - 1)
= \( \hspace{0.5 cm } \) Substitution x := j
\( \hspace{2 cm } \)j = 2(j - 1) QED


(simultaneous use of Substitution and Leibniz collapses some steps)
\( \hspace{2 cm }E \equiv \) 2j/2 = 2(j - 1)
= \( \hspace{0.5 cm } \) Substitution and Leibniz 2x/2:= x
\( \hspace{2 cm } \)j = 2(j - 1) QED

(3) Transitivity

\( \frac{X=Y,Y=Z}{X=Z} \)

iow if X = Y and Y = Z are theorems, so is X = Z

(4) Equanimity

\( \frac{E,E=F}{F} \)


iow a theorem is either an axiom or the result of an inference rule where the premises are axioms

Example for use of all 4 inference rules

Prove that \( \neg p \equiv p \equiv false \)

Proof:

(0) \( \hspace{2 cm } \neg p \equiv p \equiv false \)
(1) = \( \hspace{0.5 cm } \) Leibniz and Substitution with Theorem \(\neg (x \equiv y) \equiv \neg x \equiv y \) used in the reverse direction, substituting x,y := p,p and z = \(\neg p \equiv p \)
(2) \( \hspace{2 cm } \neg (p \equiv p) \equiv\) false
(3) = \( \hspace{0.5 cm } \) Leib + Sub using Theorem Identity of \( \equiv \),\( x \equiv x \equiv \) true , z is p \( \equiv \) p, and x := p
(4) \( \hspace{2 cm } \neg true \equiv false \)
(3) = \( \hspace{0.5 cm } \) is an Axiom and therefore
(5) \( \hspace{2 cm } \) true QED

and since (0) = (2) and (2) = (4) and (4) = (5), by Transitivity (0) = (4)

and since (0) = (4) and (4) is a theorem, (0) is a theorem by Equanimity.