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
The Powerset
We will define the powerset as the set of all subsets of a set.
764definition
765 𝒫(a) := {x | x ⊆ a}
766end
The existence of this set is provided by one of the ZFC axioms in the same manner as before.
771theorem powset.def [a : term] :
772 |- ∀x, x ∈ 𝒫(a) ↔ x ⊆ a
773proof
774 suffices ∀x, x ∈ {y | y ⊆ a} ↔ x ⊆ a;
775 follows ∃b, ∀x, x ∈ b ↔ (∀y, y ∈ x → y ∈ a) by zfc.powerset;
776 thus ∃b, ∀x, x ∈ b ↔ x ⊆ a;
777 thus ∀x, x ∈ {y | y ⊆ a} ↔ x ⊆ a by uncomp.def [_ ⊆ a];
778qed
The singletons and pairs of elements from the original set are both examples of sets in the powerset.
783theorem powset.singleton_in [a A : term] : (a ∈ A)
784 |- {a} ∈ 𝒫(A)
785proof
786 follows {a} ⊆ A by singleton.sub;
787 thus {a} ∈ 𝒫(A) by powset.def;
788qed
790theorem powset.pair_in [a b A : term] : (a ∈ A) (b ∈ A)
791 |- {a, b} ∈ 𝒫(A)
792proof
793 follows {a, b} ⊆ A by pair.sub;
794 thus {a, b} ∈ 𝒫(A) by powset.def;
795qed
If
Using restricted comprehensions we can define the if then else operator. This will be useful for casewise definitions.
802notation if
803 term ::= "if " sentence " then " term " else " term
804end
806definition
807 if p then a else b := {x ∈ a | p} ∪ {x ∈ b | ¬p}
808end
810theorem union.empty [a : term] :
811 |- a ∪ ∅ = a
812proof
813 todo
814qed
816theorem empty.union [a : term] :
817 |- ∅ ∪ a = a
818proof
819 done by union.empty, union.symm
820qed
822theorem if.true [p : sentence] [a b : term] : (p)
823 |- if p then a else b = a
824proof
825 suffices {x ∈ a | p} ∪ {x ∈ b | ¬p} = a;
826 follows {x ∈ a | p} = a given p;
827 follows {x ∈ b | ¬p} = ∅ by empty.def given p;
828 follows a ∪ ∅ = a by union.empty;
829 done logically
830qed
832theorem if.false [p : sentence] [a b : term] : (¬p)
833 |- if p then a else b = b
834proof
835 suffices {x ∈ a | p} ∪ {x ∈ b | ¬p} = b;
836 follows {x ∈ a | p} = ∅ by empty.def given ¬p;
837 follows {x ∈ b | ¬p} = b given ¬p;
838 follows ∅ ∪ b = b by empty.union;
839 done logically
840qed
842theorem if.swap [p : sentence] [a b : term] :
843 |- if p then a else b = if ¬p then b else a
844proof
845 cases:
846 | p then
847 follows if p then a else b = a by if.true [p] [a] [b];
848 follows ¬¬p logically; -- TODO: use vampire for this.
849 follows if ¬p then b else a = a by if.false [¬p] [b] [a];
850 done logically
851 | ¬p then
852 follows if p then a else b = b by if.false [p] [a] [b];
853 follows if ¬p then b else a = b by if.true [¬p] [b] [a];
854 done logically
855qed
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}, {a, b}} | ⋃{{a}, {a, b}} ≠ ⋂{{a}, {a, b}} → x ∉ ⋂{{a}, {a, b}}} = b;
82 -- thus ∀x, x ∈ ⋃{{a}, {a, b}} ↔ (x ∈ {a} ∨ x ∈ {a, b}) by union.def [{a}] [{a, b}];
83 -- follows ∀x, x ∈ ⋂{{a}, {a, b}} ↔ (x ∈ {a} ∧ x ∈ {a, b}) by inter.def [{a}] [{a, b}];
84 -- follows ∀x, (x ∈ {a} ∧ x ∈ {a, b}) ↔ (x = a ∧ x ∈ {a, b}) by singleton.def;
85 -- follows ∀x, (x = a ∧ x ∈ {a, b}) ↔ (x = a ∧ (x = a ∨ x = b)) by pair.def;
86 -- hence ∀x, x ∈ ⋂{{a}, {a, b}} ↔ x = a by opair.inter;
87 -- thus ∀x, x = a ↔ x ∈ {a} by singleton.def;
88 -- follows ⋂{{a}, {a, b}} = {a} by zfc.extensionality;
89 -- hence ⋃⟨a, b⟩ = {a, b} by opair.union;
90 -- hence ⋃{x ∈ {a, b} | {a, b} ≠ {a} → x ∉ {a}} = ⋃{x ∈ ⋃{{a}, {a, b}} | ⋃{{a}, {a, b}} ≠ ⋂{{a}, {a, b}} → x ∉ ⋂{{a}, {a, b}}} logically;
91 -- thus ∀x, x ∈ {a, b} ↔ (x = a ∨ x = b) by pair.def;
92 -- hence ∀x, x ∈ {a} ↔ x = a by singleton.def;
93 -- follows {a, b} ≠ {a} ↔ a ≠ b logically;
94 -- hence ∀x, ((x = a ∨ x = b) ∧ (a ≠ b → x ∉ {a})) ↔ (x = b) logically;
95 -- thus ∀x, x ∈ {x ∈ {a, b} | {a, b} ≠ {a} → x ∉ {a}} ↔ x = b by zfc.extensionality;
96 -- hence ∀x, x = b ↔ x ∈ {b} by singleton.def;
97 -- follows ∀x, x ∈ {x ∈ {a, b} | {a, b} ≠ {a} → x ∉ {a}} ↔ x ∈ {b} logically;
98 -- follows {x ∈ {a, b} | {a, b} ≠ {a} → x ∉ {a}} = {b} by zfc.extensionality;
99 -- hence ⋃{x ∈ {a, b} | {a, b} ≠ {a} → x ∉ {a}} = ⋃{b} logically;
100 -- hence ⋃{x ∈ ⋃{{a}, {a, b}} | ⋃{{a}, {a, b}} ≠ ⋂{{a}, {a, b}} → x ∉ ⋂{{a}, {a, b}}} = ⋃{b} logically;
101 -- thus ∀x, x ∈ ⋃{b} ↔ (∃y, x ∈ y ∧ y ∈ {b}) by big_union.def;
102 -- hence ∀x, (∃y, x ∈ y ∧ y ∈ {b}) ↔ x ∈ b logically;
103 -- follows ∀x, x ∈ ⋃{b} ↔ x ∈ b logically;
104 -- thus ⋃{b} = b by zfc.extensionality;
105 -- done logically
106 todo
107qed
Finally, we show that two ordered pairs are equal iff their first and second elements are equal.
111theorem opair.eq [a b c d : term] :
112 |- ⟨a, b⟩ = ⟨c, d⟩ ↔ (a = c ∧ b = d)
113proof
114 hence ⟨a, b⟩ = ⟨c, d⟩ → π₁(⟨a, b⟩) = π₁(⟨c, d⟩) by zfc.extensionality;
115 follows π₁(⟨a, b⟩) = π₁(⟨c, d⟩) ↔ a = c by opair_first.def;
116 follows ⟨a, b⟩ = ⟨c, d⟩ → π₂(⟨a, b⟩) = π₂(⟨c, d⟩) by zfc.extensionality;
117 follows π₂(⟨a, b⟩) = π₂(⟨c, d⟩) ↔ b = d by opair_second.def;
118 -- suffices ⟨a, b⟩ = ⟨c, d⟩ ↔ (a = c ∧ b = d);
119 hence ⟨a, b⟩ = ⟨c, d⟩ → (a = c ∧ b = d) logically;
120 hence (a = c ∧ b = d) → ⟨a, b⟩ = ⟨c, d⟩ logically;
121 done logically
122qed
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.
131notation product
132 term (350) ::= term " × " term
133end
135definition
136 A × B := {x ∈ 𝒫(𝒫(A ∪ B)) | ∃a ∈ A, ∃b ∈ B, x = ⟨a, b⟩}
137end
The difficult task is to prove that this gives us every possible ordered pair.
141theorem cart_prod.def [A B : term] :
142 |- ∀x, x ∈ A × B ↔ ∃a ∈ A, ∃b ∈ B, x = ⟨a, b⟩
143proof
144 arbitrary x;
145
146 -- remember the definition of A × B. (specifically have Vampire remember it)
147 follows A × B = {x ∈ 𝒫(𝒫(A ∪ B)) | ∃a ∈ A, ∃b ∈ B, x = ⟨a, b⟩}
148 by eq.refl [A × B];
149
150 -- the forward direction is pretty simple. it just comes directly from the
151 -- definition of restricted comprehension.
152 assume x ∈ A × B then ∃a ∈ A, ∃b ∈ B, x = ⟨a, b⟩ logically;
153
154 -- the other direction is harder. it follows quickly that x satisfies the
155 -- comprehension condition, but it is a little more work to show it is in
156 -- the double powerset.
157 assume ∃a ∈ A, ∃b ∈ B, x = ⟨a, b⟩ then x ∈ A × B as
158 obtain a st a ∈ A and b st b ∈ B ∧ x = ⟨a, b⟩ logically;
159 follows x = {{a}, {a, b}} by_def x = ⟨a, b⟩;
160
161 -- we already have that x is a pair so we just need to prove it is in the powerset
162 suffices x ∈ 𝒫(𝒫(A ∪ B)) ∧ (∃a ∈ A, ∃b ∈ B, x = ⟨a, b⟩) logically;
163 suffices x ∈ 𝒫(𝒫(A ∪ B)) given x = ⟨a, b⟩;
164
165 follows a ∈ A ∪ B ∧ b ∈ A ∪ B by union.def given a ∈ A and b ∈ B;
166 thus {a} ∈ 𝒫(A ∪ B) by powset.singleton_in;
167 thus {a, b} ∈ 𝒫(A ∪ B) by powset.pair_in;
168 thus {{a}, {a, b}} ∈ 𝒫(𝒫(A ∪ B)) by powset.pair_in;
169 thus x ∈ 𝒫(𝒫(A ∪ B)) given x = {{a}, {a, b}};
170 ;
171
172 done logically
173qed
Next, we prove a useful result relating the cartesian product of sets to their subsets.
177lemma cart_prod.sub [A B C D : term] : (A ⊆ C) (B ⊆ D)
178 |- A × B ⊆ C × D
179proof
180 suffices ∀x ∈ A × B, x ∈ C × D;
181 arbitrary x;
182 assume x ∈ A × B then x ∈ C × D as
183 obtain a st a ∈ A and b st b ∈ B ∧ x = ⟨a, b⟩ by cart_prod.def;
184 follows a ∈ C by sub.def given A ⊆ C;
185 follows b ∈ D by sub.def given B ⊆ D;
186 done by cart_prod.def
187 ;
188 done logically
189qed
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 .
197notation term.with_term_term
198 term (1000) ::= @name "(" term ", " term ")"
199end
201definition
202 Rel(A, B) := 𝒫(A × B)
203end
205theorem rel_on.def [A B : term] :
206 |- ∀R, R ∈ Rel(A, B) ↔ R ⊆ A × B
207proof
208 follows Rel(A, B) = 𝒫(A × B) by eq.refl [Rel(A, B)];
209 done by powset.def
210qed
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.
216definition
217 dom(R) := {π₁(x) | x ∈ R}
218end
220definition
221 ran(R) := {π₂(x) | x ∈ R}
222end
We can prove the following using the set map definition.
226theorem dom.def [R : term] :
227 |- ∀x, x ∈ dom(R) ↔ ∃y ∈ R, x = π₁(y)
228proof
229 suffices ∀x, x ∈ {π₁(z) | z ∈ R} ↔ ∃y ∈ R, x = π₁(y);
230 thus ∀x, x ∈ {π₁(z) | z ∈ R} ↔ (∃z, z ∈ R ∧ x = π₁(z)) by set_map.def [π₁(_)] [R];
231 done logically
232qed
234theorem ran.def [R : term] :
235 |- ∀x, x ∈ ran(R) ↔ ∃y ∈ R, x = π₂(y)
236proof
237 suffices ∀x, x ∈ {π₂(z) | z ∈ R} ↔ ∃y ∈ R, x = π₂(y);
238 thus ∀x, x ∈ {π₂(z) | z ∈ R} ↔ (∃z, z ∈ R ∧ x = π₂(z)) by set_map.def [π₂(_)] [R];
239 done logically
240qed
We can also have the notion of being a relation without having to know the exact domain and range.
245notation postfix_pred
246 sentence ::= term " : " @name
247end
249definition
250 R : Rel := R ∈ Rel(dom(R), ran(R))
251end
253theorem rel.def [R : term] :
254 |- R : Rel ↔ R ∈ Rel(dom(R), ran(R))
255proof
256 done by iff.refl [R : Rel]
257qed
The following result can be proved using the different relation definitions as well as the definition of the domain and range.
261theorem rel.is_rel_on [R : term] :
262 |- R : Rel ↔ ∃A, ∃B, R ∈ Rel(A, B)
263proof
264 -- (→)
265 assume R : Rel then ∃A, ∃B, R ∈ Rel(A, B) as
266 follows R ∈ Rel(dom(R), ran(R)) by rel.def;
267 done logically;
268 -- (←)
269 assume ∃A, ∃B, R ∈ Rel(A, B) then R : Rel as
270 -- We can fix A and B with our assumption
271 obtain A st ∃B, R ∈ Rel(A, B) logically;
272 obtain B st R ∈ Rel(A, B) logically;
273 follows R ⊆ A × B by rel_on.def;
274 suffices R ∈ Rel(dom(R), ran(R)) by rel.def;
275 suffices R ⊆ dom(R) × ran(R) by rel_on.def;
276 suffices ∀x, x ∈ R → x ∈ dom(R) × ran(R) by sub.def;
277 arbitrary x;
278 assume x ∈ R then x ∈ dom(R) × ran(R) as
279 follows ∀y, y ∈ R → y ∈ A × B by sub.def given R ⊆ A × B;
280 follows x ∈ A × B logically;
281 -- 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
282 obtain a st a ∈ A and b st b ∈ B ∧ x = ⟨a, b⟩ by cart_prod.def;
283 -- TODO: This (2 next lines) should not be something we have to prove
284 follows π₁(x) = a by opair_first.def given x = ⟨a, b⟩;
285 follows π₂(x) = b by opair_second.def given x = ⟨a, b⟩;
286 -- The first and second coordinates of x are by definition in the domain and range of R
287 thus π₁(x) ∈ dom(R) by dom.def given x ∈ R;
288 thus π₂(x) ∈ ran(R) by ran.def given x ∈ R;
289 done by cart_prod.def;
290 ;
291 done logically
292qed
We can show this fact in a similar manner to the previous proof, additionally making use of our cartesian product subset lemma.
295theorem rel_on.is_rel [R A B : term] :
296 |- R ∈ Rel(A, B) ↔ (R : Rel ∧ dom(R) ⊆ A ∧ ran(R) ⊆ B)
297proof
298 -- If R is a relation, then its a relation between sets
299 follows R : Rel ↔ ∃C, ∃D, R ∈ Rel(C, D) by rel.is_rel_on;
300 suffices R ∈ Rel(A, B) ↔ ((∃C, ∃D, R ∈ Rel(C, D)) ∧ dom(R) ⊆ A ∧ ran(R) ⊆ B) logically;
301 -- (→)
302 assume R ∈ Rel(A, B) then ((∃C, ∃D, R ∈ Rel(C, D)) ∧ dom(R) ⊆ A ∧ ran(R) ⊆ B) as
303 -- Really we just have to show that dom(R) ⊆ A and ran(R) ⊆ B as the first proposition is the same as our assumption
304 hence R ⊆ A × B by rel_on.def;
305 hence ∃C, ∃D, R ⊆ C × D logically;
306 follows ∃C, ∃D, R ∈ Rel(C, D) by rel_on.def;
307 suffices dom(R) ⊆ A ∧ ran(R) ⊆ B logically;
308 suffices (∀x ∈ dom(R), x ∈ A) ∧ (∀y ∈ ran(R), y ∈ B) by sub.def;
309 suffices (∀x, x ∈ dom(R) → x ∈ A) ∧ (∀y, y ∈ ran(R) → y ∈ B) logically;
310 -- Similarly to the last proof, we want to show the statement holds for an arbitrary element
311 hence (∀x, x ∈ dom(R) → x ∈ A) as
312 arbitrary x;
313 assume x ∈ dom(R) then x ∈ A as
314 obtain z st z ∈ R ∧ x = π₁(z) by dom.def;
315 follows z ∈ A × B by sub.def given R ⊆ A × B;
316 obtain a st a ∈ A and b st b ∈ B ∧ z = ⟨a, b⟩ by cart_prod.def;
317 follows π₁(z) = a by opair_first.def given z = ⟨a, b⟩;
318 done logically
319 ;
320 done logically
321 ;
322 hence (∀y, y ∈ ran(R) → y ∈ B) as
323 arbitrary y;
324 assume y ∈ ran(R) then y ∈ B as
325 obtain z st z ∈ R ∧ y = π₂(z) by ran.def;
326 follows z ∈ A × B by sub.def given R ⊆ A × B;
327 obtain b st b ∈ B and a st a ∈ A ∧ z = ⟨a, b⟩ by cart_prod.def;
328 follows π₂(z) = b by opair_second.def given z = ⟨a, b⟩;
329 done logically
330 ;
331 done logically
332 ;
333 done logically
334 ;
335 -- (←)
336 assume ((∃C, ∃D, R ∈ Rel(C, D)) ∧ dom(R) ⊆ A ∧ ran(R) ⊆ B) then R ∈ Rel(A, B) as
337 hence R : Rel by rel.is_rel_on;
338 follows R ∈ Rel(dom(R), ran(R)) by rel.def;
339 thus R ⊆ dom(R) × ran(R) by rel_on.def;
340 -- TODO: is this lemma useful?
341 follows dom(R) × ran(R) ⊆ A × B by cart_prod.sub;
342 hence R ⊆ A × B by sub.def given R ⊆ dom(R) × ran(R);
343 done by rel_on.def
344 ;
345 done logically
346qed
A functional relation is a particular kind of binary relation where the first element of each ordered pair in the relation is unique.
351notation functional_relation
352 term ::= term " → " term
353end
355definition
356 A → B := {f ∈ Rel(A, B) | ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f}
357end
359theorem fn_on.def [A B : term] :
360 |- ∀f, f ∈ (A → B) ↔ f ∈ Rel(A, B) ∧ ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f
361proof
362 suffices ∀f, f ∈ {f ∈ Rel(A, B) | ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f} ↔ f ∈ Rel(A, B) ∧ ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f;
363 done by zfc.extensionality
364qed
And once again we can define the notion of being a function independent of the domain and range.
369definition
370 f : Fn := f ∈ (dom(f) → ran(f))
371end
373theorem fn.def [f : term] :
374 |- f : Fn ↔ f ∈ (dom(f) → ran(f))
375proof
376 done by iff.refl [f : Fn]
377qed
379lemma fn.in_rel [A B : term] :
380 |- (A → B) ⊆ Rel(A, B)
381proof
382 thus {f ∈ Rel(A, B) | ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f} ⊆ Rel(A, B)
383 by comp.sub [∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ _] [Rel(A, B)];
384qed
386theorem fn.is_fn_on [f : term] :
387 |- f : Fn ↔ ∃A, ∃B, f ∈ (A → B)
388proof
389 suffices f ∈ (dom(f) → ran(f)) ↔ ∃A, ∃B, f ∈ (A → B);
390 assume f ∈ (dom(f) → ran(f)) then ∃A, ∃B, f ∈ (A → B) logically;
391 assume ∃A, ∃B, f ∈ (A → B) then f ∈ (dom(f) → ran(f)) as
392 obtain A st ∃B, f ∈ (A → B) logically;
393 obtain B st f ∈ (A → B) logically;
394 hence f ∈ Rel(A, B) ∧ ∀a ∈ A, ∃!b, ⟨a, b⟩ ∈ f by fn_on.def;
395 follows f : Rel by rel.is_rel_on;
396 follows f ∈ Rel(dom(f), ran(f)) by rel.def;
397 follows dom(f) ⊆ A by rel_on.is_rel;
398 follows ∀a, a ∈ dom(f) → a ∈ A by sub.def given dom(f) ⊆ A;
399 hence ∀a ∈ dom(f), ∃!b, ⟨a, b⟩ ∈ f logically;
400 done by fn_on.def
401 ;
402 done logically
403qed
405theorem fn_on.is_fn [f A B : term] :
406 |- f ∈ (A → B) ↔ (f : Fn ∧ dom(f) = A ∧ ran(f) ⊆ B)
407proof
408 todo
409qed
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.
415notation function_application
416 term (1000) ::= term "(" term ")"
417end
419definition
420 f:term (a) := ℩b, ⟨a, b⟩ ∈ f
421end
423theorem fn_on.pairs [f A B : term] : (f ∈ (A → B))
424 |- f = {⟨a, f(a)⟩ | a ∈ A}
425proof
426 todo
427qed
429theorem fn.pairs [f : term] : (f : Fn)
430 |- f = {⟨x, f(x)⟩ | x ∈ dom(f)}
431proof
432 follows f ∈ (dom(f) → ran(f)) by fn.def;
433 done by fn_on.pairs [f] [dom(f)] [ran(f)]
434qed
437notation function_maps_to
438 term ::= x:@binding(term) " ∈ " term " ↦ " term(x)
439end
441definition
442 x ∈ X ↦ f(x) := {⟨x, f(x)⟩ | x ∈ X}
443end
445theorem fun_map.is.rel [A B : term] [f(_) : term(term)]: (∀x ∈ A, f(x) ∈ B)
446 |- x ∈ A ↦ f(x) ∈ (A → B)
447proof
448 suffices {⟨x, f(x)⟩ | x ∈ A} ∈ {f ∈ Rel(A, B) | ∀a, a ∈ A → (∃!b, ⟨a, b⟩ ∈ f)};
449 todo
450qed
TODO:
455grammar_category chain_list
457tactic tactic.chain
458 tactic ::= @kw"chain" term:@fragment(term) list:chain_list
459end
461tactic chain_list.one
462 chain_list ::= "=" term:@fragment(term) just:justification ";"
463end
464tactic chain_list.many
465 chain_list ::= "=" term:@fragment(term) just:justification ";" rest:chain_list
466end
469theorem fn.eq_on_dom.eq [f g : term] : (f : Fn) (g : Fn) (dom(f) = dom(g))
470 (∀x ∈ dom(f), f(x) = g(x))
471 |- f = g
472proof
473 -- chain f = {⟨x, f(x)⟩ | x ∈ dom(f)} by fn.pairs;
474 -- = {⟨x, g(x)⟩ | x ∈ dom(f)} given ∀x ∈ dom(f), f(x) = g(x);
475 -- = {⟨x, g(x)⟩ | x ∈ dom(g)} given dom(f) = dom(g);
476 -- = g by fn.pairs;
477 chain f = {⟨x, f(x)⟩ | x ∈ dom(f)} as todo;
478 = {⟨x, g(x)⟩ | x ∈ dom(f)} as todo;
479 = {⟨x, g(x)⟩ | x ∈ dom(g)} as todo;
480 = g as todo;
481qed
483notation fn_restriction
484 term ::= term " ↾ " term
485end
487definition
488 f ↾ A := {x ∈ f | π₁(x) ∈ A}
489end
491theorem fn.restriction.is [f X : term] : (f : Fn)
492 |- f ↾ X : Fn
493proof
494 todo
495qed
497theorem fn.restriction.pairs [f X : term] : (f : Fn)
498 |- f ↾ X = {⟨x, f(x)⟩ | x ∈ dom(f) ∩ X}
499proof
500 todo
501qed
503theorem fn.restriction.eq [f g X : term] : (f : Fn) (g : Fn) (dom(f) ∩ X = dom(g) ∩ X)
504 (∀x ∈ dom(f) ∩ X, f(x) = g(x))
505 |- f ↾ X = g ↾ X
506proof
507 -- chain f ↾ X
508 -- = {⟨x, f(x)⟩ | x ∈ dom(f) ∩ X} by fn.restriction.pairs;
509 -- = {⟨x, g(x)⟩ | x ∈ dom(f) ∩ X} given ∀x ∈ X, f(x) = g(x);
510 -- = {⟨x, g(x)⟩ | x ∈ dom(g) ∩ X} given dom(f) ∩ X = dom(g) ∩ X;
511 -- = g ↾ X by fn.restriction.pairs;
512 chain f ↾ X
513 = {⟨x, f(x)⟩ | x ∈ dom(f) ∩ X} as todo;
514 = {⟨x, g(x)⟩ | x ∈ dom(f) ∩ X} as todo;
515 = {⟨x, g(x)⟩ | x ∈ dom(g) ∩ X} as todo;
516 = g ↾ X as todo;
517qed
The Ordinals 3.4
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.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