(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.
No comments:
Post a Comment