waffle edits in tutorial world intro + 1-4
This commit is contained in:
Kevin Buzzard
@@ -24,17 +24,15 @@ Introduction
|
||||
|
||||
In this game, we will build the basic theory of the natural
|
||||
numbers `{0,1,2,3,4,...}` from scratch. Our first goal is to prove
|
||||
that `2 + 2 = 4`. After that we'll prove that `x + y = y + x`.
|
||||
that `2 + 2 = 4`. Next we'll prove that `x + y = y + x`.
|
||||
And at the end we'll see if we can prove Fermat's Last Theorem.
|
||||
**TODO** link to github repo if I get funded
|
||||
We'll do this by solving levels of a computer puzzle game called `Lean`.
|
||||
|
||||
To learn more about these puzzles, click on \"Tutorial World\".
|
||||
(**TODO** ensure they can't click on level 1 directly)
|
||||
|
||||
## More
|
||||
|
||||
Open the \"Game Info\" in the burger menu on the top right for resources,
|
||||
Open \"Game Info\" in the burger menu on the top right for resources,
|
||||
links, and ways to interact with the Lean community.
|
||||
"
|
||||
|
||||
|
||||
@@ -1,5 +1,3 @@
|
||||
/- **TODO** need that brief apache2 and author string?
|
||||
-/
|
||||
import Game.Levels.Tutorial.L01rfl
|
||||
import Game.Levels.Tutorial.L02rw
|
||||
import Game.Levels.Tutorial.L03three_eq_sss0
|
||||
@@ -13,8 +11,8 @@ import Game.Levels.Tutorial.L07twoaddtwo
|
||||
|
||||
This file defines Tutorial World. Like all worlds, this world
|
||||
has a name, a title, an introduction, and most importantly
|
||||
a finite set of levels (imported above). Each level has an
|
||||
associated level number defined in it, and that's what determines
|
||||
a finite set of levels (imported above). Each level has a
|
||||
level number defined within it, and that's what determines
|
||||
the order of the levels.
|
||||
-/
|
||||
World "Tutorial"
|
||||
@@ -24,7 +22,7 @@ Introduction
|
||||
"In Tutorial World, you're going to learn how to prove theorems about numbers.
|
||||
The boss level of this world is to prove that `2 + 2 = 4`.
|
||||
|
||||
You prove theorems like this using tools called *tactics*. Each
|
||||
You prove theorems by solving puzzles using tools called *tactics*. Each
|
||||
tactic performs a certain logical idea, and the puzzle is to
|
||||
prove the theorem by applying the tactics in the right order.
|
||||
|
||||
|
||||
@@ -8,17 +8,16 @@ Title "The rfl tactic"
|
||||
|
||||
DefinitionDoc MyNat as "ℕ"
|
||||
"
|
||||
The natural numbers, defined as an inductive type, with two constructors:
|
||||
`ℕ` is the natural numbers, defined as an inductive type, with two constructors:
|
||||
|
||||
* `0 : ℕ`
|
||||
* `succ (n : ℕ) : ℕ`
|
||||
|
||||
## Game Implementation
|
||||
|
||||
*The game uses its own copy of the natural numbers, called `MyNat` or `ℕ`.
|
||||
If you ever see `Nat`, then you probably need to use `(1 : ℕ)` instead of `1` somewhere to tell Lean
|
||||
to work in `MyNat`.*
|
||||
"
|
||||
*The game uses its own copy of the natural numbers, called `MyNat` with notation `ℕ`.
|
||||
It is distinct from the Lean natural numbers `Nat`, which should hopefully
|
||||
never leak into the natural number game.*"
|
||||
|
||||
NewDefinition MyNat
|
||||
|
||||
@@ -94,5 +93,5 @@ Congratulations! You completed your first verified proof!
|
||||
Remember that `rfl` is a *tactic*. If you ever want information about the `rfl` tactic,
|
||||
just click on `rfl` in the list of tactics on the right.
|
||||
|
||||
Now click on \"Next\" to continue the journey.
|
||||
Now click on \"Next\" to learn about the `rw` tactic.
|
||||
"
|
||||
|
||||
@@ -18,13 +18,14 @@ and `h` is a secret *proof* of that proposition, in the same kind of
|
||||
way that `x` and `y` are secret numbers.
|
||||
|
||||
Before we can use `rfl`, we have to \"sub in for $y$\".
|
||||
We do this in Lean by *rewriting* with the hypothesis `h`.
|
||||
We do this in Lean by *rewriting* the hypothesis `h`,
|
||||
using the `rw` tactic.
|
||||
"
|
||||
|
||||
/-- If $x$ and $y$ are natural numbers, and $y = x + 7$, then $2y = 2(x + 7)$. -/
|
||||
Statement
|
||||
(x y : ℕ) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by
|
||||
Hint "You can use `rw [h]` to replace the `y` with `x + 7`."
|
||||
Hint "You can execute `rw [h]` to replace the `y` with `x + 7`."
|
||||
rw [h]
|
||||
Hint "Now `rfl` will work."
|
||||
rfl
|
||||
@@ -37,84 +38,69 @@ all `X`s in the goal to `Y`s.
|
||||
|
||||
## Variants
|
||||
|
||||
`rw [←h]` (changes `Y` to `X`)
|
||||
`rw [←h]` (changes `Y` to `X`, get the back arrow by typing `\\left ` or `\\l `.)
|
||||
`rw [h1, h2]` (a sequence of rewrites)
|
||||
`rw [h] at h2` (changes `X` to `Y` in hypothesis `h2`)
|
||||
`rw [h] at h1 h2 ⊢ (rewrite at two hypotheses and the goal)
|
||||
`rw [h] at h2` (changes `X`s to `Y`s in hypothesis `h2`)
|
||||
`rw [h] at h1 h2 ⊢ (rewrites at two hypotheses and the goal)
|
||||
|
||||
## Details
|
||||
|
||||
The `rw` tactic is a way to do \"substituting in\". There
|
||||
are two distinct situations where you can use this tactic.
|
||||
|
||||
1) Basic usage: if `h : A = B` is an assumption,
|
||||
and if the goal contains one or more `A`s, then `rw h`
|
||||
1) Basic usage: if `h : A = B` is an assumption or
|
||||
the proof of a theorem, and if the goal contains one or more `A`s, then `rw [h]`
|
||||
will change them all to `B`'s. The tactic will error
|
||||
if there are no `A`s in the goal.
|
||||
|
||||
2) Advanced usage: Assumptions coming from *theorems*
|
||||
2) Advanced usage: Assumptions coming from theorems
|
||||
often have missing pieces. For example `add_zero`
|
||||
is a proof that `? + 0 = ?` because `add_zero` really a function,
|
||||
is a proof that `? + 0 = ?` because `add_zero` really is a function,
|
||||
and we didn't give it enough inputs yet.
|
||||
In this situation `rw` will look through the term
|
||||
for any subterm of the form `x + 0` and the moment it
|
||||
In this situation `rw` will look through the goal
|
||||
for any subterm of the form `x + 0`, and the moment it
|
||||
finds one it fixes `?` to be `x` then changes all `x + 0`s to `x`s.
|
||||
|
||||
Exercise: think about why `rw [add_zero]` changes the term
|
||||
`(0 + 0) + (x + 0) + (0 + 0) + (x + 0)` to
|
||||
`0 + (x + 0) + 0 + (x + 0)`
|
||||
|
||||
**** UP TO HERE *****
|
||||
|
||||
. The `rw` tactic will also work with proofs of theorems
|
||||
which are equalities (look for them in the drop down
|
||||
menu on the left, within Theorem Statements).
|
||||
For example, in world 1 level 4
|
||||
we learn about `add_zero x : x + 0 = x`, and `rw add_zero`
|
||||
will change `x + 0` into `x` in your goal (or fail with
|
||||
an error if Lean cannot find `x + 0` in the goal).
|
||||
If you can't remember the name of an equality lemma, look it up in
|
||||
the list of lemmas on the right.
|
||||
|
||||
Important note: if `h` is not a proof of the form `A = B`
|
||||
or `A ↔ B` (for example if `h` is a function, an implication,
|
||||
or perhaps even a proposition itself rather than its proof),
|
||||
then `rw` is not the tactic you want to use. For example,
|
||||
`rw (P = Q)` is never correct: `P = Q` is the true-false
|
||||
statement itself, not the proof.
|
||||
If `h : P = Q` is its proof, then `rw h` will work.
|
||||
`rw (P = Q)` is never correct: `P = Q` is the theorem *statement*,
|
||||
not the proof. If `h : P = Q` is the proof, then `rw [h]` will work.
|
||||
|
||||
Pro tip 1: If `h : A = B` and you want to change
|
||||
`B`s to `A`s instead, try `rw ←h` (get the arrow with `\\l` and
|
||||
note that this is a small letter L, not a number 1).
|
||||
|
||||
### Example:
|
||||
If it looks like this in the top right hand box:
|
||||
If you have the assumption `h : x = y + y` and your goal is
|
||||
```
|
||||
x y : mynat
|
||||
h : x = y + y
|
||||
⊢ succ (x + 0) = succ (y + y)
|
||||
succ (x + 0) = succ (y + y)
|
||||
```
|
||||
|
||||
then
|
||||
|
||||
`rw add_zero,`
|
||||
`rw [add_zero]`
|
||||
|
||||
will change the goal into `⊢ succ x = succ (y + y)`, and then
|
||||
will change the goal into `succ x = succ (y + y)`, and then
|
||||
|
||||
`rw h,`
|
||||
`rw [h]`
|
||||
|
||||
will change the goal into `⊢ succ (y + y) = succ (y + y)`, which
|
||||
can be solved with `refl,`.
|
||||
will change the goal into `succ (y + y) = succ (y + y)`, which
|
||||
can be solved with `rfl,`.
|
||||
|
||||
### Example:
|
||||
You can use `rw` to change a hypothesis as well.
|
||||
For example, if your local context looks like this:
|
||||
For example, if you have two hypotheses
|
||||
```
|
||||
x y : mynat
|
||||
h1 : x = y + 3
|
||||
h2 : 2 * y = x
|
||||
⊢ y = 3
|
||||
```
|
||||
then `rw h1 at h2` will turn `h2` into `h2 : 2 * y = y + 3`.
|
||||
then `rw [h1] at h2` will turn `h2` into `h2 : 2 * y = y + 3`.
|
||||
-/
|
||||
"
|
||||
|
||||
@@ -122,7 +108,7 @@ NewTactic rw
|
||||
|
||||
Conclusion
|
||||
"
|
||||
If you want to inspect the proof you created, toggle \"Editor mode\" by clicking
|
||||
If you want to inspect the proof you just created, toggle \"Editor mode\" by clicking
|
||||
on the `</>` button in the top right. In editor mode,
|
||||
you can click around the proof and see the state of Lean's brain at any point.
|
||||
If you want to go back to interactive mode with hints, click the button again.
|
||||
|
||||
@@ -10,34 +10,34 @@ namespace MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
The goals of the previous levels in the tutorial mentioned things like addition and
|
||||
multiplication of numbers. But now we start the game itself: building
|
||||
numbers from scratch. Our definition of (natural) numbers is based on
|
||||
Giuseppe Peano's, and consists of three axioms:
|
||||
|
||||
# The birth of number.
|
||||
|
||||
Now you know some tactics, let's begin the game. We were talking
|
||||
about numbers in the previous levels, but now let's go back to basics.
|
||||
What are numbers? Numbers in Lean can be defined by three axioms, an
|
||||
idea going back to Giuseppe Peano. Here are the first two of them.
|
||||
|
||||
* `0` is a number.
|
||||
* If `n` is a number, then the *successor* `succ n` of `n` (that is, the number after `n`) is a number.
|
||||
* That's it.
|
||||
* If `n` is a number, then the *successor* `succ n` of `n` (that is, the number after `n`)
|
||||
is a number.
|
||||
|
||||
The final boss of this world is `2 + 2 = 4`. If you can prove this theorem,
|
||||
you've mastered the basics. Our problem right now is that we cannot even *state*
|
||||
the theorem because we haven't yet defined `2` or `+` or `4`. Let's worry about `+`
|
||||
later; before we learn to add we learn to count, so let's count to four.
|
||||
What numbers can we make in this system? Let's figure out how to count,
|
||||
and name a few small numbers.
|
||||
|
||||
# Counting to four.
|
||||
|
||||
What kind of numbers can we make from Peano's axioms? Well, Peano gives us the number `0` for free,
|
||||
but the only other thing we have is this successor function, which eats a number and
|
||||
spits out the number after it. So we could *define* `1` to be `succ 0` (Note that Lean
|
||||
does not *need* brackets for function inputs, although you can use them if you want after the space).
|
||||
The first axiom gives us the number `0` for free. The other gives us
|
||||
the successor function `succ`. If we apply this function to `0`
|
||||
then we get a new number `succ 0`, the number after `0`. Let's
|
||||
call this new number `1`.
|
||||
|
||||
Let's define `2` to be `succ 1`, `3` to be `succ 2` and `4` to be `succ 3`.
|
||||
You can think of a statement like `3 = succ 2` as an axiom or hypothesis, and
|
||||
this game has a special name for this hypothesis, which is `three_eq_succ_two`. This should
|
||||
be the first theorem you rewrite with in the proof of the theorem below;
|
||||
the natural flow of the proof is to break down the larger more complex numbers
|
||||
into simpler ones, and ultimately down to a hugely inefficient \"normal form\"
|
||||
`succ (succ (succ (succ ... 0))..)
|
||||
We can define `2` to be `succ 1`, then set `3 = succ 2` and `4 = succ 3`.
|
||||
This gives us plenty of numbers to be getting along with.
|
||||
|
||||
You can think of a statement like `3 = succ 2` as an axiom or hypothesis or
|
||||
theorem, and this game has a special name for the proof of this theorem:
|
||||
it's called `three_eq_succ_two`.
|
||||
|
||||
Use the `rw` tactic to prove that 3 is the number after the number after the number after 0.
|
||||
|
||||
@@ -45,8 +45,8 @@ Use the `rw` tactic to prove that 3 is the number after the number after the num
|
||||
/-- $3=\operatorname{succ}\operatorname{succ}(\operatorname{succ}(0))$. -/
|
||||
Statement
|
||||
: 3 = succ (succ (succ 0)) := by
|
||||
Hint "Take a look at the names of the proofs in the `numerals` tab on the right.
|
||||
Start to think about how to guess the names of proofs automatically."
|
||||
Hint "Use the lemmas in the *numerals* section to break `3` down into
|
||||
basic pieces."
|
||||
rw [three_eq_succ_two]
|
||||
rw [two_eq_succ_one]
|
||||
rw [one_eq_succ_zero]
|
||||
@@ -56,17 +56,25 @@ LemmaDoc MyNat.one_eq_succ_zero as "one_eq_succ_zero" in "numerals"
|
||||
"`one_eq_succ_zero` is a proof of `1 = succ 0`."
|
||||
|
||||
LemmaDoc MyNat.two_eq_succ_one as "two_eq_succ_one" in "numerals"
|
||||
"`two_eq_succ_one is a proof of `2 = succ 1`."
|
||||
"`two_eq_succ_one` is a proof of `2 = succ 1`."
|
||||
|
||||
LemmaDoc MyNat.three_eq_succ_two as "three_eq_succ_two" in "numerals"
|
||||
"`three_eq_succ_two is a proof of `3 = succ 2`."
|
||||
"`three_eq_succ_two` is a proof of `3 = succ 2`."
|
||||
|
||||
LemmaDoc MyNat.four_eq_succ_three as "four_eq_succ_three" in "numerals"
|
||||
"`four_eq_succ_three is a proof of `4 = succ 3`."
|
||||
"`four_eq_succ_three` is a proof of `4 = succ 3`."
|
||||
|
||||
LemmaDoc MyNat.five_eq_succ_four as "five_eq_succ_four" in "numerals"
|
||||
"`five_eq_succ_four is a proof of `5 = succ 4`."
|
||||
"`five_eq_succ_four` is a proof of `5 = succ 4`."
|
||||
|
||||
-- **todo** do we need 5?
|
||||
|
||||
NewLemma MyNat.one_eq_succ_zero MyNat.two_eq_succ_one MyNat.three_eq_succ_two
|
||||
MyNat.four_eq_succ_three MyNat.five_eq_succ_four
|
||||
LemmaTab "numerals"
|
||||
|
||||
Conclusion
|
||||
"
|
||||
Why did we not just define `succ n` to be `n + 1`? Because we have not
|
||||
even *defined* addition yet! We'll do that in the next level.
|
||||
"
|
||||
|
||||
@@ -10,81 +10,108 @@ open MyNat
|
||||
|
||||
Introduction
|
||||
"
|
||||
We have defined all the numbers up to 4 (note that in this game, by \"number\"
|
||||
I *always* mean \"natural number\"), but we still cannot state
|
||||
the theorem that `2 + 2 = 4` because we have not yet defined addition.
|
||||
Let's now fix this.
|
||||
We have defined all the numbers up to 4, but we still cannot *state*
|
||||
the theorem that `2 + 2 = 4` because we haven't yet defined addition.
|
||||
Before we do this, we need to informally introduce the final axiom
|
||||
used in this game.
|
||||
|
||||
# \"There's only two ways to make numbers\"
|
||||
|
||||
Peano's third axiom, informally, says that `0` and `succ` are *the
|
||||
only ways to make numbers*. More precisely: if we want to do something
|
||||
for *every number*, then all we have to do is two things:
|
||||
|
||||
* Do it for `0`.
|
||||
|
||||
* Assuming we've done it for `n`, do it for `succ n`.
|
||||
|
||||
The axiom then guarantees that we've done it for all numbers.
|
||||
|
||||
# The definition of addition
|
||||
|
||||
Say `x` and `y` are numbers. How are we going to define `x + y`?
|
||||
This is where Peano's third axiom comes in. \"That's it\" means
|
||||
that if you want to define how to add `y` to something, you only have
|
||||
to say how to do it in the two ways that numbers can be born.
|
||||
More explicitly, you have to explain how to add zero to something, and how to add
|
||||
a successor to something. So let's start with adding zero.
|
||||
Let's try and define the function which adds `37` to a number, using
|
||||
this principle. We have to do two things.
|
||||
|
||||
We need to decide how to define `x + 0`. We want addition to agree with our intuition,
|
||||
so we should define `x + 0` to be `x`. Let's throw in a new axiom or hypothesis
|
||||
or proof or however you want to think about it, saying this:
|
||||
* We must define `37 + 0`.
|
||||
|
||||
* `add_zero (a : ℕ) : a + 0 = a`
|
||||
* If we already know what `37 + n` is, we must define `37 + succ n`.
|
||||
|
||||
In fact `add_zero` is a *family* of proofs. For example `add_zero 37` is a proof
|
||||
that `37 + 0 = 37`, and `add_zero (p * q)` is a proof that `p * q + 0 = p * q`.
|
||||
Mathematicians might encourage you to think of `add_zero` as just one proof:
|
||||
# Adding 0
|
||||
|
||||
* `add_zero : ∀ (a : ℕ), a + 0 = a`
|
||||
To make addition agree with our intuition, we should define `37 + 0`
|
||||
to be `37`. More generally, we should define `x + 0` to be `x` for
|
||||
any number `x`. The name of this hypothesis in Lean is `add_zero x`.
|
||||
|
||||
but here it is very helpful to invoke the principle coming from computer science
|
||||
(not always true, but true here) that a proof is the same as a function. Lean
|
||||
is a functional programming language and you should think of `add_zero` as a function
|
||||
which eats a number and spits out a proof.
|
||||
`add_zero 37 : 37 + 0 = 37`
|
||||
|
||||
`add_zero x : x + 0 = x`
|
||||
|
||||
You can think of `add_zero` as a function which eats a number, and spits
|
||||
out a proof about that number.
|
||||
"
|
||||
|
||||
namespace MyNat
|
||||
|
||||
/-- $a+(0+0)+(0+0+0)=a.$ -/
|
||||
Statement (a : ℕ) : (a + (0 + 0)) + (0 + 0 + 0) = a := by
|
||||
Hint "I will walk you through this level so I can show you some
|
||||
techniques which will speed up your proving.
|
||||
|
||||
This is an annoying goal. One of `rw [add_zero a]` and `rw [add_zero 0]`
|
||||
will work, but not the other. Can you figure out which? Try the one
|
||||
that works."
|
||||
Branch
|
||||
rw [add_zero 0]
|
||||
Hint "Walkthrough: Now `rw [add_zero a]` will work, so try that next."
|
||||
rw [add_zero a]
|
||||
Hint "OK this is getting old really quickly. And if we end up with more complex
|
||||
goals and have to type weird stuff like `rw [add_zero (a + 0)]` it will be
|
||||
even worse.
|
||||
|
||||
Fortunately `rw` can do smart rewriting. Go back to the very start
|
||||
of this proof by clicking \"Delete\" to remove all the moves you've
|
||||
made so far and then try `rw [add_zero]` few times. Then delete all of
|
||||
these and try `repeat rw [add_zero]`.
|
||||
"
|
||||
repeat rw [add_zero]
|
||||
Hint "`rw [add_zero]` will change `? + 0` into `?`
|
||||
where `?` is arbitrary; `rw` will use the
|
||||
first solution which matches for `?`."
|
||||
/-- $a+(b+0)+(c+0)=a+b+c.$ -/
|
||||
Statement (a b c : ℕ) : a + (b + 0) + (c + 0) = a + b + c := by
|
||||
Hint "`rw [add_zero b]` will change `b + 0` into `b`."
|
||||
repeat rw [add_zero b]
|
||||
Hint "`rw [add_zero]` will change `? + 0` into `?` for the first value of `?` which works."
|
||||
rw [add_zero]
|
||||
rfl
|
||||
|
||||
Conclusion "Those of you interested in speedrunning the game may want to know
|
||||
that `repeat rw [add_zero]` will do both rewrites at once."
|
||||
|
||||
|
||||
|
||||
DefinitionDoc Add as "+" "`Add a b`, with notation `a + b`, is
|
||||
the usual sum of natural numbers. Internally it is defined by
|
||||
recursion on b, with the two \"equation lemmas\" being
|
||||
|
||||
* `add_zero a : a + 0 = a`
|
||||
|
||||
* `add_succ a b : a + succ b = succ (a + b)
|
||||
|
||||
Other theorems about naturals, such as `zero_add a : 0 + a = a`, are proved
|
||||
by induction from these two basic theorems."
|
||||
|
||||
NewDefinition Add
|
||||
|
||||
LemmaTab "Add"
|
||||
|
||||
LemmaDoc MyNat.add_zero as "add_zero" in "Add"
|
||||
"`add_zero n` is a proof that `n + 0 = n`.
|
||||
|
||||
This is one of the two axioms for addition."
|
||||
You can think of `add_zero` as a function, which
|
||||
eats a number, and returns a proof of a theorem
|
||||
about that number. For example `add_zero 37` is
|
||||
a proof that `37 + 0 = 37`.
|
||||
|
||||
DefinitionDoc Add as "+" "`Add a b`, with notation `a + b`, is
|
||||
the usual sum of natural numbers. Internally it is defined by
|
||||
induction on one of the variables, but that is an implementation issue;
|
||||
All you need to know is that `add_zero` and `zero_add` are both theorems."
|
||||
A mathematician sometimes thinks of `add_zero`
|
||||
as \"one thing\", namely a proof of $\\forall n ∈ ℕ, n + 0 = n$$`."
|
||||
|
||||
NewLemma MyNat.add_zero
|
||||
|
||||
TacticDoc «repeat» "
|
||||
## Summary
|
||||
|
||||
`repeat t` repeatedly applies the tactic `t`
|
||||
to the goal.
|
||||
|
||||
## Example
|
||||
|
||||
`repeat rw [add_zero]` will turn the goal
|
||||
`⊢ a + 0 + (0 + (0 + 0)) = b + 0 + 0`
|
||||
into the goal
|
||||
`⊢ a = b`
|
||||
|
||||
## Variant
|
||||
|
||||
`repeat' t` applies `t` to all subgoals
|
||||
more reliably.
|
||||
"
|
||||
NewTactic «repeat» -- TODO: Do we want it to be unlocked here?
|
||||
NewDefinition Add
|
||||
LemmaTab "Add"
|
||||
|
||||
Conclusion
|
||||
"
|
||||
|
||||
27
Game/Levels/Tutorial/set_theory_rant_BLOG_THIS.txt
Normal file
27
Game/Levels/Tutorial/set_theory_rant_BLOG_THIS.txt
Normal file
@@ -0,0 +1,27 @@
|
||||
|
||||
A set theorist would object to the idea of `add_zero`
|
||||
being an actual *function*. But in Lean, a *theorem statement
|
||||
is a set too*, and the elements of the set are the proofs
|
||||
of the statement. In particular it's totally fine to have
|
||||
a function sending a number to a proof.
|
||||
|
||||
An *extremely pedantic* set theorist would object to the
|
||||
use of the word \"function\" because the target space appears
|
||||
to be the \"set of all proofs\" and it's a *theorem* that
|
||||
there is no set of all groups, so how do we know there is
|
||||
definitely a set of all proofs as formalised within ZFC set
|
||||
theory. And we say no of course we don't want to consider
|
||||
all proofs at once, the idea is that the input is a natural
|
||||
number `n` and the output is a proof that `n + 0 = n`.
|
||||
And the *extremely extremely pedantic* set theorist would
|
||||
then say that the target set, namely the theorem
|
||||
statement `n + 0 = n`, depends on the *input* from source set!
|
||||
A function from `X` to `Y` means that you have to say
|
||||
in advance what `Y` is, you can't let `Y` change according
|
||||
to the input! And so you tell this extremely extremely pedantic
|
||||
set theorist that technically you're right and it's
|
||||
actually a section of a fibre bundle `add_zero → ℕ`, or
|
||||
equivalently a function sending a natual number `n` to a proof
|
||||
of `n + 0 = n`, the fibre of `add_zero → ℕ` at `n`.
|
||||
|
||||
This is one of the two axioms for addition.
|
||||
Reference in New Issue
Block a user