alternative definition of naturals

Stream: maths

[Kevin Buzzard]

I remember Andrej Bauer pointing out to me that if one has a "cardinal of a set" definition of natural numbers, then statements like commutativity of addition need not be proved by induction, they can instead be proved by showing that A disjoint union B bijects with B disjoint union A.

So I was thinking of trying to implement this in Lean because I'm giving a talk about numbers at this conference and in particular I was wondering how to actually define nat in a different way to the "Peano" Lean definition. One can start by defining equiv and proving it's an equivalence relation on Type and then taking the quotient (this is cardinals). Now one can define addition and show it's well-defined commutative -- but one still hasn't defined the naturals. One now wants to define the naturals as the "finite cardinals" but is there a non-inductive definition? One can define succ on cardinals, and then define finite inductively, via "the cardinal of the empty type is finite; if the cardinal of X is finite then the cardinal of option X is finite" -- but that is essentially rewriting Peano's definition. One could define finite as "every injection from X to X is a bijection" but now I'm a bit worried about whether one can prove that these are precisely the finite cardinals without using tools such as "if there's an injection which isn't a bijection then there's an injection from nat into your type" which uses nat, which of course isn't allowed.

[Johan Commelin]

Can't you use Fintype mod equivalence?

[Kevin Buzzard]

Oh that's a good idea! I should check to see if there is any mention of nat in any discussions here, but I am optimistic...

[David Wärn]

I think you can make the definition "$\kappa$ is finite iff $\kappa < \kappa + 1$" non-circular. With this definition, you want an induction principle for finite cardinals, saying they are generated from $0$ by adding $1$. The idea is that any finite $\kappa$ is either $0$ or $\kappa' + 1$, in which case $\kappa' < \kappa$ is still finite. So you just need well-foundedness of cardinal $<$, which follows from the well-ordering principle.

[Kevin Buzzard]

where < means "injection but no bijection" I guess. Yes, this looks like it's worth a try as well!

[David Wärn]

Yes, you might want to be a bit more careful than usual with this definition since Cantor-Schöder-Bernstein sort of uses the naturals, but "injection but no bijection" should work.

[David Wärn]

The Fintype approach is certainly more natural, but it's not very different from Peano's definition. Basically a type is a fintype if it's empty or equivalent to a fintype plus one. Still the way you set up arithmetic becomes different.

[Scott Morrison]

You could pick out the naturals from the surreals. :-)

[David Wärn]

Yet another approach is

• use Peano naturals
• define fin n
• prove that if fin m bijects with fin n then m = n. The key lemma for this is that you can subtract 1: if option X bijects with option Y then X bijects with Y.
• define addition and multiplication by recursion
• show by induction that fin n + fin m bijects with fin (n+m), and fin n x fin m bijects with fin (n * m)
• deduce semiring axioms

[Kevin Buzzard]

Yeah, I wanted to try and avoid Peano naturals completely -- it's an exercise to see if I can do this. Scott I had somehow imagined that going via surreals would be cheating because "Peano's axioms are buried in there somewhere" but looking at the definition of pgame it only has one constructor so it "can't" be, right? This is great, I'm really glad I asked here, I might do this as well and I think that's basically written the talk for me :-)

[Scott Morrison]

I'm pretty sure no natural numbers are mentioned in setting up pgame, except to cast the natural numbers into pgame. It would actually be fun to have the very initial part of pgame defined without even the prelude. I think it is closer to the bare metal than anything else we have. :-)

[David Wärn]

Don't you need some induction to prove the ring axioms, like with Peano naturals?

[Scott Morrison]

Sure there's lots of induction when setting up pgame and surreal. But none of it is induction on natural numbers, it's all just some-other-inductive-type-induction.

[Scott Morrison]

It is definitely much more complicated in every way that setting up the Peano naturals!

[Kevin Buzzard]

@Johan Commelin I don't like this Fintype idea any more. Fintype, and set finite, use fintype, which uses finset which uses multiset which uses list, and list is cheating because the definition of list unit is the same as the definition of nat so it's not allowed.

[Patrick Massot]

That's sneaky

[Adam Topaz]

Fintype is "just" the category of compact objects of Type*

[Adam Topaz]

No nat involved

[Johan Commelin]

@Kevin Buzzard fair enough, I give up (-;

[Kevin Buzzard]

Adam Topaz said:

Fintype is "just" the category of compact objects of Type*

Can I define compact without mentioning "finite subcover"?

[Johan Commelin]

Well, you can define Fintype as those types for which every injection is a bijection, right?

[Kevin Buzzard]

This is David's claim above but I've not checked it yet.

[Adam Topaz]

Compact in the categorical sense

[Johan Commelin]

@Adam Topaz that mentions finite somewhere, right?

[Adam Topaz]

https://ncatlab.org/nlab/show/compact+object

[Adam Topaz]

Nope, just need the notion of a filtered colimit

[Johan Commelin]

But usually you define filtered category in terms of finite diagrams right? Or do you want $\kappa$-filtered colimites for $\kappa =$ Type?

[Adam Topaz]

docs#category_theory.is_filtered

[Adam Topaz]

You need to know what a "pair" of things is.

[Adam Topaz]

If you want to use topological compactness, then you can use the ultrafilter characterization to avoid speaking about finite subcovers

[Adam Topaz]

So a set is finite if and only if every ultrafilter is principal

[Adam Topaz]

But this is more-or-less the same argument since the ultrafilter monad is a Kan extension of the inclusion of fintype to type

[Patrick Massot]

When I was a kid I was taught that a set is infinite if it is in bijection with the disjoint union of itself and one extra element (without discussing why this extra element exists), and it is finite otherwise.

[Adam Topaz]

TBH I don't remember the definition of "finite" I was taught in school...

[Johan Commelin]

You probably went to school outside France...

[Adam Topaz]

Indeed :pensive:

[Patrick Massot]

TBH this was during my first undergrad year.

[Mario Carneiro]

Metamath has a delightful section on Eight inequivalent definitions of finite set which are all equivalent in the presence of the axiom of choice (real AC, not LEM). The one we are all familiar with is Fin-I, that is, the numbers inductively generated from zero and successor. The fintype-mod-equivalence definition is also Fin-I. Another one that some may be familiar with is Fin-IV, also known as dedekind-finite. A set is dedekind-finite if it is not in bijection with a proper subset of itself. (The definitions mentioned by Patrick Massot and David Wärn's $\kappa<\kappa+1$ are using Fin-IV.) Other definitions include:

• Fin-V: A + A ≃ A fails (discounting 0)
• Fin-VI: A × A ≃ A fails (discounting 0 and 1)
• Fin-II: Every nonempty chain of subsets contains a maximum element

[Mario Carneiro]

The main source is A. Lévy, The independence of various definitions of finiteness

[Mario Carneiro]

Regarding carving out a subset of pgame, that depends on exactly how you pick the subset. pgame is basically equivalent to the set of ordinal numbers, so there is well ordering but no finiteness embedded in the definition. You can find all 8 of the Fins in there except for Fin-VII, whose definition is basically "non-well-ordered or Fin-I" which is kind of a cop-out definition. (The equivalence of Fin-VII and Fin-I is equivalent to the axiom of choice.)

[Bhavik Mehta]

There's also the definitions on nlab: https://ncatlab.org/nlab/show/finite+set which are again equivalent with AC plus definitions without naturals and apparently one in terms of schemes(!)