Zulip Chat Archive

Stream: maths

Topic: alternative definition of naturals


view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 06 2021 at 09:13):

Can't you use Fintype mod equivalence?

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (May 06 2021 at 10:11):

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

view this post on Zulip 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

view this post on Zulip 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 :-)

view this post on Zulip 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. :-)

view this post on Zulip David Wärn (May 06 2021 at 10:48):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (May 06 2021 at 10:50):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 06 2021 at 16:29):

That's sneaky

view this post on Zulip Adam Topaz (May 06 2021 at 16:30):

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

view this post on Zulip Adam Topaz (May 06 2021 at 16:31):

No nat involved

view this post on Zulip Johan Commelin (May 06 2021 at 16:32):

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

view this post on Zulip 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"?

view this post on Zulip Johan Commelin (May 06 2021 at 16:55):

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

view this post on Zulip Kevin Buzzard (May 06 2021 at 16:55):

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

view this post on Zulip Adam Topaz (May 06 2021 at 16:57):

Compact in the categorical sense

view this post on Zulip Johan Commelin (May 06 2021 at 16:58):

@Adam Topaz that mentions finite somewhere, right?

view this post on Zulip Adam Topaz (May 06 2021 at 16:58):

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

view this post on Zulip Adam Topaz (May 06 2021 at 16:58):

Nope, just need the notion of a filtered colimit

view this post on Zulip 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?

view this post on Zulip Adam Topaz (May 06 2021 at 17:03):

docs#category_theory.is_filtered

view this post on Zulip Adam Topaz (May 06 2021 at 17:04):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (May 06 2021 at 17:05):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (May 06 2021 at 17:08):

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

view this post on Zulip Johan Commelin (May 06 2021 at 17:09):

You probably went to school outside France...

view this post on Zulip Adam Topaz (May 06 2021 at 17:11):

Indeed :pensive:

view this post on Zulip Patrick Massot (May 06 2021 at 17:13):

TBH this was during my first undergrad year.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 07 2021 at 00:23):

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

view this post on Zulip 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.)

view this post on Zulip 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: Jun 17 2021 at 17:28 UTC