Set Theory
3
14module set
Set theory is almost the simplest possible first order logical system. It contains no formal terms and only a single binary predicate symbol: .
4syntax in
5 sentence (500) ::= term " ∈ " term
6end
8notation not_in
9 sentence (500) ::= term " ∉ " term
10end
12@[reducible]
13definition
14 a ∉ b := ¬a ∈ b
15end
The intended reading of is that is a set of which is an element. In our version of set theory, all objects are sets. Despite this simplicity, we can encode essentially all of mathematics using set theory. We will find ways to encode objects not traditionally thought of as sets using sets.
We have an intuitive notion of what a set is, but of course, we will need to provide axioms to make this understanding rigorous.
Axioms 3.1
27module set.axioms
The set of axioms we will be using for our set theory is called the Zermelo-Fraenkel axioms with Choice, abbreviated ZFC. There are other systems of axioms we could use, but ZFC is a commonly accepted set.
You may be hoping that will come with two axioms, an introduction and an elimination rule. Sadly this is not the case.
We do get an elimination rule. It says that two sets are equal if they contain exactly the same elements. This is traditionally known as extensionality.
11axiom zfc.extensionality :
12 |- ∀a, ∀b, (∀x, x ∈ a ↔ x ∈ b) → a = b
13end
We will be presenting the axioms as unschematized statements in first-order logic without using the iota operator. This is done to make clear the distinction between the axioms for which this can be done, and those for which it can't. We will state more natural forms of these axioms as theorems later.
Intuitively, a set is supposed to be a collection of all the objects with a certain property. Therefore, we might naturally expect to have an introduction rule similar to the following:
axiom zfc.comprehension [p(_) : sentence(term)] :
|- ∃x, ∀y, (y ∈ x ↔ p(y))
end
However, such an axiom would be inconsistent. In particular, we would run into Russell's paradox: the axiom allows us to construct the set which consists of all sets which do not contain themselves. Then we ask if . If it is then it should not be and if it isn't then it should be. We have a contradiction.
This leads us to the conclusion that not all properties can define sets. The remainder of the axioms of ZFC essentially define restricted forms of our idealized comprehension axiom which are believed not to lead to a contradiction. This will leave us with various operations which we can use to define our sets. In the end, almost all the sets we care about will be definable with these operations and so we will be able to act much as if we did have unrestricted comprehension.
The empty set axiom asserts the existence of a set with no elements.
46axiom zfc.empty_set :
47 |- ∃x, ∀y, y ∉ x
48end
For any two sets we can form the set containing exactly those two sets.
52axiom zfc.pairing :
53 |- ∀a, ∀b, ∃x, ∀y, y ∈ x ↔ y = a ∨ y = b
54end
For any set we can take the union of all elements in the set.
58axiom zfc.union :
59 |- ∀a, ∃x, ∀y, y ∈ x ↔ (∃z, y ∈ z ∧ z ∈ a)
60end
For any set we can form the set of all subsets of the set (the powerset).
64axiom zfc.powerset :
65 |- ∀a, ∃x, ∀y, y ∈ x ↔ (∀z, z ∈ y → z ∈ a)
66end
There is a set containing the empty set with the property that for any in the set, the set also contains . Such a set is called an inductive set and must be infinite. Without this axiom we would have no way to prove any infinite sets exist.
73axiom zfc.infinity :
74 |- ∃x, (∃y, y ∈ x ∧ ∀z, z ∉ y)
75 ∧ (∀y, y ∈ x → ∃z, z ∈ x ∧ (∀w, w ∈ z ↔ w ∈ y ∨ w = y))
76end
Then we get the two axiom schemas. These are statements about all sentences which can't be stated using only quantifiers. The first says that for any set we can take the subset of all elements with a particular property. This is quite similar to the rejected comprehension axiom, but this one doesn't lead to contradictions (as far as we know). This is sometimes also called separation or restricted comprehension.
85axiom zfc.specification [p(_) : sentence(term)] :
86 |- ∀a, ∃x, ∀y, y ∈ x ↔ y ∈ a ∧ p(y)
87end
This axiom asserts that the image of any set under a function (implicitly defined by ) exists. This is surprisingly rarely required.
92axiom zfc.replacement [p(_0, _1) : sentence(term, term)] :
93 |- ∀a, (∀x, x ∈ a → ∃!y, p(x, y)) → (∃x, ∀y, y ∈ x ↔ (∃z, z ∈ a ∧ p(z, y)))
94end
The final axiom has a formal statement that is somewhat difficult to parse. But the important point is that it guarantees that we do not get an infinite chain of descending sets . In other words, all sets are nested at a finite depth (despite the fact that some sets contain an infinite number of elements).
102axiom zfc.regularity :
103 |- ∀a, (∃x, x ∈ a) → (∃y, y ∈ a ∧ ¬∃z, (z ∈ y ∧ z ∈ a))
104end
The final axiom is the famed Axiom of Choice. It is the C in ZFC. However it has a much longer first order statement and it is generally considered more polite to be clear when one is using it. So we will postpone adding it until it becomes necessary.
Set Operations 3.2
30module set.operations
The fundamental operation over sets is forming the set of all elements with a certain property. We discussed previously that this set does not always exist, however the iota operator allows us to define notation for it which will have the expected properties if it does exist.
6notation comprehension
7 term ::= "{" x:@binding(term) " | " sentence(x) "}"
8end
10definition
11 {x | p(x)} := ℩y, ∀x, x ∈ y ↔ p(x)
12end
We want to prove that if the set exists, then the notation we have given for it will refer to that set. We need to invoke the iota axiom from the previous chapter.
18theorem uncomp.def [p(_) : sentence(term)] : (∃x, ∀y, y ∈ x ↔ p(y))
19 |- ∀y, y ∈ {x | p(x)} ↔ p(y)
20proof
21 -- this property is essentially the definition of {x | p(x)} so we just
22 -- need to extract it using iota.unique. to do this we need that
23 -- the set is unique.
24 suffices ∃!x, ∀y, y ∈ x ↔ p(y) by iota.unique [∀y, y ∈ _ ↔ p(y)];
25
26 -- we can unwrap the definition of ∃!. this step is by definition.
27 suffices (∃x, ∀y, y ∈ x ↔ p(y)) ∧ (∃*x, ∀y, y ∈ x ↔ p(y));
28
29 -- we already have the lhs as a hypothesis.
30 suffices ∃*x, ∀y, y ∈ x ↔ p(y) by and.intro [∃x, ∀y, y ∈ x ↔ p(y)] [∃*x, ∀y, y ∈ x ↔ p(y)];
31
32 -- now we unwrap the definition of ∃*.
33 suffices ∀a, ∀b, (∀y, y ∈ a ↔ p(y)) ∧ (∀y, y ∈ b ↔ p(y)) → a = b;
34
35 -- let's extract all the pieces of this definition.
36 arbitrary a;
37 arbitrary b;
38 assume (∀y, y ∈ a ↔ p(y)) ∧ (∀y, y ∈ b ↔ p(y));
39 thus ∀y, y ∈ a ↔ p(y) by and.elim_left [∀y, y ∈ a ↔ p(y)] [∀y, y ∈ b ↔ p(y)];
40 thus ∀y, y ∈ b ↔ p(y) by and.elim_right [∀y, y ∈ a ↔ p(y)] [∀y, y ∈ b ↔ p(y)];
41
42 -- now we can prove the equality using extensionality.
43 suffices ∀x, x ∈ a ↔ x ∈ b as
44 follows ∀a, ∀b, (∀x, x ∈ a ↔ x ∈ b) → a = b by zfc.extensionality;
45 thus ∀b, (∀x, x ∈ a ↔ x ∈ b) → a = b specializing ∀a, ∀b, (∀x, x ∈ a ↔ x ∈ b) → a = b;
46 thus (∀x, x ∈ a ↔ x ∈ b) → a = b specializing ∀b, (∀x, x ∈ a ↔ x ∈ b) → a = b;
47 thus a = b by modus_ponens [∀x, x ∈ a ↔ x ∈ b] [a = b];
48 ;
49
50 arbitrary x;
51
52 -- We can use the transitivity of ↔ to finish the proof.
53 follows x ∈ a ↔ p(x) specializing ∀y, y ∈ a ↔ p(y);
54 follows x ∈ b ↔ p(x) specializing ∀y, y ∈ b ↔ p(y);
55 thus p(x) ↔ x ∈ b by iff.symm [x ∈ b] [p(x)];
56 thus x ∈ a ↔ x ∈ b by iff.trans [x ∈ a] [p(x)] [x ∈ b];
57qed
Sorry, was that painful to read? It was painful to write. That proof wasn't actually very complicated but it was 40 lines long anyway. This is not sustainable. Lucky we have something to help. Vampire is an automated theorem prover. It will find proofs of mathematical facts automatically. We can make a new tactic that sends the current known facts and goal to Vampire to have it generate a proof. This proof is then translated for Watson to understand. This is a very complex but also very powerful tactic which eliminates the need for tedious manipulations.
68tactic justification.logically
69 justification ::= @kw"logically"
70end
At this point we are also going to start doing more complex mathematics so it will helpful to add a few more useful tactics.
Sometimes it is helpful to annotate exactly which hypotheses go into an
application of a theorem. We will add given as a justification which uses
Vampire like logically but also checks that Vampire uses the given hypotheses.
79grammar_category sentence_list
81tactic sentence_list.one sentence_list ::= sentence:@fragment(sentence) end
82tactic sentence_list.many sentence_list ::= sentence:@fragment(sentence) @kw"and" rest:sentence_list end
84grammar_category givens
86tactic givens.none givens ::= end
87tactic givens.some givens ::= @kw"given" sentences:sentence_list end
89tactic justification.given
90 justification ::= @kw"given" givens:sentence_list
91end
We will also extend the by tactic to use Vampire to apply the provided theorem.
Note that Vampire can't do second order reasoning so this won't work with any
theorems that contain templates more complex than unparameterized terms.
97grammar_category theorem_list
99tactic theorem_list.one theorem_list ::= thm:@name end
100tactic theorem_list.many theorem_list ::= thm:@name "," rest:theorem_list end
102tactic justification.by.vampire
103 -- bind stronger than the original to override it.
104 justification (600) ::= @kw"by" thms:theorem_list givens:givens
105end
107tactic justification.by_def
108 justification ::= @kw"by_def" sentence:@fragment(sentence)
109end
If we want to have Vampire use a theorem multiple times the recall tactic
will add the statement of the theorem to the current proof state, making it so
Vampire can use it in all future proofs.
115tactic tactic.recall
116 tactic ::= @kw"recall" thm:@name ";" next:tactic
117end
We will also add the done tactic which is just an alias for using a
justification to prove the current goal instead of a tactic. This is equivalent
to thus goal <just>.
123tactic tactic.done
124 tactic ::= @kw"done" just:justification
125end
We will also add a cases tactic. This is a little more complex then just
splitting an or. By default, Vampire is used to prove this disjunction of all
the case conditions. Or a separate justification can be provided for this
purpose. Then the provided tactics are used to prove each case implies the
original goal.
133grammar_category case_list
134grammar_category case
136tactic case_list.one case_list ::= c:case end
137tactic case_list.many case_list ::= c:case rest:case_list end
139tactic case
140 case ::= "|" sentence:@fragment(sentence) @kw"then" tactic:tactic
141end
143tactic tactic.cases
144 tactic ::= @kw"cases" just:justification ":" cases:case_list
145end
The final new tactic we will add is the let tactic. This allows making new
definitions inside a proof. These definitions will be invisible to Vampire so
adding them won't effect reasoning at all.
151tactic tactic.let
152 tactic ::= @kw"let" name:@name ":=" frag:@fragment(term) ";" next:tactic
153end
The Subset Relation
The other fundamental relationship between sets, besides equality, is the subset relation.
161notation subset
162 sentence (500) ::= term " ⊆ " term
163end
165definition
166 a ⊆ b := ∀x, x ∈ a → x ∈ b
167end
169theorem sub.def [a b : term] :
170 |- a ⊆ b ↔ ∀x, x ∈ a → x ∈ b
171proof
172 done by iff.refl [a ⊆ b]
173qed
The subset relation is both reflexive and transitive.
177theorem sub.refl [a : term] :
178 |- a ⊆ a
179proof
180 suffices ∀x, x ∈ a → x ∈ a by sub.def;
181 done logically
182qed
184theorem sub.trans [a b c : term] : (a ⊆ b) (b ⊆ c)
185 |- a ⊆ c
186proof
187 follows ∀x, x ∈ a → x ∈ b by sub.def given a ⊆ b;
188 follows ∀x, x ∈ b → x ∈ c by sub.def given b ⊆ c;
189 thus ∀x, x ∈ a → x ∈ c logically;
190 done by sub.def
191qed
We also have that if two sets are subsets of each other then they are equal. In fact, this is just a restatement of the extensionality axiom.
196theorem sub.sub_eq [a b : term] : (a ⊆ b) (b ⊆ a)
197 |- a = b
198proof
199 follows ∀x, x ∈ a → x ∈ b by sub.def given a ⊆ b;
200 follows ∀x, x ∈ b → x ∈ a by sub.def given b ⊆ a;
201 thus ∀x, x ∈ a ↔ x ∈ b logically;
202 thus a = b by zfc.extensionality;
203qed
We can also have the notion of a strict subset.
207notation strict_subset
208 sentence (500) ::= term " ⊂ " term
209end
211@[reducible]
212definition
213 a ⊂ b := a ⊆ b ∧ a ≠ b
214end
216theorem ssub.def [a b : term] :
217 |- a ⊂ b ↔ (a ⊆ b ∧ a ≠ b)
218proof
219 done by iff.refl [a ⊂ b]
220qed
Bounded Quantifiers
When defining the subset relation we wrote . The component makes the quantifier only meaningful for elements of the set . This is a very common pattern so we will define shorthand notation for it.
229notation forall.bounded
230 sentence (000) ::= "∀" x:@binding(term) " ∈ " term ", " sentence(x)
231end
233@[reducible]
234definition
235 ∀x ∈ X, p(x) := ∀x, x ∈ X → p(x)
236end
Note that for the existential quantifier we use instead of because we are looking for an element that is both in the set and satisfies the property.
242notation exists.bounded
243 sentence (000) ::= "∃" x:@binding(term) " ∈ " term ", " sentence(x)
244end
246@[reducible]
247definition
248 ∃x ∈ X, p(x) := ∃x, x ∈ X ∧ p(x)
249end
The Empty Set
Returning to mathematics, we can use the unrestricted comprehension syntax to define our first concrete set, the empty set.
256notation empty_set
257 term ::= "∅"
258end
260definition
261 ∅ := {x | ⊥}
262end
The empty set axiom tells us that this set actually exists.
266theorem empty.def :
267 |- ∀x, x ∉ ∅
268proof
269 -- expand the definition of ∅
270 suffices ∀x, x ∉ {x | ⊥};
271 -- existence from the axiom
272 follows ∃x, ∀y, y ∉ x by zfc.empty_set;
273 thus ∃x, ∀y, (y ∈ x ↔ ⊥) logically;
274 -- and then set comprehension is always unique
275 thus ∀y, (y ∈ {x | ⊥} ↔ ⊥) by uncomp.def [⊥];
276 thus ∀y, y ∉ {x | ⊥} logically;
277qed
We can also characterize a non-empty set as one containing an element.
281theorem nonempty.has_element [a : term] :
282 |- a ≠ ∅ ↔ ∃x, x ∈ a
283proof
284 follows ∀x, x ∉ ∅ by empty.def;
285 follows a = ∅ ↔ ∀x, x ∉ a by zfc.extensionality;
286 thus a ≠ ∅ ↔ ¬∀x, x ∉ a logically;
287 thus a ≠ ∅ ↔ ∃x, x ∈ a logically;
288qed
The empty set is a subset of any set.
292theorem empty.is_sub [a : term] :
293 |- ∅ ⊆ a
294proof
295 follows ∀x, x ∉ ∅ by empty.def;
296 thus ∀x, x ∈ ∅ → x ∈ a logically;
297qed
Every subset of the empty set is the empty set.
301theorem empty.sub_is_empty [a : term] : (a ⊆ ∅)
302 |- a = ∅
303proof
304 follows ∀x, x ∈ a → x ∈ ∅ by sub.def;
305 follows ∀x, x ∉ ∅ by empty.def;
306 thus ¬∃x, x ∈ a logically;
307 thus a = ∅ by zfc.extensionality;
308qed
The Unordered Pair
We can develop the pair set in an essentially identical way.
314notation pair
315 term ::= "{" term ", " term "}"
316end
318definition
319 {a, b} := {x | x = a ∨ x = b}
320end
This time it is the pairing axiom that tells us that this set exists.
324theorem pair.def [a b : term] :
325 |- ∀x, x ∈ {a, b} ↔ (x = a ∨ x = b)
326proof
327 suffices ∀x, x ∈ {y | y = a ∨ y = b} ↔ (x = a ∨ x = b);
328 follows ∃c, ∀x, x ∈ c ↔ (x = a ∨ x = b) by zfc.pairing;
329 thus ∀x, x ∈ {y | y = a ∨ y = b} ↔ (x = a ∨ x = b) by uncomp.def [_ = a ∨ _ = b];
330qed
The unordered pair is unordered. That is, it is symmetric.
334theorem pair.symm [a b : term] :
335 |- {a, b} = {b, a}
336proof
337 thus ∀x, x ∈ {a, b} ↔ x ∈ {b, a} by pair.def;
338 thus {a, b} = {b, a} by zfc.extensionality;
339qed
The unordered pair being a subset is equivalent to both elements of the pair being members of the set.
344theorem pair.sub [a b A : term] :
345 |- (a ∈ A ∧ b ∈ A) ↔ {a, b} ⊆ A
346proof
347 done by sub.def, pair.def
348qed
It is also non-empty.
352theorem pair.non_empty [a b : term] :
353 |- {a, b} ≠ ∅
354proof
355 follows a ∈ {a, b} by pair.def;
356 thus {a, b} ≠ ∅ by empty.def;
357qed
The Singleton Set
We can define the singleton set as the pair of the same element twice. We could define it as simply but how would we prove this set exists? We would have to appeal to the pairing axiom anyway.
365notation singleton
366 term ::= "{" term "}"
367end
369definition
370 {a} := {a, a}
371end
373theorem singleton.def [a : term] :
374 |- ∀x, x ∈ {a} ↔ x = a
375proof
376 suffices ∀x, x ∈ {a, a} ↔ x = a;
377 thus ∀x, x ∈ {a, a} ↔ x = a by pair.def;
378qed
An element being in a set is equivalent to the singleton set being a subset.
382theorem singleton.sub [a A : term] :
383 |- a ∈ A ↔ {a} ⊆ A
384proof
385 follows a ∈ A → (∀x, x ∈ {a} → x ∈ A) by singleton.def;
386 follows (∀x, x ∈ {a} → x ∈ A) → a ∈ A by singleton.def;
387 done by sub.def
388qed
Restricted Comprehension
In contrast to unrestricted comprehensions, which are not always sets, a comprehension which is limited to be a subset of another set always exists. This is guaranteed by the specification axiom.
396notation restricted_comprehension
397 term ::= "{" x:@binding(term) " ∈ " term " | " sentence(x) "}"
398end
400definition
401 {x ∈ X | p(x)} := {x | x ∈ X ∧ p(x)}
402end
This proof follows from the specification axiom.
406theorem comp.def [p(_) : sentence(term)] [X : term] :
407 |- ∀y, y ∈ {x ∈ X | p(x)} ↔ (y ∈ X ∧ p(y))
408proof
409 suffices ∀y, y ∈ {x | x ∈ X ∧ p(x)} ↔ (y ∈ X ∧ p(y));
410 hence ∀a, ∃x, ∀y, y ∈ x ↔ (y ∈ a ∧ p(y)) by zfc.specification [p(_)];
411 follows ∃x, ∀y, y ∈ x ↔ (y ∈ X ∧ p(y)) logically;
412 thus ∀y, y ∈ {x | x ∈ X ∧ p(x)} ↔ (y ∈ X ∧ p(y)) by uncomp.def [_ ∈ X ∧ p(_)];
413qed
It easily follows from this definition that a restricted comprehension is always a subset of the original set.
418theorem comp.sub [p(_) : sentence(term)] [X : term] :
419 |- {x ∈ X | p(x)} ⊆ X
420proof
421 follows ∀y, y ∈ {x ∈ X | p(x)} ↔ (y ∈ X ∧ p(y)) by comp.def [p(_)] [X];
422 thus ∀y, y ∈ {x ∈ X | p(x)} → y ∈ X logically;
423qed
Because comp.def is a second order theorem, that is it is schematized over
all predicates , Vampire cannot reason with it automatically. This is why we
had to manually provide the template instantiations when we invoked it.
Restricted comprehension comes up so frequently and invoking second order
theorems is so tedious that we are just going to hard code this theorem so that
it is automatically given to Vampire any time a comprehension appears in the
local context.
The Set Map
TODO
437notation term.with_term
438 term (1000) ::= @name "(" term ")"
439end
441notation set_map
442 term ::= "{" term(x) " | " x:@binding(term) " ∈ " term "}"
443end
445definition
446 {f(x) | x ∈ A} := {y | ∃x, x ∈ A ∧ y = f(x)}
447end
The proof follows from the replacement axiom and the definition of the set map.
451theorem set_map.def [f(_) : term(term)] [A : term] :
452 |- ∀y, y ∈ {f(x) | x ∈ A} ↔ (∃x, x ∈ A ∧ y = f(x))
453proof
454 suffices ∀y, y ∈ {z | ∃x, x ∈ A ∧ z = f(x)} ↔ (∃x, x ∈ A ∧ y = f(x));
455 suffices (∃x, ∀y, y ∈ x ↔ ∃x, x ∈ A ∧ y = f(x)) by uncomp.def [∃x, x ∈ A ∧ _ = f(x)];
456 hence ∀x ∈ A, ∃!y, y = f(x) logically;
457 follows ∀a, (∀x, x ∈ a → ∃!y, y = f(x)) → (∃x, ∀y, y ∈ x ↔ (∃z, z ∈ a ∧ y = f(z))) by zfc.replacement [_1 = f(_0)];
458 done logically
459qed
Unions
We can return to defining new sets with the union of a set.
465notation big_union
466 term (000) ::= "⋃" term
467end
469definition
470 ⋃a := {x | ∃y, x ∈ y ∧ y ∈ a}
471end
Once more the existence of this set is guaranteed by the union axiom of ZFC.
475theorem big_union.def [a : term] :
476 |- ∀x, x ∈ ⋃a ↔ (∃y, x ∈ y ∧ y ∈ a)
477proof
478 suffices ∀x, x ∈ {x | ∃y, x ∈ y ∧ y ∈ a} ↔ (∃y, x ∈ y ∧ y ∈ a);
479 follows ∃x, ∀y, y ∈ x ↔ (∃z, y ∈ z ∧ z ∈ a) by zfc.union;
480 follows ∀x, x ∈ {x | ∃y, x ∈ y ∧ y ∈ a} ↔ (∃y, x ∈ y ∧ y ∈ a) by uncomp.def [∃y, _ ∈ y ∧ y ∈ a];
481qed
Any element of a set is a subset of the union of that set.
485theorem big_union.super [a b : term] : (a ∈ b)
486 |- a ⊆ ⋃b
487proof
488 follows ∀x, (∃y, x ∈ y ∧ y ∈ b) ↔ x ∈ ⋃b by big_union.def;
489 thus ∀x, x ∈ a → x ∈ ⋃b logically;
490qed
Next, we show that the union of a singleton is the element of the singleton.
494theorem big_union.singleton [a : term] :
495 |- ⋃{a} = a
496proof
497 follows ∀x, x ∈ {a} ↔ x = a by singleton.def;
498 hence ∀x, x ∈ ⋃{a} ↔ (∃y, x ∈ y ∧ y ∈ {a}) by big_union.def [{a}];
499 thus ∀x, x ∈ ⋃{a} ↔ (∃y, x ∈ y ∧ y = a) logically;
500 follows ∀x, x ∈ ⋃{a} ↔ (∃y, x ∈ a) logically;
501 follows ∀x, x ∈ ⋃{a} ↔ x ∈ a logically;
502 done by zfc.extensionality
503qed
We can define the regular union using the pair and the big union. Once again, although we could define this directly using unrestricted comprehension, it is easier to do it this way to avoid repeated proofs of existence.
508notation union
509 term (650>) ::= term " ∪ " term
510end
512definition
513 a ∪ b := ⋃{a, b}
514end
The definition of the union can be easily proved from the definitions of the big union and the pair.
519theorem union.def [a b : term] :
520 |- ∀x, x ∈ a ∪ b ↔ (x ∈ a ∨ x ∈ b)
521proof
522 suffices ∀x, x ∈ ⋃{a, b} ↔ (x ∈ a ∨ x ∈ b);
523 follows ∀x, x ∈ ⋃{a, b} ↔ ∃y, x ∈ y ∧ y ∈ {a, b} by big_union.def;
524 follows ∀y, y ∈ {a, b} ↔ (y = a ∨ y = b) by pair.def;
525 done logically
526qed
The union operator is also symmetric. This follows either from the fact that the unordered pair is symmetric, or just the symmetry of or itself.
531theorem union.symm [a b : term] :
532 |- a ∪ b = b ∪ a
533proof
534 follows ∀x, x ∈ a ∪ b ↔ (x ∈ a ∨ x ∈ b) by union.def;
535 follows ∀x, x ∈ b ∪ a ↔ (x ∈ a ∨ x ∈ b) by union.def;
536 thus a ∪ b = b ∪ a by zfc.extensionality;
537qed
The union is also associative. This follows from the associativity of or.
541theorem union.assoc [a b c : term] :
542 |- a ∪ (b ∪ c) = (a ∪ b) ∪ c
543proof
544 follows ∀x, x ∈ a ∪ (b ∪ c) ↔ (x ∈ a ∨ (x ∈ b ∨ x ∈ c)) by union.def;
545 follows ∀x, x ∈ (a ∪ b) ∪ c ↔ ((x ∈ a ∨ x ∈ b) ∨ x ∈ c) by union.def;
546 thus a ∪ (b ∪ c) = (a ∪ b) ∪ c by zfc.extensionality;
547qed
Either set in the union is a subset of the union as a whole. These facts are really just simplifications of the defining fact.
552theorem union.left_sub [a b : term] :
553 |- a ⊆ a ∪ b
554proof
555 follows ∀x, (x ∈ a ∨ x ∈ b) ↔ x ∈ a ∪ b by union.def;
556 thus ∀x, x ∈ a → x ∈ a ∪ b logically;
557qed
559theorem union.right_sub [a b : term] :
560 |- b ⊆ a ∪ b
561proof
562 follows ∀x, (x ∈ a ∨ x ∈ b) ↔ x ∈ a ∪ b by union.def;
563 thus ∀x, x ∈ b → x ∈ a ∪ b logically;
564qed
Intersections
Instead of defining the big intersection with an unrestricted comprehension as we did for the big union, we will define it as a subset of the union. This makes it easier to prove existence.
572notation big_inter
573 term (000) ::= "⋂" term
574end
576definition
577 ⋂a := {x ∈ ⋃a | ∀y, y ∈ a → x ∈ y}
578end
This definition implies that the intersection of the empty set is the empty set. However, based on the defining property of the intersection, the intersection of the empty set should be the proper class of all sets, which isn't a set. So we restrict the definition theorem to only applying to non-empty sets.
585theorem big_inter.def [a : term] : (a ≠ ∅)
586 |- ∀x, x ∈ ⋂a ↔ (∀y, y ∈ a → x ∈ y)
587proof
588 arbitrary x;
589 suffices x ∈ {z ∈ ⋃a | ∀y, y ∈ a → z ∈ y} ↔ (∀y, y ∈ a → x ∈ y);
590
591 assume x ∈ {z ∈ ⋃a | ∀y, y ∈ a → z ∈ y} then ∀y, y ∈ a → x ∈ y logically;
592
593 assume ∀y, y ∈ a → x ∈ y then x ∈ {z ∈ ⋃a | ∀y, y ∈ a → z ∈ y} as
594 obtain y st y ∈ a by nonempty.has_element;
595 follows x ∈ y logically;
596 thus x ∈ ⋃a by big_union.def;
597 done logically
598 ;
599
600 done logically
601qed
The big intersection of a set is a subset of every element of the set.
605theorem big_inter.sub [a b : term] : (a ∈ b)
606 |- ⋂b ⊆ a
607proof
608 follows b ≠ ∅ by nonempty.has_element;
609 follows ∀x, x ∈ ⋂b ↔ (∀y, y ∈ b → x ∈ y) by big_inter.def;
610 thus ∀x, x ∈ ⋂b → x ∈ a logically;
611qed
We define the small intersection the same way we defined the small union.
615notation inter
616 term (700) ::= term " ∩ " term
617end
619definition
620 a ∩ b := ⋂{a, b}
621end
Since the pair set is always non-empty, the small intersection is always well defined.
626theorem inter.def [a b : term] :
627 |- ∀x, x ∈ a ∩ b ↔ (x ∈ a ∧ x ∈ b)
628proof
629 suffices ∀x, x ∈ ⋂{a, b} ↔ (x ∈ a ∧ x ∈ b);
630
631 -- we need that the pair set isn't empty to apply big_inter.def.
632 follows {a, b} ≠ ∅ by pair.non_empty;
633 follows ∀x, x ∈ ⋂{a, b} ↔ (∀y, y ∈ {a, b} → x ∈ y) by big_inter.def;
634 follows ∀y, y ∈ {a, b} ↔ (y = a ∨ y = b) by pair.def;
635 thus ∀x, x ∈ ⋂{a, b} ↔ (x ∈ a ∧ x ∈ b) logically;
636qed
Like the union, the intersection is symmetric and associative. The proofs are identical to those for union, just replacing every with an .
641theorem inter.symm [a b : term] :
642 |- a ∩ b = b ∩ a
643proof
644 follows ∀x, x ∈ a ∩ b ↔ (x ∈ a ∧ x ∈ b) by inter.def;
645 follows ∀x, x ∈ b ∩ a ↔ (x ∈ a ∧ x ∈ b) by inter.def;
646 thus a ∩ b = b ∩ a by zfc.extensionality;
647qed
649theorem inter.assoc [a b c : term] :
650 |- a ∩ (b ∩ c) = (a ∩ b) ∩ c
651proof
652 follows ∀x, x ∈ a ∩ (b ∩ c) ↔ (x ∈ a ∧ (x ∈ b ∧ x ∈ c)) by inter.def;
653 follows ∀x, x ∈ (a ∩ b) ∩ c ↔ ((x ∈ a ∧ x ∈ b) ∧ x ∈ c) by inter.def;
654 thus a ∩ (b ∩ c) = (a ∩ b) ∩ c by zfc.extensionality;
655qed
The intersection of two sets is a subset of both of the original sets.
659theorem inter.sub_left [a b : term] :
660 |- a ∩ b ⊆ a
661proof
662 follows ∀x, x ∈ a ∩ b ↔ (x ∈ a ∧ x ∈ b) by inter.def;
663 thus ∀x, x ∈ a ∩ b → x ∈ a logically;
664qed
666theorem inter.sub_right [a b : term] :
667 |- a ∩ b ⊆ b
668proof
669 follows ∀x, x ∈ a ∩ b ↔ (x ∈ a ∧ x ∈ b) by inter.def;
670 thus ∀x, x ∈ a ∩ b → x ∈ b logically;
671qed
673theorem inter.left_sub [a b c : term] : (c ⊆ a ∩ b)
674 |- c ⊆ a
675proof
676 follows ∀x, x ∈ c → x ∈ a ∧ x ∈ b by inter.def, sub.def given c ⊆ a ∩ b;
677 follows ∀x, x ∈ c → x ∈ a logically;
678qed
680theorem inter.right_sub [a b c : term] : (c ⊆ a ∩ b)
681 |- c ⊆ b
682proof
683 follows ∀x, x ∈ c → x ∈ a ∧ x ∈ b by inter.def, sub.def given c ⊆ a ∩ b;
684 follows ∀x, x ∈ c → x ∈ b logically;
685qed
687theorem inter.both_sub [a b c : term] : (a ⊆ c) (b ⊆ c)
688 |- a ∩ b ⊆ c
689proof
690 suffices ∀x, x ∈ a ∧ x ∈ b → x ∈ c by inter.def, sub.def;
691 follows ∀x, x ∈ a → x ∈ c by sub.def given a ⊆ c;
692 follows ∀x, x ∈ b → x ∈ c by sub.def given b ⊆ c;
693 done logically
694qed
696theorem inter.sub_both [a b c : term] : (c ⊆ a) (c ⊆ b)
697 |- c ⊆ a ∩ b
698proof
699 suffices ∀x, x ∈ c → x ∈ a ∧ x ∈ b by inter.def, sub.def;
700 follows ∀x, x ∈ c → x ∈ a by sub.def given c ⊆ a;
701 follows ∀x, x ∈ c → x ∈ b by sub.def given c ⊆ b;
702 done logically
703qed
The Set Difference
We define the difference between two sets as the set of elements of the first set which are not in the second set.
709notation set_difference
710 term (700) ::= term " - " term
711end
713definition
714 a - b := {x ∈ a | x ∉ b}
715end
Since we used a restricted comprehension, the defining property follows directly without any more existence proofs.
720theorem set_diff.def [a b : term] :
721 |- ∀x, x ∈ a - b ↔ (x ∈ a ∧ x ∉ b)
722proof
723 suffices ∀x, x ∈ {y ∈ a | y ∉ b} ↔ (x ∈ a ∧ x ∉ b);
724 -- remember we gave Vampire the power to understand restricted comprehensions.
725 done logically
726qed
The set difference is a subset of the first set. This follows from the fact that all restricted comprehensions are subsets.
731theorem set_diff.sub [a b : term] :
732 |- a - b ⊆ a
733proof
734 suffices {x ∈ a | x ∉ b} ⊆ a;
735 done by comp.sub [_ ∉ b] [a]
736qed
We can also characterize a non-empty difference.
740theorem set_diff.non_empty [a b : term] : (b ⊆ a)
741 |- a - b ≠ ∅ ↔ a ≠ b
742proof
743 assume a - b ≠ ∅ then a ≠ b as
744 obtain x st x ∈ a - b by nonempty.has_element;
745 thus x ∈ a ∧ x ∉ b by set_diff.def;
746 thus a ≠ b by zfc.extensionality;
747 ;
748
749 assume a ≠ b then a - b ≠ ∅ as
750 obtain x st (x ∈ a ∧ x ∉ b) ∨ (x ∈ b ∧ x ∉ a) by zfc.extensionality;
751 follows ¬(x ∈ b ∧ x ∉ a) by sub.def;
752 thus x ∈ a ∧ x ∉ b logically;
753 thus x ∈ a - b by set_diff.def;
754 thus a - b ≠ ∅ by nonempty.has_element;
755 ;
756
757 done logically
758qed
760theorem set_diff.anti [a X Y : term] : (X ⊆ Y)
761 |- a - Y ⊆ a - X
762proof
763 suffices ∀x, x ∈ a - Y → x ∈ a - X by sub.def;
764 done by set_diff.def, sub.def
765qed
767theorem set_diff.double [a S : term] : (S ⊆ a)
768 |- a - (a - S) = S
769proof
770 follows ∀x, x ∈ a - (a - S) ↔ (x ∈ a ∧ x ∉ a - S) by set_diff.def;
771 follows ∀x, x ∈ a - S ↔ (x ∈ a ∧ x ∉ S) by set_diff.def;
772 follows ∀x, x ∈ a - (a - S) ↔ x ∈ S by sub.def;
773 done by zfc.extensionality
774qed
776theorem set_diff.union [a S : term] : (S ⊆ a)
777 |- S ∪ (a - S) = a
778proof
779 hence ∀x, x ∈ S ∪ (a - S) ↔ x ∈ S ∨ x ∈ a - S by union.def;
780 follows ∀x, x ∈ a - S ↔ (x ∈ a ∧ x ∉ S) by set_diff.def;
781 thus ∀x, x ∈ S ∨ x ∈ a - S ↔ (x ∈ S ∨ (x ∈ a ∧ x ∉ S)) logically;
782 furthermore ∀x, (x ∈ S ∨ (x ∈ a ∧ x ∉ S)) ↔ ((x ∈ S ∨ x ∈ a) ∧ (x ∈ S ∨ x ∉ S)) logically;
783 hence ∀x, ((x ∈ S ∨ x ∈ a) ∧ (x ∈ S ∨ x ∉ S)) ↔ x ∈ S ∨ x ∈ a logically;
784 indeed ∀x, x ∈ S ∨ x ∈ a ↔ x ∈ a by sub.def given S ⊆ a;
785 done by zfc.extensionality
786qed
788theorem set_diff.disjoint [a S : term] :
789 |- S ∩ (a - S) = ∅
790proof
791 follows ∀x, x ∈ S ∩ (a - S) ↔ x ∈ S ∧ x ∈ (a - S) by inter.def;
792 follows ∀x, x ∈ a - S ↔ (x ∈ a ∧ x ∉ S) by set_diff.def;
793 hence ∀x, x ∈ S ∧ x ∈ a - S ↔ (x ∈ S ∧ x ∈ a ∧ x ∉ S) logically;
794 furthermore ∀x, (x ∈ S ∧ x ∈ a ∧ x ∉ S) ↔ ⊥ logically;
795 follows ∀x, x ∉ S ∩ (a - S) logically;
796 done by zfc.extensionality, empty.def
797qed
The Powerset
We will define the powerset as the set of all subsets of a set.
803definition
804 𝒫(a) := {x | x ⊆ a}
805end
The existence of this set is provided by one of the ZFC axioms in the same manner as before.
810theorem powset.def [a : term] :
811 |- ∀x, x ∈ 𝒫(a) ↔ x ⊆ a
812proof
813 suffices ∀x, x ∈ {y | y ⊆ a} ↔ x ⊆ a;
814 follows ∃b, ∀x, x ∈ b ↔ (∀y, y ∈ x → y ∈ a) by zfc.powerset;
815 thus ∃b, ∀x, x ∈ b ↔ x ⊆ a;
816 thus ∀x, x ∈ {y | y ⊆ a} ↔ x ⊆ a by uncomp.def [_ ⊆ a];
817qed
The singletons and pairs of elements from the original set are both examples of sets in the powerset.
822theorem powset.singleton_in [a A : term] : (a ∈ A)
823 |- {a} ∈ 𝒫(A)
824proof
825 follows {a} ⊆ A by singleton.sub;
826 thus {a} ∈ 𝒫(A) by powset.def;
827qed
829theorem powset.pair_in [a b A : term] : (a ∈ A) (b ∈ A)
830 |- {a, b} ∈ 𝒫(A)
831proof
832 follows {a, b} ⊆ A by pair.sub;
833 thus {a, b} ∈ 𝒫(A) by powset.def;
834qed
If
Using restricted comprehensions we can define the if then else operator. This will be useful for casewise definitions.
841notation if
842 term ::= "if " sentence " then " term " else " term
843end
845definition
846 if p then a else b := {x ∈ a | p} ∪ {x ∈ b | ¬p}
847end
849theorem union.empty [a : term] :
850 |- a ∪ ∅ = a
851proof
852 hence ∀x, x ∈ a ∪ ∅ ↔ (x ∈ a ∨ x ∈ ∅) by union.def;
853 thus ∀x, x ∉ ∅ by empty.def;
854 done by zfc.extensionality
855qed
857theorem empty.union [a : term] :
858 |- ∅ ∪ a = a
859proof
860 done by union.empty, union.symm
861qed
863theorem if.true [p : sentence] [a b : term] : (p)
864 |- if p then a else b = a
865proof
866 suffices {x ∈ a | p} ∪ {x ∈ b | ¬p} = a;
867 follows {x ∈ a | p} = a given p;
868 follows {x ∈ b | ¬p} = ∅ by empty.def given p;
869 follows a ∪ ∅ = a by union.empty;
870 done logically
871qed
873theorem if.false [p : sentence] [a b : term] : (¬p)
874 |- if p then a else b = b
875proof
876 suffices {x ∈ a | p} ∪ {x ∈ b | ¬p} = b;
877 follows {x ∈ a | p} = ∅ by empty.def given ¬p;
878 follows {x ∈ b | ¬p} = b given ¬p;
879 follows ∅ ∪ b = b by empty.union;
880 done logically
881qed
883theorem if.swap [p : sentence] [a b : term] :
884 |- if p then a else b = if ¬p then b else a
885proof
886 cases:
887 | p then
888 follows if p then a else b = a by if.true [p] [a] [b];
889 follows ¬¬p logically; -- TODO: use vampire for this.
890 follows if ¬p then b else a = a by if.false [¬p] [b] [a];
891 done logically
892 | ¬p then
893 follows if p then a else b = b by if.false [p] [a] [b];
894 follows if ¬p then b else a = b by if.true [¬p] [b] [a];
895 done logically
896qed
898theorem tarski_fixed_point [A : term] [p(_) : term(term)] :
899 (∀X, ∀Y, X ⊆ Y → p(X) ⊆ p(Y)) (∀X, p(X) ⊆ A)
900 |- ∃C, C ⊆ A ∧ C = p(C)
901proof
902 let C := {a ∈ A | ∃X ∈ 𝒫(A), X ⊆ p(X) ∧ a ∈ X};
903 follows ∀a, a ∈ C ↔ (a ∈ A ∧ ∃X ∈ 𝒫(A), X ⊆ p(X) ∧ a ∈ X)
904 by comp.def [∃X ∈ 𝒫(A), X ⊆ p(X) ∧ _ ∈ X] [A];
905 -- every post-fixed point of φ is contained in C, since it witnesses its own
906 -- members' membership in C.
907 thus ∀X, X ∈ 𝒫(A) ∧ X ⊆ p(X) → X ⊆ C as
908 arbitrary X;
909 assume X ∈ 𝒫(A) ∧ X ⊆ p(X) then X ⊆ C as
910 suffices ∀a, a ∈ X → a ∈ C by sub.def;
911 arbitrary a;
912 assume a ∈ X then a ∈ C as
913 indeed X ⊆ A by powset.def;
914 follows a ∈ A by sub.def;
915 done logically
916 ;
917 done logically
918 ;
919 done logically
920 ;
921 -- C ⊆ φ(C): each a ∈ C sits in some post-fixed point X ⊆ C, and φ is monotone.
922 follows C ⊆ p(C) as
923 suffices ∀a, a ∈ C → a ∈ p(C) by sub.def;
924 arbitrary a;
925 assume a ∈ C then a ∈ p(C) as
926 obtain X st X ∈ 𝒫(A) ∧ X ⊆ p(X) ∧ a ∈ X logically;
927 follows X ⊆ C logically;
928 hence p(X) ⊆ p(C) logically;
929 done by sub.def
930 ;
931 done logically
932 ;
933 hence C ⊆ A by sub.trans;
934 indeed p(C) ⊆ A logically;
935 furthermore p(C) ∈ 𝒫(A) by powset.def;
936 thus p(C) ⊆ C logically;
937 done by sub.sub_eq
938qed
Functions 3.3
33module set.fn
The Ordered Pair
An ordered pair (a, b) is a set composed of a singleton {a} and a pair {a, b}. We can use ordered pairs to enforce certain structure on sets.
4notation ordered_pair
5 term ::= "⟨" term ", " term "⟩"
6end
8definition
9 ⟨a, b⟩ := {{a}, {a, b}}
10end
The proof follows from the pairing axiom and the definition of the ordered pair.
15theorem opair.def [a b : term] :
16 |- ∀x, x ∈ ⟨a, b⟩ ↔ (x = {a} ∨ x = {a, b})
17proof
18 suffices ∀x, x ∈ {{a}, {a, b}} ↔ (x = {a} ∨ x = {a, b});
19 follows ∃c, ∀x, x ∈ c ↔ (x = {a} ∨ x = {a, b}) by zfc.pairing;
20 thus ∀x, x ∈ {{a}, {a, b}} ↔ (x = {a} ∨ x = {a, b}) by uncomp.def [_ = {a} ∨ _ = {a, b}];
21qed
23theorem opair.unfold [a b : term] :
24 |- ⟨a, b⟩ = {{a}, {a, b}}
25proof
26 done by eq.refl [⟨a, b⟩]
27qed
Lets prove some basic properties of ordered pairs
31theorem opair.union [a b : term] :
32 |- ⋃⟨a, b⟩ = {a, b}
33proof
34 suffices ⋃{{a}, {a, b}} = {a, b};
35 thus ∀x, x ∈ {a, b} ↔ (x = a ∨ x = b) by pair.def;
36 thus ∀x, x ∈ ⋃{{a}, {a, b}} ↔ (x ∈ {a} ∨ x ∈ {a, b}) by union.def [{a}] [{a, b}];
37 hence ∀x, (x = a ∨ (x = a ∨ x = b)) ↔ (x = a ∨ x = b) logically;
38 follows ∀x, (x ∈ {a} ∨ x ∈ {a, b}) ↔ (x = a ∨ (x = a ∨ x = b)) by singleton.def, pair.def;
39 done by zfc.extensionality
40qed
42theorem opair.inter [a b : term] :
43 |- ⋂⟨a, b⟩ = {a}
44proof
45 suffices ⋂{{a}, {a, b}} = {a};
46 thus ∀x, x ∈ {a} ↔ x = a by singleton.def;
47 thus ∀x, x ∈ {a, b} ↔ (x = a ∨ x = b) by pair.def;
48 thus ∀x, x ∈ ⋂{{a}, {a, b}} ↔ (x ∈ {a} ∧ x ∈ {a, b}) by inter.def [{a}] [{a, b}];
49 hence ∀x, (x = a ∧ (x = a ∨ x = b)) ↔ x = a logically;
50 thus ∀x, x ∈ ⋂{{a}, {a, b}} ↔ x ∈ {a} by singleton.def;
51 follows ⋂{{a}, {a, b}} = {a} by zfc.extensionality;
52qed
Next, we define a function which gives us the first element of an ordered pair. We define this function somewhat broadly, but it allows for an easy proof.
56definition
57 π₁(a) := ⋃⋂a
58end
The proof follows from the definition of the ordered pair and many of the intersection properties we've shown.
62theorem opair_first.def [a b : term] :
63 |- π₁(⟨a, b⟩) = a
64proof
65 hence ⋂⟨a, b⟩ = {a} by opair.inter;
66 thus ⋃{a} = a by big_union.singleton;
67 hence ⋃⋂⟨a, b⟩ = a logically;
68qed
Naturally, we now define the second element of an ordered pair.
72definition
73 π₂(a) := ⋃{x ∈ ⋃a | ⋃a ≠ ⋂a → x ∉ ⋂a}
74end
This proof follows simply from the definition of the ordered pair and the properties of unions and intersections.
78theorem opair_second.def [a b : term] :
79 |- π₂(⟨a, b⟩) = b
80proof
81 suffices ⋃{x ∈ ⋃⟨a, b⟩ | ⋃⟨a, b⟩ ≠ ⋂⟨a, b⟩ → x ∉ ⋂⟨a, b⟩} = b;
82 follows ⋃⟨a, b⟩ = {a, b} by opair.union;
83 follows ⋂⟨a, b⟩ = {a} by opair.inter;
84 -- We can simplify our goal with our known facts for the union and intersection
85 hence ⋃{x ∈ ⋃⟨a, b⟩ | ⋃⟨a, b⟩ ≠ ⋂⟨a, b⟩ → x ∉ ⋂⟨a, b⟩}
86 = ⋃{x ∈ {a, b} | {a, b} ≠ {a} → x ∉ {a}} logically;
87 thus ∀x, x ∈ {a, b} ↔ (x = a ∨ x = b) by pair.def;
88 follows ∀x, x ∈ {a} ↔ x = a by singleton.def;
89 follows {a, b} ≠ {a} ↔ a ≠ b logically;
90 hence ∀x, ((x = a ∨ x = b) ∧ (a ≠ b → x ∉ {a})) ↔ x = b logically;
91 thus ∀x, x ∈ {x ∈ {a, b} | {a, b} ≠ {a} → x ∉ {a}} ↔ x = b by zfc.extensionality;
92 hence ∀x, x = b ↔ x ∈ {b} by singleton.def;
93 follows ∀x, x ∈ {x ∈ {a, b} | {a, b} ≠ {a} → x ∉ {a}} ↔ x ∈ {b} logically;
94 follows {x ∈ {a, b} | {a, b} ≠ {a} → x ∉ {a}} = {b} by zfc.extensionality;
95 -- so π₂(⟨a, b⟩) = ⋃{b} = b
96 hence ⋃{x ∈ {a, b} | {a, b} ≠ {a} → x ∉ {a}} = ⋃{b} logically;
97 done by big_union.singleton
98qed
Finally, we show that two ordered pairs are equal iff their first and second elements are equal.
102theorem opair.eq [a b c d : term] :
103 |- ⟨a, b⟩ = ⟨c, d⟩ ↔ (a = c ∧ b = d)
104proof
105 hence ⟨a, b⟩ = ⟨c, d⟩ → π₁(⟨a, b⟩) = π₁(⟨c, d⟩) by zfc.extensionality;
106 follows π₁(⟨a, b⟩) = π₁(⟨c, d⟩) ↔ a = c by opair_first.def;
107 follows ⟨a, b⟩ = ⟨c, d⟩ → π₂(⟨a, b⟩) = π₂(⟨c, d⟩) by zfc.extensionality;
108 follows π₂(⟨a, b⟩) = π₂(⟨c, d⟩) ↔ b = d by opair_second.def;
109 -- suffices ⟨a, b⟩ = ⟨c, d⟩ ↔ (a = c ∧ b = d);
110 hence ⟨a, b⟩ = ⟨c, d⟩ → (a = c ∧ b = d) logically;
111 hence (a = c ∧ b = d) → ⟨a, b⟩ = ⟨c, d⟩ logically;
112 done logically
113qed
The Cartesian Product
The Cartesian product of two sets is the set of all ordered pairs formed from the elements of those sets. A double powerset is sufficient to make a superset of the Cartesian product from which we can then restrict to get the required set.
122notation product
123 term (350) ::= term " × " term
124end
126definition
127 A × B := {x ∈ 𝒫(𝒫(A ∪ B)) | ∃a ∈ A, ∃b ∈ B, x = ⟨a, b⟩}
128end
The difficult task is to prove that this gives us every possible ordered pair.
132theorem cart_prod.def [A B : term] :
133 |- ∀x, x ∈ A × B ↔ ∃a ∈ A, ∃b ∈ B, x = ⟨a, b⟩
134proof
135 arbitrary x;
136
137 -- remember the definition of A × B. (specifically have Vampire remember it)
138 follows A × B = {x ∈ 𝒫(𝒫(A ∪ B)) | ∃a ∈ A, ∃b ∈ B, x = ⟨a, b⟩}
139 by eq.refl [A × B];
140
141 -- the forward direction is pretty simple. it just comes directly from the
142 -- definition of restricted comprehension.
143 assume x ∈ A × B then ∃a ∈ A, ∃b ∈ B, x = ⟨a, b⟩ logically;
144
145 -- the other direction is harder. it follows quickly that x satisfies the
146 -- comprehension condition, but it is a little more work to show it is in
147 -- the double powerset.
148 assume ∃a ∈ A, ∃b ∈ B, x = ⟨a, b⟩ then x ∈ A × B as
149 obtain a st a ∈ A and b st b ∈ B ∧ x = ⟨a, b⟩ logically;
150 follows x = {{a}, {a, b}} by_def x = ⟨a, b⟩;
151
152 -- we already have that x is a pair so we just need to prove it is in the powerset
153 suffices x ∈ 𝒫(𝒫(A ∪ B)) ∧ (∃a ∈ A, ∃b ∈ B, x = ⟨a, b⟩) logically;
154 suffices x ∈ 𝒫(𝒫(A ∪ B)) given x = ⟨a, b⟩;
155
156 follows a ∈ A ∪ B ∧ b ∈ A ∪ B by union.def given a ∈ A and b ∈ B;
157 thus {a} ∈ 𝒫(A ∪ B) by powset.singleton_in;
158 thus {a, b} ∈ 𝒫(A ∪ B) by powset.pair_in;
159 thus {{a}, {a, b}} ∈ 𝒫(𝒫(A ∪ B)) by powset.pair_in;
160 thus x ∈ 𝒫(𝒫(A ∪ B)) given x = {{a}, {a, b}};
161 ;
162
163 done logically
164qed
Next, we prove a useful result relating the cartesian product of sets to their subsets.
168lemma cart_prod.sub [A B C D : term] : (A ⊆ C) (B ⊆ D)
169 |- A × B ⊆ C × D
170proof
171 suffices ∀x ∈ A × B, x ∈ C × D;
172 arbitrary x;
173 assume x ∈ A × B then x ∈ C × D as
174 obtain a st a ∈ A and b st b ∈ B ∧ x = ⟨a, b⟩ by cart_prod.def;
175 follows a ∈ C by sub.def given A ⊆ C;
176 follows b ∈ D by sub.def given B ⊆ D;
177 done by cart_prod.def
178 ;
179 done logically
180qed
We can define the set of binary relations between two sets as the powerset of the Cartesian product of those two sets. Conceptually, if is a relation between and then it is the set of all pairs where and are related by .
188notation term.with_term_term
189 term (1000) ::= @name "(" term ", " term ")"
190end
192definition
193 Rel(A, B) := 𝒫(A × B)
194end
196theorem rel_on.def [A B : term] :
197 |- ∀R, R ∈ Rel(A, B) ↔ R ⊆ A × B
198proof
199 follows Rel(A, B) = 𝒫(A × B) by eq.refl [Rel(A, B)];
200 done by powset.def
201qed
For a relation we have the notions of the domain and range which are the sets of the first element of each pair and the second element of each pair, respectively.
207definition
208 dom(R) := {π₁(x) | x ∈ R}
209end
211definition
212 ran(R) := {π₂(x) | x ∈ R}
213end
We can prove the following using the set map definition.
217theorem dom.def [R : term] :
218 |- ∀x, x ∈ dom(R) ↔ ∃y ∈ R, x = π₁(y)
219proof
220 suffices ∀x, x ∈ {π₁(z) | z ∈ R} ↔ ∃y ∈ R, x = π₁(y);
221 thus ∀x, x ∈ {π₁(z) | z ∈ R} ↔ (∃z, z ∈ R ∧ x = π₁(z)) by set_map.def [π₁(_)] [R];
222 done logically
223qed
225theorem ran.def [R : term] :
226 |- ∀x, x ∈ ran(R) ↔ ∃y ∈ R, x = π₂(y)
227proof
228 suffices ∀x, x ∈ {π₂(z) | z ∈ R} ↔ ∃y ∈ R, x = π₂(y);
229 thus ∀x, x ∈ {π₂(z) | z ∈ R} ↔ (∃z, z ∈ R ∧ x = π₂(z)) by set_map.def [π₂(_)] [R];
230 done logically
231qed
We can also have the notion of being a relation without having to know the exact domain and range.
236notation postfix_pred
237 sentence ::= term " : " @name
238end
240definition
241 R : Rel := R ∈ Rel(dom(R), ran(R))
242end
244theorem rel.def [R : term] :
245 |- R : Rel ↔ R ∈ Rel(dom(R), ran(R))
246proof
247 done by iff.refl [R : Rel]
248qed
The following result can be proved using the different relation definitions as well as the definition of the domain and range.
252theorem rel.is_rel_on [R : term] :
253 |- R : Rel ↔ ∃A, ∃B, R ∈ Rel(A, B)
254proof
255 -- (→)
256 assume R : Rel then ∃A, ∃B, R ∈ Rel(A, B) as
257 follows R ∈ Rel(dom(R), ran(R)) by rel.def;
258 done logically;
259 -- (←)
260 assume ∃A, ∃B, R ∈ Rel(A, B) then R : Rel as
261 -- We can fix A and B with our assumption
262 obtain A st ∃B, R ∈ Rel(A, B) logically;
263 obtain B st R ∈ Rel(A, B) logically;
264 follows R ⊆ A × B by rel_on.def;
265 suffices R ∈ Rel(dom(R), ran(R)) by rel.def;
266 suffices R ⊆ dom(R) × ran(R) by rel_on.def;
267 suffices ∀x, x ∈ R → x ∈ dom(R) × ran(R) by sub.def;
268 arbitrary x;
269 assume x ∈ R then x ∈ dom(R) × ran(R) as
270 follows ∀y, y ∈ R → y ∈ A × B by sub.def given R ⊆ A × B;
271 follows x ∈ A × B logically;
272 -- As x is an ordered pair in A × B, we know specifically that there is an a and b which make up the ordered pair x
273 obtain a st a ∈ A and b st b ∈ B ∧ x = ⟨a, b⟩ by cart_prod.def;
274 -- TODO: This (2 next lines) should not be something we have to prove
275 follows π₁(x) = a by opair_first.def given x = ⟨a, b⟩;
276 follows π₂(x) = b by opair_second.def given x = ⟨a, b⟩;
277 -- The first and second coordinates of x are by definition in the domain and range of R
278 thus π₁(x) ∈ dom(R) by dom.def given x ∈ R;
279 thus π₂(x) ∈ ran(R) by ran.def given x ∈ R;
280 done by cart_prod.def;
281 ;
282 done logically
283qed
We can show this fact in a similar manner to the previous proof, additionally making use of our cartesian product subset lemma.
286theorem rel_on.is_rel [R A B : term] :
287 |- R ∈ Rel(A, B) ↔ (R : Rel ∧ dom(R) ⊆ A ∧ ran(R) ⊆ B)
288proof
289 -- If R is a relation, then its a relation between sets
290 follows R : Rel ↔ ∃C, ∃D, R ∈ Rel(C, D) by rel.is_rel_on;
291 suffices R ∈ Rel(A, B) ↔ ((∃C, ∃D, R ∈ Rel(C, D)) ∧ dom(R) ⊆ A ∧ ran(R) ⊆ B) logically;
292 -- (→)
293 assume R ∈ Rel(A, B) then ((∃C, ∃D, R ∈ Rel(C, D)) ∧ dom(R) ⊆ A ∧ ran(R) ⊆ B) as
294 -- Really we just have to show that dom(R) ⊆ A and ran(R) ⊆ B as the first proposition is the same as our assumption
295 hence R ⊆ A × B by rel_on.def;
296 hence ∃C, ∃D, R ⊆ C × D logically;
297 follows ∃C, ∃D, R ∈ Rel(C, D) by rel_on.def;
298 suffices dom(R) ⊆ A ∧ ran(R) ⊆ B logically;
299 suffices (∀x ∈ dom(R), x ∈ A) ∧ (∀y ∈ ran(R), y ∈ B) by sub.def;
300 suffices (∀x, x ∈ dom(R) → x ∈ A) ∧ (∀y, y ∈ ran(R) → y ∈ B) logically;
301 -- Similarly to the last proof, we want to show the statement holds for an arbitrary element
302 hence (∀x, x ∈ dom(R) → x ∈ A) as
303 arbitrary x;
304 assume x ∈ dom(R) then x ∈ A as
305 obtain z st z ∈ R ∧ x = π₁(z) by dom.def;
306 follows z ∈ A × B by sub.def given R ⊆ A × B;
307 obtain a st a ∈ A and b st b ∈ B ∧ z = ⟨a, b⟩ by cart_prod.def;
308 follows π₁(z) = a by opair_first.def given z = ⟨a, b⟩;
309 done logically
310 ;
311 done logically
312 ;
313 hence (∀y, y ∈ ran(R) → y ∈ B) as
314 arbitrary y;
315 assume y ∈ ran(R) then y ∈ B as
316 obtain z st z ∈ R ∧ y = π₂(z) by ran.def;
317 follows z ∈ A × B by sub.def given R ⊆ A × B;
318 obtain b st b ∈ B and a st a ∈ A ∧ z = ⟨a, b⟩ by cart_prod.def;
319 follows π₂(z) = b by opair_second.def given z = ⟨a, b⟩;
320 done logically
321 ;
322 done logically
323 ;
324 done logically
325 ;
326 -- (←)
327 assume ((∃C, ∃D, R ∈ Rel(C, D)) ∧ dom(R) ⊆ A ∧ ran(R) ⊆ B) then R ∈ Rel(A, B) as
328 hence R : Rel by rel.is_rel_on;
329 follows R ∈ Rel(dom(R), ran(R)) by rel.def;
330 thus R ⊆ dom(R) × ran(R) by rel_on.def;
331 -- TODO: is this lemma useful?
332 follows dom(R) × ran(R) ⊆ A × B by cart_prod.sub;
333 hence R ⊆ A × B by sub.def given R ⊆ dom(R) × ran(R);
334 done by rel_on.def
335 ;
336 done logically
337qed
A functional relation is a particular kind of binary relation where the first element of each ordered pair in the relation is unique.
342notation functional_relation
343 term ::= term " → " term
344end
346definition
347 A → B := {f ∈ Rel(A, B) | ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f}
348end
350theorem fn_on.def [A B : term] :
351 |- ∀f, f ∈ (A → B) ↔ f ∈ Rel(A, B) ∧ ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f
352proof
353 suffices ∀f, f ∈ {f ∈ Rel(A, B) | ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f} ↔ f ∈ Rel(A, B) ∧ ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f;
354 done by zfc.extensionality
355qed
And once again we can define the notion of being a function independent of the domain and range.
360definition
361 f : Fn := f ∈ (dom(f) → ran(f))
362end
364theorem fn.def [f : term] :
365 |- f : Fn ↔ f ∈ (dom(f) → ran(f))
366proof
367 done by iff.refl [f : Fn]
368qed
370lemma fn.in_rel [A B : term] :
371 |- (A → B) ⊆ Rel(A, B)
372proof
373 thus {f ∈ Rel(A, B) | ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f} ⊆ Rel(A, B)
374 by comp.sub [∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ _] [Rel(A, B)];
375qed
377theorem fn.is_fn_on [f : term] :
378 |- f : Fn ↔ ∃A, ∃B, f ∈ (A → B)
379proof
380 suffices f ∈ (dom(f) → ran(f)) ↔ ∃A, ∃B, f ∈ (A → B);
381 assume f ∈ (dom(f) → ran(f)) then ∃A, ∃B, f ∈ (A → B) logically;
382 assume ∃A, ∃B, f ∈ (A → B) then f ∈ (dom(f) → ran(f)) as
383 obtain A st ∃B, f ∈ (A → B) logically;
384 obtain B st f ∈ (A → B) logically;
385 hence f ∈ Rel(A, B) ∧ ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f by fn_on.def;
386 follows f : Rel by rel.is_rel_on;
387 follows f ∈ Rel(dom(f), ran(f)) by rel.def;
388 follows dom(f) ⊆ A by rel_on.is_rel;
389 follows ∀a, a ∈ dom(f) → a ∈ A by sub.def given dom(f) ⊆ A;
390 hence ∀a ∈ dom(f), ∃!b, ⟨a, b⟩ ∈ f logically;
391 done by fn_on.def
392 ;
393 done logically
394qed
396theorem fn_on.is_fn [f A B : term] :
397 |- f ∈ (A → B) ↔ (f : Fn ∧ dom(f) = A ∧ ran(f) ⊆ B)
398proof
399 hence f: Fn ↔ ∃C, ∃D, f ∈ (C → D) by fn.is_fn_on;
400 suffices f ∈ (A → B) ↔ (∃C, ∃D, f ∈ (C → D) ∧ dom(f) = A ∧ ran(f) ⊆ B) logically;
401 assume f ∈ (A → B) then (∃C, ∃D, f ∈ (C → D) ∧ dom(f) = A ∧ ran(f) ⊆ B) as
402 hence ∃C, ∃D, f ∈ (C → D) logically;
403 thus ∀x, x ∈ (A → B) → ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ x by fn_on.def;
404 follows ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f logically;
405 suffices dom(f) = A ∧ ran(f) ⊆ B logically;
406 follows (A → B) ⊆ Rel(A, B) by fn.in_rel;
407 follows f ∈ Rel(A, B) by sub.def given (A → B) ⊆ Rel(A, B);
408 follows dom(f) ⊆ A ∧ ran(f) ⊆ B by rel_on.is_rel;
409 suffices A ⊆ dom(f) by sub.sub_eq;
410 suffices ∀a ∈ A, a ∈ dom(f) by sub.def;
411 arbitrary a;
412 assume a ∈ A then a ∈ dom(f) as
413 obtain b st ⟨a, b⟩ ∈ f logically;
414 thus a = π₁(⟨a, b⟩) by opair_first.def;
415 done by dom.def given ⟨a, b⟩ ∈ f
416 ;
417 done logically
418 ;
419 assume (∃C, ∃D, f ∈ (C → D) ∧ dom(f) = A ∧ ran(f) ⊆ B) then f ∈ (A → B) as
420 obtain C st ∃D, f ∈ (C → D) ∧ dom(f) = A ∧ ran(f) ⊆ B logically;
421 obtain D st f ∈ (C → D) ∧ dom(f) = A ∧ ran(f) ⊆ B logically;
422 follows f : Fn by fn.is_fn_on;
423 follows f ∈ (dom(f) → ran(f)) by fn.def;
424 follows ∀a ∈ dom(f), ∃!b, ⟨a, b⟩ ∈ f by fn_on.def;
425 hence ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f logically;
426 follows (C → D) ⊆ Rel(C, D) by fn.in_rel;
427 follows f ∈ Rel(C, D) by sub.def given (C → D) ⊆ Rel(C, D);
428 follows f : Rel by rel.is_rel_on;
429 hence dom(f) = A logically;
430 follows dom(f) ⊆ dom(f) by sub.refl;
431 follows dom(f) ⊆ A by eq.subst [dom(f) ⊆ _] [dom(f)] [A];
432 follows f ∈ Rel(A, B) by rel_on.is_rel;
433 done by fn_on.def
434 ;
435 done logically
436qed
We define function application by extracting the second element of the unique ordered pair which has the argument as the first element. We can make this definition using the iota operator.
442notation function_application
443 term (1000) ::= term "(" term ")"
444end
446definition
447 f:term (a) := ℩b, ⟨a, b⟩ ∈ f
448end
This proof follows from our definition as well as the iota operator which lets us show unambiguity
452theorem fn_on.pairs [f A B : term] : (f ∈ (A → B))
453 |- f = {⟨a, f(a)⟩ | a ∈ A}
454proof
455 suffices f = {y | ∃a, a ∈ A ∧ y = ⟨a, f(a)⟩};
456 thus f ∈ Rel(A, B) ∧ ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f by fn_on.def;
457 follows f ⊆ A × B by rel_on.def;
458 follows ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f logically;
459 thus ∀x, x ∈ f ↔ (∃a, a ∈ A ∧ x = ⟨a, f(a)⟩) as
460 arbitrary x;
461 assume x ∈ f then ∃a, a ∈ A ∧ x = ⟨a, f(a)⟩ as
462 follows x ∈ A × B by sub.def given f ⊆ A × B;
463 obtain a st a ∈ A and b st b ∈ B ∧ x = ⟨a, b⟩ by cart_prod.def;
464 follows ⟨a, b⟩ ∈ f given x = ⟨a, b⟩;
465 follows ∃!b, ⟨a, b⟩ ∈ f logically;
466 follows ⟨a, f(a)⟩ ∈ f by iota.unique [⟨a, _⟩ ∈ f];
467 hence f(a) = b logically;
468 hence x = ⟨a, f(a)⟩ logically;
469 done logically
470 ;
471 assume ∃a, a ∈ A ∧ x = ⟨a, f(a)⟩ then x ∈ f as
472 obtain a st a ∈ A ∧ x = ⟨a, f(a)⟩ logically;
473 follows ∃!b, ⟨a, b⟩ ∈ f logically;
474 follows ⟨a, f(a)⟩ ∈ f by iota.unique [⟨a, _⟩ ∈ f];
475 done logically
476 ;
477 done logically
478 ;
479 -- f itself witnesses that the set exists, so the comprehension is well
480 -- defined and has the expected members.
481 follows ∃z, ∀x, x ∈ z ↔ (∃a, a ∈ A ∧ x = ⟨a, f(a)⟩) logically;
482 follows ∀x, x ∈ {y | ∃a, a ∈ A ∧ y = ⟨a, f(a)⟩} ↔ (∃a, a ∈ A ∧ x = ⟨a, f(a)⟩) by uncomp.def [∃a, a ∈ A ∧ _ = ⟨a, f(a)⟩];
483 follows ∀x, x ∈ f ↔ x ∈ {y | ∃a, a ∈ A ∧ y = ⟨a, f(a)⟩} logically;
484 done by zfc.extensionality
485qed
487theorem fn.pairs [f : term] : (f : Fn)
488 |- f = {⟨x, f(x)⟩ | x ∈ dom(f)}
489proof
490 follows f ∈ (dom(f) → ran(f)) by fn.def;
491 done by fn_on.pairs [f] [dom(f)] [ran(f)]
492qed
A useful lemma which lets us skip a lot of notation
496lemma fn.apply_iff [f a b : term] : (f : Fn) (a ∈ dom(f))
497 |- ⟨a, b⟩ ∈ f ↔ f(a) = b
498proof
499 follows f ∈ (dom(f) → ran(f)) by fn.def;
500 follows ∀a ∈ dom(f), ∃!b, ⟨a, b⟩ ∈ f by fn_on.def;
501 follows ∃!b, ⟨a, b⟩ ∈ f logically;
502 follows ⟨a, f(a)⟩ ∈ f by iota.unique [⟨a, _⟩ ∈ f];
503 done logically
504qed
507notation function_maps_to
508 term ::= x:@binding(term) " ∈ " term " ↦ " term(x)
509end
511definition
512 x ∈ X ↦ f(x) := {⟨x, f(x)⟩ | x ∈ X}
513end
This theorem follows from an ever-rare explicit use of the axiom of replacement as well as previously shown results for relations.
517theorem fun_map.is.rel [A B : term] [f(_) : term(term)]: (∀x ∈ A, f(x) ∈ B)
518 |- x ∈ A ↦ f(x) ∈ (A → B)
519proof
520 suffices {⟨x, f(x)⟩ | x ∈ A} ∈ (A → B);
521 suffices {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} ∈ (A → B);
522 -- Using our replacement axiom to show that a functional mapping of a set defines its own set
523 follows ∀a, (∀x, x ∈ a → ∃!y, y = ⟨x, f(x)⟩) → (∃x, ∀y, y ∈ x ↔ (∃z, z ∈ a ∧ y = ⟨z, f(z)⟩))
524 by zfc.replacement [_1 = ⟨_0, f(_0)⟩];
525 -- Then we show the set that it defines
526 follows ∃z, ∀y, y ∈ z ↔ (∃x, x ∈ A ∧ y = ⟨x, f(x)⟩) logically;
527 thus ∀y, y ∈ {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} ↔ (∃x, x ∈ A ∧ y = ⟨x, f(x)⟩)
528 by uncomp.def [∃x, x ∈ A ∧ _ = ⟨x, f(x)⟩];
529 suffices {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} ∈ Rel(A, B)
530 ∧ ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} by fn_on.def;
531 -- Function mappings are subsets of all of the relations between two sets
532 thus {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} ∈ Rel(A, B) as
533 suffices {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} ⊆ A × B by rel_on.def;
534 suffices ∀w, w ∈ {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} → w ∈ A × B by sub.def;
535 arbitrary w;
536 assume w ∈ {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} then w ∈ A × B as
537 obtain a st a ∈ A ∧ w = ⟨a, f(a)⟩ logically;
538 follows f(a) ∈ B logically;
539 done by cart_prod.def
540 ;
541 done logically
542 ;
543 -- Showing function well-definedness, basically that every element a in A has a mapping, and that a = a → f(a) = f(a)
544 thus ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} as
545 arbitrary a;
546 assume a ∈ A then ∃!b, ⟨a, b⟩ ∈ {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} as
547 thus ⟨a, f(a)⟩ ∈ {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} logically;
548 thus ∀b, ⟨a, b⟩ ∈ {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} → b = f(a) as
549 arbitrary b;
550 assume ⟨a, b⟩ ∈ {y | ∃x, x ∈ A ∧ y = ⟨x, f(x)⟩} then b = f(a) as
551 obtain c st c ∈ A ∧ ⟨a, b⟩ = ⟨c, f(c)⟩ logically;
552 follows a = c ∧ b = f(c) by opair.eq;
553 done logically
554 ;
555 done logically
556 ;
557 done logically
558 ;
559 done logically
560 ;
561
562 done logically
563qed
566lemma fun_map.apply [A B a : term] [e(_) : term(term)] : (∀x ∈ A, e(x) ∈ B) (a ∈ A)
567 |- (x ∈ A ↦ e(x))(a) = e(a)
568proof
569 follows x ∈ A ↦ e(x) ∈ (A → B) by fun_map.is.rel [A] [B] [e(_)];
570 follows x ∈ A ↦ e(x) : Fn by fn_on.is_fn;
571 follows dom(x ∈ A ↦ e(x)) = A by fn_on.is_fn;
572 follows a ∈ dom(x ∈ A ↦ e(x)) logically;
573 follows ∀y, y ∈ {⟨x, e(x)⟩ | x ∈ A} ↔ (∃x, x ∈ A ∧ y = ⟨x, e(x)⟩)
574 by set_map.def [⟨_, e(_)⟩] [A];
575 follows ⟨a, e(a)⟩ ∈ {⟨x, e(x)⟩ | x ∈ A} ↔ (∃x, x ∈ A ∧ ⟨a, e(a)⟩ = ⟨x, e(x)⟩)
576 specializing ∀y, y ∈ {⟨x, e(x)⟩ | x ∈ A} ↔ (∃x, x ∈ A ∧ y = ⟨x, e(x)⟩);
577 follows ⟨a, e(a)⟩ ∈ {⟨x, e(x)⟩ | x ∈ A} logically;
578 follows ⟨a, e(a)⟩ ∈ (x ∈ A ↦ e(x)) logically;
579 follows ⟨a, e(a)⟩ ∈ (x ∈ A ↦ e(x)) ↔ (x ∈ A ↦ e(x))(a) = e(a)
580 by fn.apply_iff [x ∈ A ↦ e(x)] [a] [e(a)];
581 done logically
582qed
TODO:
586grammar_category chain_list
588tactic tactic.chain
589 tactic ::= @kw"chain" term:@fragment(term) list:chain_list
590end
592tactic chain_list.one
593 chain_list ::= "=" term:@fragment(term) just:justification ";"
594end
595tactic chain_list.many
596 chain_list ::= "=" term:@fragment(term) just:justification ";" rest:chain_list
597end
600theorem fn.eq_on_dom.eq [f g : term] : (f : Fn) (g : Fn) (dom(f) = dom(g))
601 (∀x ∈ dom(f), f(x) = g(x))
602 |- f = g
603proof
604 -- chain f = {⟨x, f(x)⟩ | x ∈ dom(f)} by fn.pairs;
605 -- = {⟨x, g(x)⟩ | x ∈ dom(f)} given ∀x ∈ dom(f), f(x) = g(x);
606 -- = {⟨x, g(x)⟩ | x ∈ dom(g)} given dom(f) = dom(g);
607 -- = g by fn.pairs;
608 chain f = {⟨x, f(x)⟩ | x ∈ dom(f)} as todo;
609 = {⟨x, g(x)⟩ | x ∈ dom(f)} as todo;
610 = {⟨x, g(x)⟩ | x ∈ dom(g)} as todo;
611 = g as todo;
612qed
614notation fn_restriction
615 term ::= term " ↾ " term
616end
618definition
619 f ↾ A := {x ∈ f | π₁(x) ∈ A}
620end
622theorem fn.restriction.is [f X : term] : (f : Fn)
623 |- f ↾ X : Fn
624proof
625 todo
626qed
628theorem fn.restriction.pairs [f X : term] : (f : Fn)
629 |- f ↾ X = {⟨x, f(x)⟩ | x ∈ dom(f) ∩ X}
630proof
631 todo
632qed
634theorem fn.restriction.eq [f g X : term] : (f : Fn) (g : Fn) (dom(f) ∩ X = dom(g) ∩ X)
635 (∀x ∈ dom(f) ∩ X, f(x) = g(x))
636 |- f ↾ X = g ↾ X
637proof
638 -- chain f ↾ X
639 -- = {⟨x, f(x)⟩ | x ∈ dom(f) ∩ X} by fn.restriction.pairs;
640 -- = {⟨x, g(x)⟩ | x ∈ dom(f) ∩ X} given ∀x ∈ X, f(x) = g(x);
641 -- = {⟨x, g(x)⟩ | x ∈ dom(g) ∩ X} given dom(f) ∩ X = dom(g) ∩ X;
642 -- = g ↾ X by fn.restriction.pairs;
643 chain f ↾ X
644 = {⟨x, f(x)⟩ | x ∈ dom(f) ∩ X} as todo;
645 = {⟨x, g(x)⟩ | x ∈ dom(f) ∩ X} as todo;
646 = {⟨x, g(x)⟩ | x ∈ dom(g) ∩ X} as todo;
647 = g ↾ X as todo;
648qed
Function properties & Composition 3.4
The image of a function under a set is the set resulting from applying the function to every element of the set
654notation image_set
655 term (1000) ::= term "[" term "]"
656end
658definition
659 f:term [A] := {f(a) | a ∈ A}
660end
662theorem image.def [f A : term] :
663 |- ∀y, y ∈ f[A] ↔ ∃a ∈ A, y = f(a)
664proof
665 suffices ∀y, y ∈ {f(a) | a ∈ A} ↔ ∃a ∈ A, y = f(a);
666 thus ∀y, y ∈ {f(a) | a ∈ A} ↔ (∃a, a ∈ A ∧ y = f(a)) by set_map.def [f(_)] [A];
667 done logically
668qed
Trivially, the image of a subset of a domain is a subset of the range, with equality when finding the image of the domain
672theorem dom.is_ran_under_image [f A B : term] : (f ∈ (A → B))
673 |- f[A] = ran(f)
674proof
675 thus f : Fn by fn_on.is_fn;
676 suffices f[dom(f)] = ran(f) by fn_on.is_fn;
677 hence ∀y, y ∈ f[dom(f)] ↔ ∃a ∈ dom(f), y = f(a) by image.def;
678 furthermore ∀y, y ∈ ran(f) ↔ ∃z ∈ f, y = π₂(z) by ran.def;
679 indeed ∀y, y ∈ f[dom(f)] ↔ y ∈ ran(f) as
680 arbitrary y;
681 assume y ∈ f[dom(f)] then y ∈ ran(f) as
682 obtain a st a ∈ dom(f) ∧ y = f(a) logically;
683 hence ⟨a, f(a)⟩ ∈ f ↔ f(a) = f(a) by fn.apply_iff given a ∈ dom(f);
684 follows π₂(⟨a, f(a)⟩) = f(a) by opair_second.def;
685 done by ran.def given ⟨a, f(a)⟩ ∈ f
686 ;
687 assume y ∈ ran(f) then y ∈ f[dom(f)] as
688 follows f ⊆ A × B by rel_on.def, fn.in_rel, sub.def;
689 obtain b st b ∈ f ∧ y = π₂(b) logically;
690 hence b ∈ A × B by sub.def;
691 obtain a st a ∈ A and c st c ∈ B ∧ b = ⟨a, c⟩ by cart_prod.def;
692 furthermore π₂(b) = c by opair_second.def given b = ⟨a, c⟩;
693 thus a = π₁(⟨a, c⟩) by opair_first.def;
694 thus ⟨a, c⟩ ∈ f given b = ⟨a, c⟩;
695 hence a ∈ dom(f) by dom.def given ⟨a, c⟩ ∈ f;
696 follows ⟨a, c⟩ ∈ f ↔ f(a) = c by fn.apply_iff [f] [a] [c];
697 follows f(a) = y logically;
698 done by image.def given a ∈ dom(f)
699 ;
700 done logically
701 ;
702 done by zfc.extensionality
703qed
706lemma image.mono [f X Y : term] : (X ⊆ Y)
707 |- f[X] ⊆ f[Y]
708proof
709 suffices ∀y, y ∈ f[X] → y ∈ f[Y] by sub.def;
710 arbitrary y;
711 assume y ∈ f[X] then y ∈ f[Y] as
712 obtain a st a ∈ X ∧ y = f(a) by image.def;
713 follows a ∈ Y by sub.def;
714 done by image.def
715 ;
716 done logically
717qed
719lemma fn_on.apply_in [f A B a : term] : (f ∈ (A → B)) (a ∈ A)
720 |- f(a) ∈ B
721proof
722 follows f[A] = ran(f) by dom.is_ran_under_image;
723 follows ran(f) ⊆ B by fn_on.is_fn;
724 follows f(a) ∈ f[A] by image.def;
725 done by sub.def
726qed
Importantly, every image has a preimage, which we'll have as the set of terms which are mapped to a specific set under a function
730notation preimage_set
731 term (1000) ::= term "⁻¹" "[" term "]"
732end
734definition
735 f:term⁻¹[A] := {x ∈ dom(f) | f(x) ∈ A}
736end
738theorem preimage.def [f A : term] :
739 |- ∀x, x ∈ f⁻¹[A] ↔ (x ∈ dom(f) ∧ f(x) ∈ A)
740proof
741 suffices ∀x, x ∈ {x ∈ dom(f) | f(x) ∈ A} ↔ (x ∈ dom(f) ∧ f(x) ∈ A);
742 done by zfc.extensionality
743qed
A surjection, also known as an onto function, between sets is a mapping where the range is the same as the codomain
747notation surjection
748 term ::= term " ↠ " term
749end
751definition
752 A ↠ B := {f ∈ (A → B) | ran(f) = B}
753end
755theorem surj_on.def [A B : term] :
756 |- ∀f, f ∈ (A ↠ B) ↔ (f ∈ (A → B) ∧ ran(f) = B)
757proof
758 suffices ∀f, f ∈ {f ∈ (A → B) | ran(f) = B} ↔ (f ∈ (A → B) ∧ ran(f) = B);
759 done by zfc.extensionality
760qed
An injection, a one-to-one function, between sets is one where every element of the domain is mapped to a unique element in the range
764notation injection
765 term ::= term " ↣ " term
766end
768definition
769 A ↣ B := {f ∈ (A → B) | ∀x, ∀y, x ∈ A ∧ y ∈ A ∧ f(x) = f(y) → x = y}
770end
772theorem inj_on.def [A B : term] :
773 |- ∀f, f ∈ (A ↣ B) ↔ (f ∈ (A → B) ∧ (∀x, ∀y, x ∈ A ∧ y ∈ A ∧ f(x) = f(y) → x = y))
774proof
775 suffices ∀f, f ∈ {f ∈ (A → B) | ∀x, ∀y, x ∈ A ∧ y ∈ A ∧ f(x) = f(y) → x = y} ↔ (f ∈ (A → B) ∧ (∀x, ∀y, x ∈ A ∧ y ∈ A ∧ f(x) = f(y) → x = y));
776 done by zfc.extensionality
777qed
779definition
780 f : Inj := f ∈ (dom(f) ↣ ran(f))
781end
783theorem inj.def [f : term] :
784 |- f : Inj ↔ f ∈ (dom(f) ↣ ran(f))
785proof
786 done by iff.refl [f : Inj]
787qed
A bijection between sets is a function that is both injective and surjective
791notation bijection
792 term ::= term " ↔ " term
793end
795definition
796 A ↔ B := {f ∈ (A ↣ B) | ran(f) = B}
797end
799theorem bij_on.def [A B : term] :
800 |- ∀f, f ∈ (A ↔ B) ↔ (f ∈ (A ↣ B) ∧ ran(f) = B)
801proof
802 suffices ∀f, f ∈ {f ∈ (A ↣ B) | ran(f) = B} ↔ (f ∈ (A ↣ B) ∧ ran(f) = B);
803 done by zfc.extensionality
804qed
806definition
807 f : Bij := f ∈ (dom(f) ↔ ran(f))
808end
810theorem bij.def [f : term] :
811 |- f : Bij ↔ f ∈ (dom(f) ↔ ran(f))
812proof
813 done by iff.refl [f : Bij]
814qed
This theorem follows cleanly from the definitions for injective, bijective, and surjective functions
818theorem bij_on.is_inj_and_surj [f A B : term] :
819 |- f ∈ (A ↔ B) ↔ (f ∈ (A ↣ B) ∧ f ∈ (A ↠ B))
820proof
821 follows f ∈ (A ↔ B) ↔ (f ∈ (A ↣ B) ∧ ran(f) = B) by bij_on.def;
822 follows f ∈ (A ↠ B) ↔ (f ∈ (A → B) ∧ ran(f) = B) by surj_on.def;
823 follows f ∈ (A ↣ B) → f ∈ (A → B) by inj_on.def;
824 done logically
825qed
We can define an inverse relation simply as the swapped coordinates of the relation
829notation inverse_relation
830 term (1000) ::= term "⁻¹"
831end
833definition
834 f:term⁻¹ := {⟨π₂(p), π₁(p)⟩ | p ∈ f}
835end
Swapping the components of every pair in f swaps the roles of the domain and the range.
839lemma inv.dom [f : term] :
840 |- dom(f⁻¹) = ran(f)
841proof
842 follows ∀x, x ∈ dom(f⁻¹) ↔ ∃y ∈ f⁻¹, x = π₁(y) by dom.def;
843 thus ∀y, y ∈ f⁻¹ ↔ ∃p ∈ f, y = ⟨π₂(p), π₁(p)⟩ by set_map.def [⟨π₂(_), π₁(_)⟩] [f];
844 follows ∀p, π₁(⟨π₂(p), π₁(p)⟩) = π₂(p) by opair_first.def;
845 follows ∀x, x ∈ ran(f) ↔ ∃p ∈ f, x = π₂(p) by ran.def;
846 hence ∀x, x ∈ dom(f⁻¹) ↔ x ∈ ran(f) logically;
847 done by zfc.extensionality
848qed
850lemma inv.ran [f : term] :
851 |- ran(f⁻¹) = dom(f)
852proof
853 follows ∀x, x ∈ ran(f⁻¹) ↔ ∃y ∈ f⁻¹, x = π₂(y) by ran.def;
854 thus ∀y, y ∈ f⁻¹ ↔ ∃p ∈ f, y = ⟨π₂(p), π₁(p)⟩ by set_map.def [⟨π₂(_), π₁(_)⟩] [f];
855 follows ∀p, π₂(⟨π₂(p), π₁(p)⟩) = π₁(p) by opair_second.def;
856 follows ∀x, x ∈ dom(f) ↔ ∃p ∈ f, x = π₁(p) by dom.def;
857 hence ∀x, x ∈ ran(f⁻¹) ↔ x ∈ dom(f) logically;
858 done by zfc.extensionality
859qed
The following proof gives us a way to reason with and construct what f⁻¹ looks like
863lemma inv.mem [f A B : term] : (f ∈ Rel(A, B))
864 |- ∀a, ∀b, ⟨a, b⟩ ∈ f⁻¹ ↔ ⟨b, a⟩ ∈ f
865proof
866 arbitrary a; arbitrary b;
867 follows f ⊆ A × B by rel_on.def;
868 thus ∀y, y ∈ f⁻¹ ↔ ∃p ∈ f, y = ⟨π₂(p), π₁(p)⟩ by set_map.def [⟨π₂(_), π₁(_)⟩] [f];
869 assume ⟨b, a⟩ ∈ f then ⟨a, b⟩ ∈ f⁻¹ as
870 follows π₁(⟨b, a⟩) = b by opair_first.def;
871 follows π₂(⟨b, a⟩) = a by opair_second.def;
872 hence ⟨a, b⟩ = ⟨π₂(⟨b, a⟩), π₁(⟨b, a⟩)⟩ logically;
873 done logically
874 ;
875 assume ⟨a, b⟩ ∈ f⁻¹ then ⟨b, a⟩ ∈ f as
876 obtain p st p ∈ f ∧ ⟨a, b⟩ = ⟨π₂(p), π₁(p)⟩ logically;
877 follows p ∈ A × B by sub.def given f ⊆ A × B;
878 obtain c st c ∈ A and d st d ∈ B ∧ p = ⟨c, d⟩ by cart_prod.def;
879 follows π₁(p) = c by opair_first.def given p = ⟨c, d⟩;
880 follows π₂(p) = d by opair_second.def given p = ⟨c, d⟩;
881 follows a = d ∧ b = c by opair.eq given ⟨a, b⟩ = ⟨π₂(p), π₁(p)⟩;
882 done logically
883 ;
884 done logically
885qed
The inverse of a relation between A and B is itself a relation, between B and A.
889lemma inv.rel [f A B : term] : (f ∈ Rel(A, B))
890 |- f⁻¹ ∈ Rel(B, A)
891proof
892 -- A relation is just some subset of the cartesian product
893 follows f ⊆ A × B by rel_on.def;
894 follows ∀a, ∀b, ⟨a, b⟩ ∈ f⁻¹ ↔ ⟨b, a⟩ ∈ f by inv.mem;
895 suffices ∀y, y ∈ f⁻¹ → y ∈ B × A by rel_on.def, sub.def;
896 arbitrary y;
897 assume y ∈ f⁻¹ then y ∈ B × A as
898 -- every element of f⁻¹ is a swapped pair from f
899 thus ∀z, z ∈ f⁻¹ ↔ ∃p ∈ f, z = ⟨π₂(p), π₁(p)⟩ by set_map.def [⟨π₂(_), π₁(_)⟩] [f];
900 obtain p st p ∈ f ∧ y = ⟨π₂(p), π₁(p)⟩ logically;
901 -- inv.mem swaps the pair back into f
902 follows ⟨π₁(p), π₂(p)⟩ ∈ f by inv.mem;
903 follows ⟨π₁(p), π₂(p)⟩ ∈ A × B by sub.def given f ⊆ A × B;
904 hence π₁(p) ∈ A ∧ π₂(p) ∈ B by cart_prod.def, opair.eq;
905 done by cart_prod.def
906 ;
907qed
When f is a bijection, its inverse is a function, every b ∈ B has a preimage because f is onto, and that preimage is unique because f is injective.
912lemma inv.is_fn_on [f A B : term] : (f ∈ (A ↔ B))
913 |- f⁻¹ ∈ (B → A)
914proof
915 indeed f ∈ (A ↣ B) ∧ ran(f) = B by bij_on.def;
916 hence f ∈ (A → B) ∧ f : Fn ∧ dom(f) = A by inj_on.def, fn_on.is_fn;
917 furthermore ∀a, ∀b, a ∈ A ∧ b ∈ A ∧ f(a) = f(b) → a = b by inj_on.def;
918 furthermore f ∈ Rel(A, B) by fn.in_rel, sub.def;
919 follows f⁻¹ ∈ Rel(B, A) by inv.rel given f ∈ Rel(A, B);
920 thus ∀a, ∀b, ⟨a, b⟩ ∈ f⁻¹ ↔ ⟨b, a⟩ ∈ f by inv.mem given f ∈ Rel(A, B);
921 suffices ∀b ∈ B, ∃!a, ⟨b, a⟩ ∈ f⁻¹ by fn_on.def;
922 arbitrary d;
923 assume d ∈ B then ∃!a, ⟨d, a⟩ ∈ f⁻¹ as
924 -- Every element of B is in the image of f[A] so a exists
925 obtain a₀ st a₀ ∈ A ∧ d = f(a₀) by image.def, dom.is_ran_under_image;
926 hence ⟨a₀, d⟩ ∈ f ∧ ⟨d, a₀⟩ ∈ f⁻¹ by fn.apply_iff given a₀ ∈ A;
927 -- any preimage of d is exactly a because f is injective
928 hence ∀a, ⟨d, a⟩ ∈ f⁻¹ → a ∈ dom(f) ∧ f(a) = d by dom.def, opair_first.def, fn.apply_iff;
929 done logically
930 ;
931 done logically
932qed
Next we show that bijections undo their inverse
936lemma inv.apply [f A B b : term] : (f ∈ (A ↔ B)) (b ∈ B)
937 |- f(f⁻¹(b)) = b
938proof
939 indeed f ∈ (A → B) ∧ f : Fn ∧ dom(f) = A by bij_on.def, inj_on.def, fn_on.is_fn;
940 furthermore f ∈ Rel(A, B) by fn.in_rel, sub.def;
941 hence ∀u, ∀v, ⟨u, v⟩ ∈ f⁻¹ ↔ ⟨v, u⟩ ∈ f by inv.mem;
942 follows f⁻¹ : Fn ∧ dom(f⁻¹) = B by inv.is_fn_on, fn_on.is_fn;
943 hence ⟨b, f⁻¹(b)⟩ ∈ f⁻¹ ∧ ⟨f⁻¹(b), b⟩ ∈ f by fn.apply_iff given b ∈ B;
944 follows f⁻¹(b) ∈ dom(f) by dom.def, opair_first.def given ⟨f⁻¹(b), b⟩ ∈ f;
945 done by fn.apply_iff given ⟨f⁻¹(b), b⟩ ∈ f and f⁻¹(b) ∈ dom(f)
946qed
948notation function_composition
949 term (400) ::= term " ∘ " term
950end
952definition
953 g ∘ f := {⟨x, g(f(x))⟩ | x ∈ {x ∈ dom(f) | f(x) ∈ dom(g)}}
954end
956theorem composition.def [f g : term] :
957 |- ∀y, y ∈ (g ∘ f) ↔ ∃x, (x ∈ dom(f) ∧ f(x) ∈ dom(g)) ∧ y = ⟨x, g(f(x))⟩
958proof
959 follows ∀y, y ∈ (g ∘ f) ↔ ∃x ∈ {x ∈ dom(f) | f(x) ∈ dom(g)}, y = ⟨x, g(f(x))⟩
960 by set_map.def [⟨_, g(f(_))⟩] [{x ∈ dom(f) | f(x) ∈ dom(g)}];
961 hence ∀x, x ∈ {x ∈ dom(f) | f(x) ∈ dom(g)} ↔ (x ∈ dom(f) ∧ f(x) ∈ dom(g))
962 by comp.def [f(_) ∈ dom(g)] [dom(f)];
963 done logically
964qed
966theorem composition.dom [f g : term] :
967 |- ∀x, x ∈ dom(g ∘ f) ↔ (x ∈ dom(f) ∧ f(x) ∈ dom(g))
968proof
969 follows ∀z, z ∈ dom(g ∘ f) ↔ ∃y ∈ (g ∘ f), z = π₁(y) by dom.def;
970 furthermore ∀y, y ∈ (g ∘ f) ↔ ∃x, (x ∈ dom(f) ∧ f(x) ∈ dom(g)) ∧ y = ⟨x, g(f(x))⟩ by composition.def;
971 indeed ∀x, π₁(⟨x, g(f(x))⟩) = x by opair_first.def;
972 done logically
973qed
Here we show that function composition is itself a function
977theorem composition.is_fn [f g : term] : (f : Fn) (g : Fn)
978 |- g ∘ f : Fn
979proof
980 -- We want to show that the composition is some functional relation between two sets
981 suffices ∃A, ∃B, g ∘ f ∈ (A → B) by fn.is_fn_on;
982 thus ∀x ∈ {x ∈ dom(f) | f(x) ∈ dom(g)}, g(f(x)) ∈ ran(g) as
983 -- The construction here is simple as we only pick x where f(x) is in dom(g), because
984 -- g(dom(g)) being in ran(g) falls out of the definition
985 arbitrary c st c ∈ {x ∈ dom(f) | f(x) ∈ dom(g)};
986 follows g(f(c)) ∈ ran(g) as
987 follows ∀x, x ∈ {x ∈ dom(f) | f(x) ∈ dom(g)} ↔ (x ∈ dom(f) ∧ f(x) ∈ dom(g))
988 by comp.def [f(_) ∈ dom(g)] [dom(f)];
989 thus f(c) ∈ dom(g) logically;
990 hence ⟨f(c), g(f(c))⟩ ∈ g ↔ g(f(c)) = g(f(c)) by fn.apply_iff [g] [f(c)] [g(f(c))];
991 hence ⟨f(c), g(f(c))⟩ ∈ g logically;
992 follows π₂(⟨f(c), g(f(c))⟩) = g(f(c)) by opair_second.def;
993 done by ran.def given ⟨f(c), g(f(c))⟩ ∈ g
994 ;
995 done logically
996 ;
997 -- g ∘ f is a functional mapping from dom(g ∘ f) to ran(g)
998 follows g ∘ f ∈ ({x ∈ dom(f) | f(x) ∈ dom(g)} → ran(g))
999 by fun_map.is.rel [{x ∈ dom(f) | f(x) ∈ dom(g)}] [ran(g)] [g(f(_))];
1000 done logically
1001qed
This theorem follows cleanly from the above facts.
1005theorem composition.apply [f g a : term] : (f : Fn) (g : Fn) (a ∈ dom(g ∘ f))
1006 |- (g ∘ f)(a) = g(f(a))
1007proof
1008 hence a ∈ dom(f) ∧ f(a) ∈ dom(g) by composition.dom;
1009 furthermore ∀y, y ∈ (g ∘ f) ↔ ∃x, (x ∈ dom(f) ∧ f(x) ∈ dom(g)) ∧ y = ⟨x, g(f(x))⟩ by composition.def;
1010 furthermore ⟨a, g(f(a))⟩ ∈ (g ∘ f) logically;
1011 indeed g ∘ f : Fn by composition.is_fn;
1012 furthermore ⟨a, g(f(a))⟩ ∈ (g ∘ f) ↔ (g ∘ f)(a) = g(f(a)) by fn.apply_iff [g ∘ f] [a] [g(f(a))];
1013 done logically
1014qed
1016theorem composition.is_fn_on [f g A B C : term] : (f ∈ (A → B)) (g ∈ (B → C))
1017 |- g ∘ f ∈ (A → C)
1018proof
1019 hence g ∘ f : Fn by composition.is_fn, fn.is_fn_on;
1020 hence ∀x, x ∈ dom(g ∘ f) ↔ (x ∈ dom(f) ∧ f(x) ∈ dom(g)) by composition.dom;
1021 follows f ∈ (A → B) → dom(f) = A ∧ ran(f) ⊆ B by fn_on.is_fn;
1022 follows g ∈ (B → C) → dom(g) = B ∧ ran(g) ⊆ C by fn_on.is_fn;
1023 indeed ∀x, x ∈ dom(g ∘ f) ↔ (x ∈ A ∧ f(x) ∈ B) logically;
1024 hence ∀x, x ∈ A → f(x) ∈ B as
1025 arbitrary c st c ∈ A;
1026 follows f(c) ∈ B as
1027 indeed c ∈ dom(f) logically;
1028 hence ⟨c, f(c)⟩ ∈ f as
1029 indeed f : Fn by fn.is_fn_on;
1030 thus ⟨c, f(c)⟩ ∈ f ↔ f(c) = f(c) by fn.apply_iff [f] [c] [f(c)];
1031 done logically
1032 ;
1033 follows f(c) ∈ ran(f) by opair_second.def, ran.def given ⟨c, f(c)⟩ ∈ f;
1034 done by sub.def given ran(f) ⊆ B
1035 ;
1036 ;
1037 hence ∀x, x ∈ dom(g ∘ f) ↔ x ∈ A logically;
1038 hence dom(g ∘ f) = A by zfc.extensionality;
1039 thus ran(g ∘ f) ⊆ C as
1040 suffices ∀y, y ∈ ran(g ∘ f) → y ∈ C by sub.def;
1041 arbitrary y;
1042 assume y ∈ ran(g ∘ f) then y ∈ C as
1043 obtain p st p ∈ (g ∘ f) ∧ y = π₂(p) by ran.def;
1044 obtain x st (x ∈ dom(f) ∧ f(x) ∈ dom(g)) ∧ p = ⟨x, g(f(x))⟩ by composition.def;
1045 indeed g : Fn by fn.is_fn_on;
1046 furthermore f(x) ∈ dom(g) logically;
1047 follows ⟨f(x), g(f(x))⟩ ∈ g ↔ g(f(x)) = g(f(x)) by fn.apply_iff [g] [f(x)] [g(f(x))];
1048 hence ⟨f(x), g(f(x))⟩ ∈ g logically;
1049 follows g(f(x)) ∈ ran(g) by ran.def, opair_second.def given ⟨f(x), g(f(x))⟩ ∈ g;
1050 done by opair_second.def, sub.def given ran(g) ⊆ C
1051 ;
1052 done logically
1053 ;
1054 done by fn_on.is_fn
1055qed
A function composed of two injective functions is itself injective. This is a standard injectivity proof where we reason that g(f(x)) = g(f(y)) implies f(x) = f(y) which impliex x = y
1060theorem comp_inj.is_inj [f g A B C : term] : (f ∈ (A ↣ B)) (g ∈ (B ↣ C))
1061 |- g ∘ f ∈ (A ↣ C)
1062proof
1063 follows g ∘ f ∈ (A → C) by composition.is_fn_on, inj_on.def;
1064 suffices ∀x, ∀y, x ∈ A ∧ y ∈ A ∧ (g ∘ f)(x) = (g ∘ f)(y) → x = y by inj_on.def;
1065 arbitrary x; arbitrary y;
1066 assume x ∈ A ∧ y ∈ A ∧ (g ∘ f)(x) = (g ∘ f)(y) then x = y as
1067 follows f ∈ (A → B) ∧ g ∈ (B → C) by inj_on.def;
1068 indeed (∀a, ∀b, a ∈ A ∧ b ∈ A ∧ f(a) = f(b) → a = b)
1069 ∧ (∀a, ∀b, a ∈ B ∧ b ∈ B ∧ g(a) = g(b) → a = b) by inj_on.def;
1070 indeed f : Fn ∧ g : Fn by fn.is_fn_on;
1071 thus dom(g ∘ f) = A ∧ dom(g) = B by fn_on.is_fn;
1072 hence x ∈ dom(g ∘ f) ∧ y ∈ dom(g ∘ f) logically;
1073 follows g(f(x)) = g(f(y)) by composition.apply;
1074 furthermore f(x) ∈ B ∧ f(y) ∈ B by composition.dom;
1075 thus f(x) = f(y) logically;
1076 done logically
1077 ;
1078 done logically
1079qed
The following proof where we show composition of surjective functions is surjective takes a different shape. We want to show that some c in ran(g) has a preimage in dom(g) and then that dom(g) = ran(f).
1084theorem comp_surj.is_surj [f g A B C : term] : (f ∈ (A ↠ B)) (g ∈ (B ↠ C))
1085 |- g ∘ f ∈ (A ↠ C)
1086proof
1087 follows g ∘ f ∈ (A → C) by composition.is_fn_on, surj_on.def;
1088 suffices ran(g ∘ f) = C by surj_on.def;
1089 follows f ∈ (A → B) ∧ ran(f) = B ∧ g ∈ (B → C) ∧ ran(g) = C by surj_on.def;
1090 hence f : Fn ∧ g : Fn by fn_on.is_fn;
1091 thus dom(f) = A ∧ dom(g) = B ∧ ran(g ∘ f) ⊆ C by fn_on.is_fn;
1092 thus f[A] = ran(f) ∧ g[B] = ran(g) ∧ (g ∘ f)[A] = ran(g ∘ f) by dom.is_ran_under_image;
1093 furthermore ∀y, y ∈ f[A] ↔ ∃z ∈ A, y = f(z) by image.def;
1094 follows ∀y, y ∈ g[B] ↔ ∃z ∈ B, y = g(z) by image.def;
1095 suffices C ⊆ ran(g ∘ f) by sub.sub_eq;
1096 suffices ∀c, c ∈ C → c ∈ ran(g ∘ f) by sub.def;
1097 arbitrary c;
1098 assume c ∈ C then c ∈ ran(g ∘ f) as
1099 obtain b st b ∈ B ∧ c = g(b) logically;
1100 obtain a st a ∈ A ∧ b = f(a) logically;
1101 thus a ∈ dom(g ∘ f) by composition.dom;
1102 follows (g ∘ f)(a) = c by composition.apply;
1103 done by image.def given a ∈ A
1104 ;
1105 done logically
1106qed
This lemma looks a bit weird, but the idea is that we want to be able to reason about where in B f has an inverse
1110lemma inj.is_bij_to_ran [f A B : term] : (f ∈ (A ↣ B))
1111 |- f ∈ (A ↔ ran(f))
1112proof
1113 suffices f ∈ (A ↣ ran(f)) by bij_on.def;
1114 suffices (f ∈ (A → ran(f))) ∧ (∀x, ∀y, x ∈ A ∧ y ∈ A ∧ f(x) = f(y) → x = y) by inj_on.def;
1115 hence f : Fn ∧ dom(f) = A by fn_on.is_fn, inj_on.def;
1116 follows ran(f) ⊆ ran(f) by sub.refl;
1117 indeed f ∈ (A → ran(f)) by fn_on.is_fn;
1118 done by inj_on.def
1119qed
1121lemma sub.has_surj [S B : term]: (S ⊆ B) (S ≠ ∅)
1122 |- ∃h, h ∈ (B ↠ S)
1123proof
1124 todo
1125qed
One of the most important properties of a bijective function is that it defines a unique bijective inverse. The proof follows cleanly from the previous inverse theorems.
1130theorem bij.has_inverse [f A B : term] : (f ∈ (A ↔ B))
1131 |- f⁻¹ ∈ (B ↔ A)
1132proof
1133 follows f⁻¹ ∈ (B → A) by inv.is_fn_on;
1134 follows dom(f) = A by bij_on.def, inj_on.def, fn_on.is_fn;
1135 follows ran(f⁻¹) = A by inv.ran given dom(f) = A;
1136 thus ∀x, ∀y, x ∈ B ∧ y ∈ B ∧ f⁻¹(x) = f⁻¹(y) → x = y as
1137 arbitrary x; arbitrary y;
1138 assume x ∈ B ∧ y ∈ B ∧ f⁻¹(x) = f⁻¹(y) then x = y as
1139 follows f(f⁻¹(x)) = x ∧ f(f⁻¹(y)) = y by inv.apply;
1140 done logically
1141 ;
1142 done logically
1143 ;
1144 follows f⁻¹ ∈ (B ↣ A) by inj_on.def;
1145 done by bij_on.def
1146qed
Here we have that an injection between sets implies the existence of a surjection the other way. We'll use this lemma later to explicitly construct this surjection. This lemma follows from the previous few where we show a surjection from B to ran(f) via sub.has_surj and ran(f) to A via bij.has_inverse as inj.is_bij_to_ran gives us a bijection between A and ran(f)
1152lemma inj.is_inv_srj [f g A B : term] : (f ∈ (A ↣ B)) (A ≠ ∅)
1153 |- ∃g, g ∈ (B ↠ A)
1154proof
1155 follows f ∈ (A → B) by inj_on.def;
1156 hence f[A] = ran(f) by dom.is_ran_under_image;
1157 suffices ∃h, ∃w, h ∈ (B ↠ ran(f)) ∧ w ∈ (ran(f) ↠ A) by comp_surj.is_surj;
1158 hence ∃w, w ∈ (ran(f) ↠ A) as
1159 follows f ∈ (A ↔ ran(f)) by inj.is_bij_to_ran;
1160 furthermore ∃w₀, w₀ ∈ (ran(f) ↔ A) by bij.has_inverse;
1161 done by bij_on.is_inj_and_surj
1162 ;
1163 furthermore ran(f) ⊆ B by fn_on.is_fn;
1164 follows ran(f) ≠ ∅ by image.def, nonempty.has_element;
1165 hence ∃h, h ∈ (B ↠ ran(f)) by sub.has_surj;
1166 done by comp_surj.is_surj
1167qed
1169theorem shroeder_bernstein [A B : term] : (∃f, f ∈ (A ↣ B)) (∃g, g ∈ (B ↣ A))
1170 |- ∃h, h ∈ (A ↔ B)
1171proof
1172 todo
1173qed
The Ordinals 3.5
36module set.ordinal
Definitions
2module set.ordinal.def
Our first goal upon the completion of our development of set theory will be to define the natural numbers. We will not develop the natural numbers directly but we will instead consider them to be certain "ordinal" numbers. So we will start by developing the ordinals.
The intuitive definition of the ordinal numbers is as follows: The empty set is an ordinal number and any set which contains every previously defined ordinal is an ordinal number. The goal is to produce a canonical set with each "number" of elements. The problem is that this definition is recursive and we will need ordinals before we can define recursion. Luckily, the ordinals admit an alternate definition. We define an ordinal as a transitive set that is well ordered by .
A transitive set is one where every element is also a subset.
16definition
17 transitive(α) := ∀x ∈ α, x ⊆ α
18end
20theorem transitive.def [α : term] :
21 |- transitive(α) ↔ ∀x ∈ α, x ⊆ α
22proof
23 done by iff.refl [transitive(α)]
24qed
A well ordered set is one where every non-empty subset has a least element.
28definition
29 is_least(α, β) := α ∈ β ∧ (∀γ ∈ β, γ ≠ α → α ∈ γ)
30end
32theorem is_least.def [α β : term] :
33 |- is_least(α, β) ↔ α ∈ β ∧ (∀γ ∈ β, γ ≠ α → α ∈ γ)
34proof
35 done by iff.refl [is_least(α, β)]
36qed
38definition
39 well_ordered(α) := ∀β, β ⊆ α ∧ β ≠ ∅ → ∃γ, is_least(γ, β)
40end
42theorem well_ordered.def [α : term] :
43 |- well_ordered(α) ↔ ∀β, β ⊆ α ∧ β ≠ ∅ → ∃γ, is_least(γ, β)
44proof
45 done by iff.refl [well_ordered(α)]
46qed
The combination of these two properties is what defines an ordinal.
50definition
51 α : Ord := transitive(α) ∧ well_ordered(α)
52end
54theorem ordinal.def [α : term] :
55 |- α : Ord ↔ transitive(α) ∧ well_ordered(α)
56proof
57 done by iff.refl [α : Ord]
58qed
Since well orders an ordinal, we can think of as being for ordinals. It would be helpful, then, to know that is anti-reflexive and anti-symmetric. These two properties follows by classic proofs from the axiom of regularity.
65lemma mem.irrefl [a : term] :
66 |- a ∉ a
67proof
68 follows ∃x, x ∈ {a} by singleton.def;
69 obtain y st y ∈ {a} ∧ ¬∃z, (z ∈ y ∧ z ∈ {a}) by zfc.regularity;
70 done by singleton.def
71qed
73lemma mem.no_loop [a b : term] :
74 |- ¬(a ∈ b ∧ b ∈ a)
75proof
76 follows ∃x, x ∈ {a, b} by pair.def;
77 obtain y st y ∈ {a, b} ∧ ¬∃z, (z ∈ y ∧ z ∈ {a, b}) by zfc.regularity;
78 -- if y = a then b ∈ a ∧ b ∈ {a, b} would lead to a contradiction and
79 -- vice versa. just let vampire work it out.
80 done by pair.def
81qed
Our First Ordinals
5module set.ordinal.basic
We are now ready for our first proof about ordinals. Recall from our intuative definition that we wanted to be the first ordinal number. Another way of thinking about this is that can be thought of as and any ordinal is the set of every previous ordinal. Thus, it stands to reason that the first ordinal is . The proof that satisfies our definition is easy; the two required properties are vacuous when applied to the empty set.
9theorem ordinal.empty.is :
10 |- ∅ : Ord
11proof
12 follows transitive(∅) as
13 suffices ∀x ∈ ∅, x ⊆ ∅ by transitive.def;
14 follows ∀x, x ∉ ∅ by empty.def;
15 done logically
16 ;
17
18 follows well_ordered(∅) as
19 suffices ∀β, β ⊆ ∅ ∧ β ≠ ∅ → ∃γ, is_least(γ, β) by well_ordered.def;
20 follows ∀β, β ⊆ ∅ → β = ∅ by empty.sub_is_empty;
21 done logically
22 ;
23
24 thus ∅ : Ord by ordinal.def given transitive(∅) and well_ordered(∅);
25qed
The empty set is the zero of the ordinal numbers. We can get the next ordinal from any previous ordinal number by applying the successor operation. If is an ordinal then it is the set of all previous ordinals. So the next ordinal after should include all the ordinals in and itself. Hence the definition.
33definition
34 succ(n) := n ∪ {n}
35end
37theorem ordinal.succ.def [n : term] :
38 |- succ(n) = n ∪ {n}
39proof
40 done by eq.refl [succ(n)]
41qed
We can prove now that the result we get is still an ordinal. This proof isn't conceptually complicated but it has a few things to check.
46theorem ordinal.succ.is [α : term] : (α : Ord)
47 |- succ(α) : Ord
48proof
49 follows succ(α) = α ∪ {α} by ordinal.succ.def;
50
51 follows transitive(succ(α)) as
52 suffices ∀x ∈ succ(α), x ⊆ succ(α) by transitive.def;
53 arbitrary x st x ∈ succ(α);
54
55 -- x is either from α or is α. split on which case we are in.
56 follows x ∈ α ∨ x = α by union.def, singleton.def given succ(α) = α ∪ {α};
57
58 cases:
59 | x ∈ α then
60 follows transitive(α) by ordinal.def given α : Ord;
61 thus x ⊆ α by transitive.def;
62 follows α ⊆ succ(α) by union.left_sub;
63 done by sub.trans
64 | x = α then
65 done by union.left_sub given succ(α) = α ∪ {α}
66 ;
67
68 follows well_ordered(succ(α)) as
69 suffices ∀β, β ⊆ succ(α) ∧ β ≠ ∅ → ∃γ, is_least(γ, β) by well_ordered.def;
70 arbitrary β st β ⊆ succ(α) ∧ β ≠ ∅;
71
72 -- there are two cases. either β = {α} in which case α is the least
73 -- element or β ∩ α ≠ ∅ in which case we can use the well orderedness of
74 -- α to get a least element from it.
75 assume β = {α} then is_least(α, β) as
76 suffices α ∈ β ∧ (∀γ ∈ β, γ ≠ α → α ∈ γ);
77 follows α ∈ β by singleton.def given β = {α};
78 follows ¬∃γ ∈ β, γ ≠ α by singleton.def;
79 done logically
80 ;
81
82 assume β ≠ {α} then ∃γ, is_least(γ, β) as
83 -- consider only the subset of β in α
84 let β' := β ∩ α;
85 follows β' ⊆ α ∧ β' ⊆ β by inter.sub_right, inter.sub_left;
86 follows β' ≠ ∅ as
87 obtain x st x ∈ β ∧ x ≠ α as
88 suffices ¬∀x ∈ β, x = α logically;
89 assume ∀x ∈ β, x = α for_contra;
90 thus β = {α} by singleton.def, nonempty.has_element, zfc.extensionality;
91 contradiction
92 ;
93 follows x ∈ succ(α) by sub.def given β ⊆ succ(α) and x ∈ β;
94 follows x ∈ α by ordinal.succ.def, union.def, singleton.def;
95 thus x ∈ β' by inter.def given x ∈ α and x ∈ β;
96 thus β' ≠ ∅ by nonempty.has_element;
97 ;
98 -- we get the minimal element of this subset by the well ordering of α
99 follows well_ordered(α) by ordinal.def given α : Ord;
100 obtain γ st is_least(γ, β') by well_ordered.def;
101 thus γ ∈ β' ∧ (∀δ ∈ β', δ ≠ γ → γ ∈ δ) by is_least.def;
102 -- we want that this is still the least element of β
103 suffices is_least(γ, β) logically;
104 suffices γ ∈ β ∧ (∀δ ∈ β, δ ≠ γ → γ ∈ δ) by is_least.def;
105 -- it's in β just because β' ⊆ β
106 follows γ ∈ β by sub.def given γ ∈ β' and β' ⊆ β;
107 follows ∀δ ∈ β, δ ≠ γ → γ ∈ δ as
108 arbitrary δ st δ ∈ β; assume δ ≠ γ;
109 -- any element of β is either in α or is α. split on which case.
110 follows δ ∈ α ∨ δ = α by union.def, singleton.def, sub.def
111 given δ ∈ β and β ⊆ succ(α) and succ(α) = α ∪ {α};
112
113 cases:
114 | δ ∈ α then
115 follows δ ∈ β' by inter.def given δ ∈ β and δ ∈ α;
116 done given ∀δ ∈ β, δ ≠ γ → γ ∈ δ
117 | δ = α then done by sub.def given γ ∈ β' and β' ⊆ α
118 ;
119
120 done logically
121 ;
122
123 done logically
124 ;
125
126 thus succ(α) : Ord by ordinal.def given transitive(succ(α)) and well_ordered(succ(α));
127qed
Properties
8module set.ordinal.props
Returning to our characterization of ordinals as sets containing every previous ordinal, we want to prove that every element of an ordinal is an ordinal. Doing this will require several new lemmas.
First we will prove that we have the trichotomy property for members of an ordinal. We will have a stronger trichotomy on all ordinals later but since we do not yet know that the elements of an ordinal are still ordinals, we cannot apply it.
10lemma ordinal.internal_trichotomy [α β γ : term] : (α : Ord) (β ∈ α) (γ ∈ α)
11 |- γ ∈ β ∨ γ = β ∨ β ∈ γ
12proof
13 follows transitive(α) ∧ well_ordered(α) by ordinal.def;
14
15 -- The idea here is that {β, γ} ⊆ α so it must have a least element.
16 follows {β, γ} ⊆ α by pair.def, sub.def given β ∈ α and γ ∈ α;
17 follows {β, γ} ≠ ∅ by pair.non_empty;
18
19 -- the least element δ must be either β or γ
20 obtain δ st is_least(δ, {β, γ}) by well_ordered.def given well_ordered(α);
21 follows δ ∈ {β, γ} by is_least.def given is_least(δ, {β, γ});
22 follows δ = β ∨ δ = γ by pair.def;
23
24 -- whichever one δ is it must be either equal to or in the other
25 follows ∀η ∈ {β, γ}, η ≠ δ → δ ∈ η by is_least.def given is_least(δ, {β, γ});
26 follows ∀η ∈ {β, γ}, η = δ ∨ δ ∈ η logically;
27 follows β = δ ∨ δ ∈ β by pair.def;
28 follows γ = δ ∨ δ ∈ γ by pair.def;
29
30 -- which suffices. you can check the cases on δ = β ∨ δ = γ
31 done logically
32qed
We will also need the fact that is transitive inside an ordinal. Again, we will have a stronger, non-internal version of this later.
37lemma ordinal.internal_trans [α β γ δ : term] : (α : Ord) (β ∈ α) (γ ∈ α) (δ ∈ α)
38 (β ∈ γ) (γ ∈ δ)
39 |- β ∈ δ
40proof
41 -- the idea here is to use the well ordering of α to find a minimal element
42 -- in {β, γ, δ}. If it is β we are happy. If it is γ we have a contradiction
43 -- from β ∈ γ and γ ∈ β. If it is δ then we have one from γ ∈ δ and δ ∈ γ.
44 let S := {β} ∪ {γ} ∪ {δ};
45 follows ∀x, x ∈ S ↔ x = β ∨ x = γ ∨ x = δ by singleton.def, union.def;
46
47 -- obtain the least element of S
48 thus S ⊆ α ∧ S ≠ ∅ by sub.def, empty.def;
49 follows well_ordered(α) by ordinal.def;
50 obtain η st is_least(η, S) by well_ordered.def;
51 thus η ∈ S by is_least.def;
52
53 cases:
54 | η = γ then
55 follows γ ∈ β by is_least.def;
56 contradiction by mem.no_loop given β ∈ γ
57 | η = δ then
58 follows δ ∈ γ by is_least.def;
59 contradiction by mem.no_loop given γ ∈ δ
60 | η = β then
61 follows β ∈ δ by is_least.def;
62qed
Now we are ready for the theorem itself.
66theorem ordinal.mem.is [α β : term] : (α ∈ β) (β : Ord)
67 |- α : Ord
68proof
69 follows well_ordered(β) ∧ transitive(β) by ordinal.def;
70
71 follows transitive(α) as
72 suffices ∀x ∈ α, x ⊆ α by transitive.def;
73 arbitrary x st x ∈ α;
74 suffices ∀y ∈ x, y ∈ α by sub.def;
75 arbitrary y st y ∈ x;
76
77 follows α ⊆ β by transitive.def given transitive(β) and α ∈ β;
78 thus x ∈ β by sub.def given x ∈ α;
79 thus x ⊆ β by transitive.def;
80 thus y ∈ β by sub.def;
81
82 cases by ordinal.internal_trichotomy:
83 | y ∈ α then
84 done
85 | y = α then
86 -- we have y ∈ x ∈ α so we get α ∈ x ∈ α, a contradiction.
87 follows α ∈ x given y ∈ x;
88 contradiction by mem.no_loop given x ∈ α
89 | α ∈ y then
90 -- α ∈ y ∈ x ∈ α, also a contradiction.
91 follows α ∈ x by ordinal.internal_trans given α ∈ y and y ∈ x;
92 contradiction by mem.no_loop given x ∈ α
93 ;
94
95 follows well_ordered(α) as
96 suffices ∀δ, δ ⊆ α ∧ δ ≠ ∅ → ∃γ, is_least(γ, δ) by well_ordered.def;
97 arbitrary δ st δ ⊆ α ∧ δ ≠ ∅;
98
99 -- by the transitivity of β, α ⊆ β, so δ ⊆ β as well. and then we use
100 -- the well ordering of β.
101 follows α ⊆ β by transitive.def given α ∈ β and transitive(β);
102 thus δ ⊆ β by sub.trans given δ ⊆ α;
103 thus ∃γ, is_least(γ, δ) by well_ordered.def given well_ordered(β) and δ ⊆ α ∧ δ ≠ ∅;
104 ;
105
106 done by ordinal.def
107qed
With this theorem we can now make proper use of the full ordinal trichotomy, although the proof of the trichotomy does not actually rely on the members of an ordinal being in ordinal. It will, however, need two more lemmas. First, the intersection of two ordinals is an ordinal. Intuitively, the intersection is just the smaller ordinal.
115theorem ordinal.inter.is [α β : term] : (α : Ord) (β : Ord)
116 |- α ∩ β : Ord
117proof
118 follows transitive(α ∩ β) as
119 suffices ∀γ ∈ α ∩ β, γ ⊆ α ∩ β by transitive.def;
120 arbitrary γ st γ ∈ α ∩ β;
121 follows γ ∈ α ∧ γ ∈ β by inter.def;
122
123 follows γ ⊆ α by ordinal.def, transitive.def given α : Ord;
124 follows γ ⊆ β by ordinal.def, transitive.def given β : Ord;
125 thus γ ⊆ α ∩ β by inter.sub_both;
126 ;
127
128 follows well_ordered(α ∩ β) as
129 suffices ∀δ, δ ⊆ α ∩ β ∧ δ ≠ ∅ → ∃γ, is_least(γ, δ);
130 arbitrary δ st δ ⊆ α ∩ β ∧ δ ≠ ∅;
131 follows δ ⊆ α by inter.left_sub;
132 obtain γ st is_least(γ, δ) by ordinal.def, well_ordered.def;
133 done logically
134 ;
135
136 done by ordinal.def
137qed
Ordinals are transitive but they also have the inverse property: any subset is a member. Unless the subset is just the original set.
142theorem ordinal.sub_mem [α β : term] : (α : Ord) (β : Ord) (β ⊆ α)
143 |- β ∈ α ∨ β = α
144proof
145 -- we just need to show β ∈ α if β ≠ α
146 suffices β ≠ α → β ∈ α logically; assume β ≠ α;
147
148 -- construct α - β which is a non-empty subset of α.
149 let S := α - β;
150 follows S ⊆ α by set_diff.sub;
151 follows S ≠ ∅ by set_diff.non_empty given β ≠ α;
152
153 -- we claim that the least element in S is β which suffices.
154 obtain μ st is_least(μ, S) by ordinal.def, well_ordered.def given α : Ord;
155 follows μ ∈ S by is_least.def;
156 follows μ ∈ α by set_diff.def;
157 follows μ ∉ β by set_diff.def;
158 follows μ ⊆ α by ordinal.def, transitive.def given α : Ord;
159 suffices μ = β logically;
160
161 follows μ ⊆ β as
162 suffices ∀δ ∈ μ, δ ∈ β by sub.def;
163 arbitrary δ st δ ∈ μ;
164
165 -- idea: δ must be in β because otherwise it would be in S and then we
166 -- would have μ ∈ δ and δ ∈ μ
167 assume δ ∉ β for_contra;
168 follows δ ∈ α by sub.def given δ ∈ μ and μ ⊆ α;
169 thus δ ∈ S by set_diff.def;
170
171 follows δ ≠ μ by mem.irrefl given δ ∈ μ;
172 thus μ ∈ δ by is_least.def given δ ∈ S and is_least(μ, S);
173 contradiction by mem.no_loop given δ ∈ μ and μ ∈ δ
174 ;
175
176 follows β ⊆ μ as
177 suffices ∀δ ∈ β, δ ∈ μ by sub.def;
178 arbitrary δ st δ ∈ β;
179
180 -- the idea here is that μ ∉ δ because if it was then μ would be in δ
181 -- by transitivity. so then it must be that δ ∈ μ by transitivity in α
182 follows δ ≠ μ given δ ∈ β and μ ∉ β;
183 follows μ ∉ δ as
184 assume μ ∈ δ for_contra;
185 follows δ ⊆ β by ordinal.def, transitive.def given β : Ord and δ ∈ β;
186 follows μ ∈ β by sub.def;
187 contradiction
188 ;
189
190 follows δ ∈ α by sub.def given β ⊆ α and δ ∈ β;
191 thus δ ∈ μ by ordinal.internal_trichotomy given δ ≠ μ and μ ∉ δ;
192 ;
193
194 thus μ = β by sub.sub_eq;
195qed
With these facts we can prove the full trichotomy theorem.
199theorem ordinal.trichotomy [α β : term] : (α : Ord) (β : Ord)
200 |- α ∈ β ∨ α = β ∨ β ∈ α
201proof
202 let γ := α ∩ β;
203 follows γ : Ord by ordinal.inter.is;
204
205 -- since γ is a subset of both α and β we have that it either is or
206 -- is a member of each
207 follows γ ⊆ α by inter.sub_left;
208 follows γ ∈ α ∨ γ = α by ordinal.sub_mem;
209 follows γ ⊆ β by inter.sub_right;
210 follows γ ∈ β ∨ γ = β by ordinal.sub_mem;
211
212 -- but it can't be a member of both because then it would be a member of itself.
213 follows ¬(γ ∈ α ∧ γ ∈ β) as
214 assume γ ∈ α ∧ γ ∈ β for_contra;
215 thus γ ∈ γ by inter.def;
216 contradiction by mem.irrefl
217 ;
218
219 -- so γ must be one of α and β. split on which case we are in.
220 follows γ = α ∨ γ = β logically;
221
222 cases:
223 | γ = α ∧ γ = β then
224 follows α = β logically;
225 done logically
226 | γ = α ∧ γ ≠ β then
227 follows γ ∈ β given γ ∈ β ∨ γ = β;
228 thus α ∈ β logically;
229 done logically
230 | γ ≠ α ∧ γ = β then
231 follows γ ∈ α given γ ∈ α ∨ γ = α;
232 thus β ∈ α logically;
233 done logically
234qed
We can also write down the full transitivity property. This is really just a restatement of transitivity.
239theorem ordinal.trans [α β γ : term] : (γ : Ord) (α ∈ β) (β ∈ γ)
240 |- α ∈ γ
241proof
242 follows β ⊆ γ by ordinal.def, transitive.def;
243 thus α ∈ γ by sub.def;
244qed
Induction
11module set.ordinal.induction
We now arrive at one of the most important facts about ordinals. Just like the natural numbers, ordinals satisfy strong induction. (In fact, the naturals are just a special case of the ordinals). In some ways, induction is definitional. It is just another way of stating the well ordering property.
6theorem ordinal.induction [p(_) : sentence(term)] : (∀α, (α : Ord ∧ ∀β ∈ α, p(β)) → p(α))
7 |- ∀α, α : Ord → p(α)
8proof
9 -- suppose we have an ordinal such that ¬p
10 assume ¬(∀α, α : Ord → p(α)) for_contra;
11 obtain α st α : Ord ∧ ¬p(α) logically;
12
13 let s := {δ ∈ succ(α) | ¬p(δ)};
14
15 -- s is a non-empty subset of succ(α)
16 follows s ⊆ succ(α) by sub.def;
17 follows α ∈ succ(α) by ordinal.succ.def, union.def, singleton.def;
18 follows s ≠ ∅ by empty.def;
19
20 -- thus, since succ(α) is well ordered, we can find the least element.
21 follows succ(α) : Ord by ordinal.succ.is;
22 thus well_ordered(succ(α)) by ordinal.def;
23 obtain μ st is_least(μ, s) by well_ordered.def;
24
25 -- μ is an ordinal since it is in succ(α)
26 follows μ ∈ s by is_least.def;
27 follows μ ∈ succ(α) logically;
28 follows μ : Ord by ordinal.mem.is;
29
30 -- every member β of μ satisfies p because otherwise it would be in s.
31 follows ∀β ∈ μ, p(β) as
32 arbitrary β st β ∈ μ;
33 assume ¬p(β) for_contra;
34
35 -- we get that β is in s
36 follows μ ⊆ succ(α) by ordinal.def, transitive.def given μ ∈ succ(α);
37 thus β ∈ succ(α) by sub.def given β ∈ μ;
38 thus β ∈ s given ¬p(β) and β ∈ succ(α);
39
40 -- but then it can't be the case that β ∈ μ since μ is least in s
41 follows β ≠ μ by mem.irrefl given β ∈ μ;
42 thus μ ∈ β by is_least.def given β ∈ s and is_least(μ, s);
43 contradiction by mem.no_loop given β ∈ μ and μ ∈ β
44 ;
45
46 thus p(μ) logically;
47 follows ¬p(μ) given μ ∈ s;
48 contradiction
49qed
Sometimes we don't want something for all ordinals but just for all ordinals up to some ceiling. That version is a simple corollary.
54corollary ordinal.induction.up_to [p(_) : sentence(term)] [α : term] : (α : Ord)
55 (∀β ∈ α, (∀γ ∈ β, p(γ)) → p(β))
56 |- ∀β ∈ α, p(β)
57proof
58 suffices ∀β, β ∈ α → p(β);
59 suffices ∀β, β : Ord → (β ∈ α → p(β)) by ordinal.mem.is;
60 suffices ∀β, (β : Ord ∧ (∀γ ∈ β, γ ∈ α → p(γ))) → (β ∈ α → p(β))
61 by ordinal.induction [_ ∈ α → p(_)];
62
63 arbitrary β;
64 assume β : Ord ∧ (∀γ ∈ β, γ ∈ α → p(γ));
65 assume β ∈ α;
66
67 follows ∀γ ∈ β, γ ∈ α by ordinal.trans;
68 follows ∀γ ∈ β, p(γ) logically;
69 thus p(β) given ∀β ∈ α, (∀γ ∈ β, p(γ)) → p(β) and β ∈ α;
70qed
Omega
14module set.ordinal.omega
As mentioned a few times, the natural numbers are a particular subset of the ordinals. Specifically, they are the ordinals that can be made by starting with the empty set and repeatedly applying the successor operation. It may not be obvious that this isn't just all the ordinals. In, fact, if we did not have the axiom of infinity this would be all the ordinals! But with the axiom of infinity we can prove the existence of a the set containing all the natural numbers. We call this set and it is actually an ordinal itself, since it contains all previous ordinals. Since we cannot reach using the successor operation from previous ordinals, we call it a limit ordinals.
The defining property of is that it is the smallest set which contains and is closed under the successor operation. We will call this closure property inductivity.
15definition
16 inductive(α) := ∅ ∈ α ∧ (∀n ∈ α, succ(n) ∈ α)
17end
19theorem inductive.def [α : term] :
20 |- inductive(α) ↔ ∅ ∈ α ∧ (∀n ∈ α, succ(n) ∈ α)
21proof
22 done by iff.refl [inductive(α)]
23qed
By the smallest set we mean that is a subset of any inductive set. Put another way, is the intersection of the proper class of all inductive sets. However, our theory does not contain proper classes so we cannot use the intersection operator developed previously. We can instead define using an unrestricted comprehension.
31definition
32 ω := {x | ∀α, inductive(α) → x ∈ α}
33end
The ZF axiom of infinity guarantees that at least one inductive set exists, which is what will let us conclude that is well defined.
38lemma inductive.exists :
39 |- ∃α, inductive(α)
40proof
41 suffices ∃α, ∅ ∈ α ∧ ∀n ∈ α, n ∪ {n} ∈ α;
42
43 -- the object whose existence is guaranteed by the axiom of infinity is the
44 -- α that we want.
45 obtain x st (∃y, y ∈ x ∧ ∀z, z ∉ y) ∧ (∀y ∈ x, ∃z ∈ x, ∀w, w ∈ z ↔ w ∈ y ∨ w = y)
46 by zfc.infinity;
47
48 -- the ∃y, y ∈ x ∧ ∀z, z ∉ y tells us that x contains ∅
49 follows ∅ ∈ x by empty.def, zfc.extensionality;
50
51 -- now we need to show that x is closed under the successor operation
52 follows ∀n ∈ x, n ∪ {n} ∈ x as
53 arbitrary n st n ∈ x;
54 obtain z st z ∈ x ∧ (∀w, w ∈ z ↔ w ∈ n ∨ w = n) logically;
55 follows ∀w, w ∈ n ∪ {n} ↔ (w ∈ n ∨ w = n) by singleton.def, union.def;
56 follows z = n ∪ {n} by zfc.extensionality;
57 thus n ∪ {n} ∈ x logically;
58 ;
59
60 done logically
61qed
From this lemma we can deduce that will be well defined, as it is a subset of that inductive set.
66theorem omega.def :
67 |- ∀x, x ∈ ω ↔ (∀α, inductive(α) → x ∈ α)
68proof
69 -- we have at least one inductive set. since ω is an infinite intersection
70 -- restricting the comprehension doesn't change anything. so ω' = ω.
71 obtain α st inductive(α) by inductive.exists;
72 let ω' := {x ∈ α | ∀β, inductive(β) → x ∈ β};
73
74 -- we prove that ω' has the defining property of ω
75 follows ∀y, y ∈ ω' ↔ (∀β, inductive(β) → y ∈ β) as
76 arbitrary y;
77 suffices y ∈ {x ∈ α | ∀β, inductive(β) → x ∈ β} ↔ (∀β, inductive(β) → y ∈ β);
78 assume y ∈ {x ∈ α | ∀β, inductive(β) → x ∈ β} then ∀β, inductive(β) → y ∈ β logically;
79 assume ∀β, inductive(β) → y ∈ β then y ∈ {x ∈ α | ∀β, inductive(β) → x ∈ β} as
80 follows y ∈ α given inductive(α);
81 follows y ∈ α ∧ (∀β, inductive(β) → y ∈ β) logically;
82 done logically
83 ;
84 done logically
85 ;
86
87 -- ω' proves that the infinite intersection exists, so ω is well defined
88 -- and thus has the desired property.
89 thus ∃w, ∀x, x ∈ w ↔ (∀β, inductive(β) → x ∈ β) logically;
90 thus ∀x, x ∈ ω ↔ (∀β, inductive(β) → x ∈ β) by uncomp.def [∀β, inductive(β) → _ ∈ β];
91qed
Since is a subset of all inductive sets, it is itself inductive.
95corollary omega.sub_inductive [a : term] : (inductive(a))
96 |- ω ⊆ a
97proof
98 done by omega.def, sub.def
99qed
101corollary omega.inductive :
102 |- inductive(ω)
103proof
104 follows ∀α, inductive(α) → ∅ ∈ α by inductive.def;
105 thus ∅ ∈ ω by omega.def;
106
107 follows ∀n ∈ ω, succ(n) ∈ ω as
108 arbitrary n st n ∈ ω;
109 follows ∀α, inductive(α) → n ∈ α by omega.def;
110 follows ∀α, inductive(α) → succ(n) ∈ α by inductive.def;
111 thus succ(n) ∈ ω by omega.def;
112 ;
113
114 done by inductive.def
115qed
The proof that is an ordinal is rather complex. We will observe first, as a lemma, that all the elements in are ordinals.
120lemma omega.mem.is_ordinal [n : term] : (n ∈ ω)
121 |- n : Ord
122proof
123 let T := {n ∈ ω | n : Ord};
124 follows T ⊆ ω by comp.sub [_ : Ord] [ω];
125
126 follows ∅ : Ord by ordinal.empty.is;
127 follows ∅ ∈ ω by omega.inductive, inductive.def;
128 thus ∅ ∈ T logically;
129
130 follows ∀n ∈ T, succ(n) ∈ T as
131 arbitrary n st n ∈ T;
132
133 follows n : Ord logically;
134 thus succ(n) : Ord by ordinal.succ.is;
135
136 follows n ∈ ω logically;
137 follows succ(n) ∈ ω by omega.inductive, inductive.def;
138
139 thus succ(n) ∈ T logically;
140 ;
141
142 -- thus T is inductive so ω = T and every element of T is an ordinal,
143 -- by definition, so we are done.
144 thus inductive(T) by inductive.def;
145 thus ω ⊆ T by omega.sub_inductive;
146 thus ω = T by sub.sub_eq;
147 done logically
148qed
It requires a few careful arguments to see that is transitive and well ordered.
153theorem ordinal.omega.is :
154 |- ω : Ord
155proof
156 follows transitive(ω) as
157 -- define the set of elements of ω that are subsets of ω. We will show
158 -- that T is inductive, thus T ⊆ ω, thus T = ω, thus ω is transitive.
159 let T := {n ∈ ω | n ⊆ ω};
160 follows T ⊆ ω by comp.sub [_ ⊆ ω] [ω];
161
162 -- T is inductive
163 follows ∅ ∈ T as
164 follows ∅ ∈ ω by omega.inductive, inductive.def;
165 follows ∅ ⊆ ω by empty.is_sub;
166 thus ∅ ∈ T logically;
167 ;
168 follows ∀n ∈ T, succ(n) ∈ T as
169 arbitrary n st n ∈ T;
170 thus n ∈ ω ∧ n ⊆ ω logically;
171 thus succ(n) ∈ ω by omega.inductive, inductive.def;
172 follows n ∪ {n} ⊆ ω as
173 suffices ∀x, x ∈ n ∪ {n} → x ∈ ω;
174 arbitrary x st x ∈ n ∪ {n};
175 follows x = n ∨ x ∈ n by union.def, singleton.def;
176 thus x ∈ ω by sub.def given n ⊆ ω and n ∈ ω;
177 ;
178 thus succ(n) ⊆ ω by ordinal.succ.def;
179 thus succ(n) ∈ T given succ(n) ∈ ω and succ(n) ⊆ ω;
180 ;
181
182 -- T = ω
183 thus inductive(T) by inductive.def;
184 thus ω ⊆ T by omega.sub_inductive;
185 thus ω = T by sub.sub_eq given T ⊆ ω and ω ⊆ T;
186
187 -- T is transitive
188 thus ∀x ∈ ω, x ⊆ ω given ω = T;
189 thus transitive(ω) by transitive.def;
190 ;
191
192 follows well_ordered(ω) as
193 suffices ∀β, β ⊆ ω ∧ β ≠ ∅ → ∃γ, is_least(γ, β) by well_ordered.def;
194 arbitrary β st β ⊆ ω ∧ β ≠ ∅;
195
196 -- idea: we restrict β to a subset of one of it's elements. we know δ+
197 -- is an ordinal so we get a least element in β ∩ δ+ ⊆ δ+ which will
198 -- also be least in β.
199 obtain δ st δ ∈ β by nonempty.has_element;
200 let β' := β ∩ succ(δ);
201
202 -- β' is a non-empty subset of succ(δ)
203 follows β' ⊆ succ(δ) by inter.sub_right;
204 follows δ ∈ succ(δ) by ordinal.succ.def, union.def, singleton.def;
205 thus δ ∈ β' by inter.def;
206 thus β' ≠ ∅ by nonempty.has_element;
207
208 -- it follows that succ(δ) is an ordinal
209 follows β ⊆ ω given transitive(ω);
210 thus δ ∈ ω by sub.def given δ ∈ β;
211 thus δ : Ord by omega.mem.is_ordinal;
212 thus succ(δ) : Ord by ordinal.succ.is;
213
214 -- therefore can obtain a least element in β'
215 thus well_ordered(succ(δ)) by ordinal.def;
216 obtain γ st is_least(γ, β') by well_ordered.def;
217
218 -- we want to claim γ is also least in β.
219 suffices is_least(γ, β) logically;
220
221 follows γ ∈ β' by is_least.def given is_least(γ, β');
222 follows γ ∈ β by inter.def;
223 suffices ∀η ∈ β, η ≠ γ → γ ∈ η by is_least.def;
224
225 -- assume there was some smaller element η ∈ β.
226 arbitrary η st η ∈ β; assume η ≠ γ;
227 assume γ ∉ η for_contra;
228 follows η ∈ γ as
229 follows η ∈ ω by sub.def given η ∈ β and β ⊆ ω;
230 follows γ ∈ ω by sub.def given γ ∈ β and β ⊆ ω;
231 thus η : Ord ∧ γ : Ord by omega.mem.is_ordinal;
232 thus η ∈ γ by ordinal.trichotomy given η ≠ γ and γ ∉ η;
233 ;
234
235 -- that η would also have to be in β' since succ(δ) is transitive.
236 follows γ ∈ succ(δ) by inter.def given γ ∈ β';
237 follows γ ⊆ succ(δ) by ordinal.def, transitive.def given succ(δ) : Ord;
238 thus η ∈ succ(δ) by sub.def given η ∈ γ;
239 thus η ∈ β' by inter.def given η ∈ β and η ∈ succ(δ);
240
241 -- but then we have both η ∈ γ and γ ∈ η.
242 thus γ ∈ η by is_least.def given is_least(γ, β');
243 contradiction by mem.no_loop given η ∈ γ and γ ∈ η
244 ;
245
246 done by ordinal.def
247qed
Since is an ordinal induction holds inside of it. From this we get induction on the natural numbers!
252corollary omega.strong_induction [p(_) : sentence(term)] : (∀n ∈ ω, (∀m ∈ n, p(m)) → p(n))
253 |- ∀n ∈ ω, p(n)
254proof
255 follows ω : Ord by ordinal.omega.is;
256 done by ordinal.induction.up_to [p(_)] [ω]
257qed
Recursion
17module set.ordinal.recursion
The next thing we want to do is define operations on ordinals. In order to do this we will need recursion. It isn't obvious a priori that recursive operations are well defined. In fact, every recursive definition needs a proof to go with it. For example, and is clearly well defined, it is the factorial function. Whereas and is nonsense, despite just changing a to a .
In order to define a recursive function , we will make use of an auxiliary function . The idea is that has the property that, for all ordinals , , i.e. that produces the next value of given the partial function of all previous values of . Except, we will define instead of and use it to produce .
The key fact we will prove, is that if satisfies the property for all , then is a restriction of . In particular . Thus, we only have to find some way of identifying functions with that property, and then is easily defined via the union of all such functions.
We will call a function with the given property coherent (not a standard term). This property is relative to . Note that, since is a function over the whole class of ordinals, it is not a set, so we need to be slightly more verbose.
25notation sentence.with_term_of_term_and_term
26 sentence ::= @name "(" x:@binding(term) "↦" term(x) "," term ")"
27end
29definition
30 coherent(f' ↦ g(f'), f) := ∀β ∈ dom(f), f(β) = g(f ↾ β)
31end
And the theorem is that all coherent functions with the same domain are equal.
35theorem coherent.unique [g(_) : term(term)] [f₁ f₂ : term] : (f₁ : Fn) (f₂ : Fn)
36 (dom(f₁) = dom(f₂)) (dom(f₁) : Ord) (coherent(f' ↦ g(f'), f₁))
37 (coherent(f' ↦ g(f'), f₂))
38 |- f₁ = f₂
39proof
40 let α := dom(f₁);
41 -- to prove two functions are equal, we show they are equal on their domains.
42 suffices ∀β ∈ α, f₁(β) = f₂(β) as todo;
43 -- we can complete the proof by induction.
44 suffices ∀β ∈ α, (∀γ ∈ β, f₁(γ) = f₂(γ)) → f₁(β) = f₂(β)
45 by ordinal.induction.up_to [f₁(_) = f₂(_)] [α]; -- todo: induction tactic
46
47 arbitrary β st β ∈ α;
48 assume ∀γ ∈ β, f₁(γ) = f₂(γ);
49
50 -- since f₁ is coherent, f₁(β) = g(f₁ ↾ β). And the same for f₂
51 follows f₁(β) = g(f₁ ↾ β) as todo;
52 follows f₂(β) = g(f₂ ↾ β) as todo;
53
54 -- but f₁ ↾ β = f₂ ↾ β so we are done.
55 follows f₁ ↾ β = f₂ ↾ β as todo; -- by fn.restriction.eq;
56 done as todo
57qed
And for each ordinal there exists a coherent function with that ordinal as its domain. This is a simple inductive argument.
62theorem coherent.exists [g(_) : term(term)] [α : term] : (α : Ord)
63 |- ∃f, dom(f) = α ∧ coherent(f' ↦ g(f'), f)
64proof
65 todo
66qed
Together, these facts let us pick the coherent function with each length. We will call this the recursive partial function with domain .
71notation term.with_term_of_term_and_term
72 term ::= @name "(" x:@binding(term) "↦" term(x) "," term ")"
73end
75definition
76 rec.partial(f' ↦ g(f'), α) := ℩f, dom(f) = α ∧ coherent(f' ↦ g(f'), f)
77end
And this allows us to define the recursive function itself simply as the value returned by each of these partial functions.
82definition
83 rec(f' ↦ g(f'), α) := rec.partial(f' ↦ g(f'), α)(α)
84end
And we need to prove that this definition produces a recursive function with the desired property.
89theorem recursion.def [g(_) : term(term)] [α : term] : (α : Ord)
90 |- rec(f' ↦ g(f'), α) = g(β ∈ α ↦ rec(f' ↦ g(f'), β))
91proof
92 todo
93qed
The Natural Numbers 3.6
39module set.nat
Numerals and Induction
2module set.nat.basic
1notation zero
2 term ::= "0"
3end
5@[reducible]
6definition
7 0 := ∅
8end
10notation one
11 term ::= "1"
12end
14@[reducible]
15definition
16 1 := succ(0)
17end
19notation two
20 term ::= "2"
21end
23@[reducible]
24definition
25 2 := succ(1)
26end
28theorem nat.one.eq :
29 |- 1 = {∅}
30proof
31 follows succ(∅) = ∅ ∪ {∅} by ordinal.succ.def;
32 follows ∀x, x ∈ ∅ ∪ {∅} ↔ x ∈ {∅} by union.def, empty.def;
33 done by zfc.extensionality
34qed
36theorem nat.two.eq :
37 |- 2 = {∅, {∅}}
38proof
39 hence succ(1) = 1 ∪ {1} by ordinal.succ.def;
40 follows succ(1) = {0} ∪ {1} by nat.one.eq;
41 hence ∀x, x ∈ {0} ∪ {1} ↔ (x ∈ {0} ∨ x ∈ {1}) by union.def;
42 furthermore ∀x, (x ∈ {0} ∨ x ∈ {1}) ↔ (x = 0 ∨ x = 1) by singleton.def;
43 furthermore ∀x, (x = 0 ∨ x = 1) ↔ x ∈ {0, 1} by pair.def;
44 done by zfc.extensionality, nat.one.eq
45qed
47corollary nat.zero.is :
48 |- 0 ∈ ω
49proof
50 done by omega.inductive, inductive.def
51qed
53corollary nat.succ.is [n : term] : (n ∈ ω)
54 |- succ(n) ∈ ω
55proof
56 done by omega.inductive, inductive.def
57qed
59theorem nat.succ.ne_zero [n : term] :
60 |- succ(n) ≠ 0
61proof
62 follows n ∈ succ(n) by ordinal.succ.def, union.def, singleton.def;
63 done by nonempty.has_element
64qed
66theorem nat.weak_induction [p(_) : sentence(term)] : (p(0)) (∀n ∈ ω, p(n) → p(succ(n)))
67 |- ∀n ∈ ω, p(n)
68proof
69 let T := {n ∈ ω | p(n)};
70 follows ∀y, y ∈ T ↔ (y ∈ ω ∧ p(y)) by comp.def [p(_)] [ω];
71 hence 0 ∈ T by nat.zero.is;
72 follows ∀n ∈ T, succ(n) ∈ T by nat.succ.is;
73 thus inductive(T) by inductive.def;
74 thus ω ⊆ T by omega.sub_inductive;
75 done by sub.def
76qed
We prove the following important result by induction on the naturals.
80theorem nat.zero_or_succ [k : term] : (k ∈ ω)
81 |- k = 0 ∨ ∃m ∈ ω, k = succ(m)
82proof
83 -- Our base case
84 follows 0 = 0 ∨ (∃m ∈ ω, 0 = succ(m)) logically;
85 -- We show that our n + 1 case follows from our n case as n itself is the predecessor of n + 1
86 follows ∀n ∈ ω, (n = 0 ∨ (∃m ∈ ω, n = succ(m))) → (succ(n) = 0 ∨ (∃i ∈ ω, succ(n) = succ(i))) logically;
87 thus ∀n ∈ ω, n = 0 ∨ (∃m ∈ ω, n = succ(m))
88 by nat.weak_induction [_ = 0 ∨ ∃m ∈ ω, _ = succ(m)];
89 done logically
90qed
92lemma ordinal.succ.mem [n x : term] :
93 |- x ∈ succ(n) ↔ (x ∈ n ∨ x = n)
94proof
95 done by ordinal.succ.def, union.def, singleton.def
96qed
98theorem nat.succ.inj [n m : term] : (n ∈ ω) (m ∈ ω)
99 |- succ(n) = succ(m) → n = m
100proof
101 follows n ∈ succ(n) ∧ m ∈ succ(m) by ordinal.succ.def, union.def, singleton.def;
102 assume succ(n) = succ(m) then n = m as
103 follows (n ∈ m ∨ n = m) ∧ (m ∈ n ∨ m = n) by ordinal.succ.mem;
104 done by mem.no_loop;
105qed