Expository source on Peano axioms for undergrads?

Stream: maths

[Jake Levinson]

Hi all, I'm teaching introductory abstract algebra this semester, and we briefly touch on the Peano axioms without covering them in great detail. I want to suggest a source to my students in case they're curious to see more. Does anyone have a favorite (accessible, expository) source on the Peano axioms and the construction/development of N, Z, Q, etc for undergrads?

[Jake Levinson]

(I realize this is not technically about Lean, but nobody I know in real life had a suggestion and it occurred to me that people here might!)

[Kevin Buzzard]

My wholly biased suggestion is of course https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ for the naturals

[Jake Levinson]

I was tempted to suggest just that :smile:

[Jake Levinson]

But I've seen you say that you think Lean is currently too hard to use for beginning undergrads (when simultaneously learning new math). Would you say the Natural Number Game is at an appropriate level since it hides a lot of the learning curve?

[Kevin Buzzard]

Oh absolutely! That's why I wrote it!

[Jake Levinson]

Well OK then. Excellent!

[Kevin Buzzard]

I don't think Lean is currently too hard to use for beginning undergrads at all. I _do_ think that attempting to teach e.g. undergraduate analysis to 1st years by plonking Lean in front of them and saying "OK so here is a bunch of new material which is extremely unlike anything you've ever seen before, and by the way you're going to have to learn a programming language as well" is unreasonable.

[Kevin Buzzard]

However if the student already knows, or can easily pick up, the material (as is the case for the maths going on in the natural number game) then I think it's fine. And of course once you've played NNG you're better at Lean so then when you try to do basic 1st year analysis in Lean it's less scary.

[Jake Levinson]

I see, that makes sense. My students do not know anything substantive about the Peano axioms -- they know proof by induction and I talked a bit about what the axioms are and how every fact about N is ultimately proven by induction. But we didn't actually prove a+1=1+a or anything like that.

[Kevin Buzzard]

To get from the naturals to the integers you either do something which is mathematically quite nasty (define the integers as the disjoint union of two copies of the naturals and develop from there, which is what is done in mathlib, and of course now you have to deal with the fact that one of the maps in is $x\mapsto -1-x$ which has no nice properties so it's a bit of a nightmare) or you have to deal with quotients, which in my experience students find hard, so this is an issue.

[Kevin Buzzard]

My most recent attempt to teach quotients in Lean to maths students is here https://xenaproject.wordpress.com/2021/03/04/formalising-mathematics-workshop-7-quotients/ but these people knew all the mathematical material back to front already.

[Jake Levinson]

My students are going to hear a very loose sketch of the quotient approach. I will say how Z can be formally constructed as equivalence classes of pairs, and give some intuition for what is going on. But that's because it's early groundwork for quotients (of rings) later in the semester.

[Jake Levinson]

Hmm, I think I did a tutorial on quotients from LFTCM2020. Is that the same one?

[Kevin Buzzard]

I think it's hard to learn that stuff and also to learn how Lean does quotients at the same time. I had a hard enough time getting to grips with quotients in Lean when I was learning it, and I had 25 years of number theory research under my belt

[Kevin Buzzard]

I don't think I wrote the LFTCM2020 quotients tutorial so I'm guessing it's not (I didn't use the tutorial as a source when I was writing that stuff either)

[Reid Barton]

I wonder if there would be any merit to something like "pairs $(a, b)$ with either $a = 0$ or $b = 0$"

[Kevin Buzzard]

There's also this for quotients: https://github.com/leanprover-community/mathlib/blob/master/docs/tutorial/Zmod37.lean

[Jake Levinson]

Oh fun. I mean personally I have yet to properly understand Lean quotients, despite having done one (1) tutorial so far.

[Jake Levinson]

@Reid do you mean for defining Z in Lean?

[Kevin Buzzard]

The blog post I linked to above is supposed to be an explanation of Lean quotients for someone who is mathematically mature (i.e. knows them back to front on paper)

[Kevin Buzzard]

Reid is suggesting yet another definition. Chris Hughes has also suggested the quotient of Nat disjoint Nat by identifying the 0's and then the two maps are x to x and x to -x, but again this involves quotients

[Reid Barton]

Yeah. Basically the quotient approach but you split the quotient by choosing a "best" representative. Probably not very good pedagogically because nobody does it that way.

[Reid Barton]

It's similar to the way the rationals are defined in Lean (fraction in lowest terms, with positive denominator)

[Jake Levinson]

What. Rationals aren't defined as a localization?

[Kevin Buzzard]

I guess one could also do nat disjoint union pnat!

[Kyle Miller]

Reid Barton said:

I wonder if there would be any merit to something like "pairs $(a, b)$ with either $a = 0$ or $b = 0$"

That has the nice property that the two inclusions of naturals as the non-negatives and non-positives are rather clean, which seems to have some merit.

[Jake Levinson]

What about having Nat start at 1 and taking two copies of that, plus 0?

[Kevin Buzzard]

