Sounds like a basic exercise when learning Lean. What is 1? What is +? Those are things you need to define in order to ask what 1 + 1 is.
In short, you define 0 to be a natural number, with no further underlying structure. “What is 0?” has no other answer than “it’s a natural number”; that is all you can and need to assume.
Next, you have a function I’ll call S that you can apply to a natural number, and just assume that S is injective and there is no n such that S(n) = 0. Together, they imply that S(0) ≠ 0, and neither 0 nor S(0) equal S(S(0)), etc. For notational convenience, we use special symbols to represent distinct values defined by repeated application of S: S(0) = 1, S(S(0)) = 2, etc
Finally, we define n + 0 = 0 for all n, and n + S(m) = S(n + m) for all n and m. Now we are ready to ask Lean what 1 + 1 is.
1
u/Temporary_Pie2733 1d ago
Sounds like a basic exercise when learning Lean. What is 1? What is +? Those are things you need to define in order to ask what 1 + 1 is.
In short, you define 0 to be a natural number, with no further underlying structure. “What is 0?” has no other answer than “it’s a natural number”; that is all you can and need to assume.
Next, you have a function I’ll call S that you can apply to a natural number, and just assume that S is injective and there is no n such that S(n) = 0. Together, they imply that S(0) ≠ 0, and neither 0 nor S(0) equal S(S(0)), etc. For notational convenience, we use special symbols to represent distinct values defined by repeated application of S: S(0) = 1, S(S(0)) = 2, etc
Finally, we define n + 0 = 0 for all n, and n + S(m) = S(n + m) for all n and m. Now we are ready to ask Lean what 1 + 1 is.
1 + 1 = 1 + S(0) = S(1 + 0) = S(1) = 2