Zulip Chat Archive

Stream: maths

Topic: alternative definition of naturals


Kevin Buzzard (May 06 2021 at 09:11):

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 (May 06 2021 at 09:13):

Can't you use Fintype mod equivalence?

Kevin Buzzard (May 06 2021 at 09:15):

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 (May 06 2021 at 09:56):

I think you can make the definition "κ\kappa is finite iff κ<κ+1\kappa < \kappa + 1" non-circular. With this definition, you want an induction principle for finite cardinals, saying they are generated from 00 by adding 11. The idea is that any finite κ\kappa is either 00 or κ+1\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 (May 06 2021 at 09:58):

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

David Wärn (May 06 2021 at 10:01):

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 (May 06 2021 at 10:01):

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 (May 06 2021 at 10:11):

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

David Wärn (May 06 2021 at 10:19):

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 (May 06 2021 at 10:44):

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 (May 06 2021 at 10:46):

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 (May 06 2021 at 10:48):

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

Scott Morrison (May 06 2021 at 10:49):

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 (May 06 2021 at 10:50):

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

Kevin Buzzard (May 06 2021 at 16:27):

@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 (May 06 2021 at 16:29):

That's sneaky

Adam Topaz (May 06 2021 at 16:30):

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

Adam Topaz (May 06 2021 at 16:31):

No nat involved

Johan Commelin (May 06 2021 at 16:32):

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

Kevin Buzzard (May 06 2021 at 16:52):

Adam Topaz said:

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

Can I define compact without mentioning "finite subcover"?

Johan Commelin (May 06 2021 at 16:55):

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

Kevin Buzzard (May 06 2021 at 16:55):

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

Adam Topaz (May 06 2021 at 16:57):

Compact in the categorical sense

Johan Commelin (May 06 2021 at 16:58):

@Adam Topaz that mentions finite somewhere, right?

Adam Topaz (May 06 2021 at 16:58):

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

Adam Topaz (May 06 2021 at 16:58):

Nope, just need the notion of a filtered colimit

Johan Commelin (May 06 2021 at 17:02):

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

Adam Topaz (May 06 2021 at 17:03):

docs#category_theory.is_filtered

Adam Topaz (May 06 2021 at 17:04):

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

Adam Topaz (May 06 2021 at 17:05):

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

Adam Topaz (May 06 2021 at 17:05):

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

Adam Topaz (May 06 2021 at 17:06):

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 (May 06 2021 at 17:07):

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 (May 06 2021 at 17:08):

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

Johan Commelin (May 06 2021 at 17:09):

You probably went to school outside France...

Adam Topaz (May 06 2021 at 17:11):

Indeed :pensive:

Patrick Massot (May 06 2021 at 17:13):

TBH this was during my first undergrad year.

Mario Carneiro (May 07 2021 at 00:18):

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 κ<κ+1\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 (May 07 2021 at 00:23):

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

Mario Carneiro (May 07 2021 at 00:40):

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 (May 07 2021 at 01:14):

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(!)


Last updated: Dec 20 2023 at 11:08 UTC