# 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 $\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 (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 $\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: Jun 17 2021 at 17:28 UTC