No -- rationals are defined as pairs (a,b) with a an integer and b a positive natural and a coprimality assumption. Computer scientists seem to want to avoid quotients at all costs -- all this stuff was done in Lean before there were mathematicians involved.

[Jake Levinson]

I see. Do you know why they want to avoid quotients?

[Kevin Buzzard]

Jake Levinson said:

What about having Nat start at 1 and taking two copies of that, plus 0?

right -- pnat is the positive naturals. The CS people won't entertain the possibility that nat starts at 1, 0 makes more sense to them in applications apparently (they don't count things)

[Jake Levinson]

I have already broken my promise to my students -- today I told them the naturals would start at 1 instead of 0 for us. Then I went and started the division theorem, which is much more convenient to do with N starting at 0.

[Jake Levinson]

But in my defense, I am a mathematician

[Jake Levinson]

I don't have to be consistent

[Kevin Buzzard]

just make sure you're canonical

[Jake Levinson]

Also, after hacking on Lean a lot in the last few weeks, I've noticed that listening to real-world math proofs is sometimes becoming... weirdly uncomfortable, because now I start noticing all the casual identifications and omitted assumptions and skipped steps...

[Mario Carneiro]

Reid Barton said:

I wonder if there would be any merit to something like "pairs $(a, b)$ with either $a = 0$ or $b = 0$"

This is the implementation in metamath BTW. It is easier to work with than the lean version, especially if you add a "reduction" function to turn an arbitrary pair into a "best" pair, so that you can basically act like you have the equivalence class version, but it has the advantage that it doesn't need the existence of infinite sets so you can do it in ZF-inf

[Kevin Buzzard]

yeah, that's the start of the slippery slope. I remember derailing the number theory seminar a few years ago demanding that the speaker explain what they meant when they wrote "this correspondence is canonical" on the board...

[Kevin Buzzard]

so what's with the quotient avoidance Mario?

[Kyle Miller]

Kevin Buzzard said:

Computer scientists seem to want to avoid quotients at all costs -- all this stuff was done in Lean before there were mathematicians involved.

Sometimes I like appealing to the universal property of quotients and constructing a more convenient type -- things don't have to literally be quot to be a quotient.

[Mario Carneiro]

In metamath, the quotient avoidance is to avoid dependence on the axiom of infinity as mentioned; in lean, the quotient avoidence is to avoid blowup of the underlying representations in the VM (especially on rat)

[Jake Levinson]

Kevin Buzzard said:

yeah, that's the start of the slippery slope. I remember derailing the number theory seminar a few years ago demanding that the speaker explain what they meant when they wrote "this correspondence is canonical" on the board...

What is wrong with 'canonical'? I feel like I always interpret it as either "functorial" in some inferrable sense, or at least exists-unique, also possibly just in some inferrable sense.

[Yaël Dillies]

Who cares about concrete structures anyway?

[Yaël Dillies]

Just build the algebraic hierarchy :upside_down:

[Mario Carneiro]

The presence of a quotient in multiset and finset is also periodically problematic, for example in the nested inductive inductive foo | mk : finset foo -> foo

[Jake Levinson]

Mario Carneiro said:

In metamath, the quotient avoidance is to avoid dependence on the axiom of infinity as mentioned; in lean, the quotient avoidence is to avoid blowup of the underlying representations in the VM (especially on rat)

I see. So is the issue that if I calculate say 1/2 + 1/4 + 1/8 + 1/16 + ... + 1/2048 + 1/2048 then internally the actual calculation has been rendered as 2048/2048 and never gets reduced?

[Mario Carneiro]

right

[Mario Carneiro]

in fact, the numbers blow up exponentially even with something as simple as 1/2 + 1/2 + 1/2 + ...

[Jake Levinson]

oh dang. right.

[Kevin Buzzard]

Jake Levinson said:

What is wrong with 'canonical'? I feel like I always interpret it as either "functorial" in some inferrable sense, or at least exists-unique, also possibly just in some inferrable sense.

When you state that a construction which eats an automorphic representation of G (an element of a set, not a category) and spits out a Galois representation into the dual group of G (ditto) is "canonical" there are no functors and no bijections so you have to say what you mean.

[Patrick Massot]

$\mathbb{N}$ starting at 1 is really nonsense. You really want $\mathbb{N}$ to be a monoid.

[Adam Topaz]

Also a good reason to say $\mathbb{N}^\times = \{1,2,...\}$ (a multiplicative monoid)

[Jake Levinson]

As the popular saying goes, "counting is as easy as 0, 1, 2!"

[Johan Commelin]

You really want $\mathbb{N}$ to be a linear ordered commutative semiring.

[Kevin Buzzard]

Everyone says this but I had nat starting at 1 in my head (and in my thesis and papers) for decades

[Ben Toner]

Taking this thread off-topic and answering the original question: I recommend Tao, Analysis I, Chapters 2, 4 (and potentially 5 if you want $\mathbb R$ as well).