873: Structural Proof Theory/5

[Buzzard, Kevin M]

Re: electronic textbook (I made selective quotes below). Have you seen the Lean game I made?

http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/

I start with 0 and S and get the student to make <=.  Works fine. I had a lot
of fun experimenting with what to give the user and what to make them
prove themselves.

*******************
ELECTRONIC TEXTBOOK DESIGN

[snip]

STARTING POINT. I was trying to decide on whether to start with just
0,S, or whether to start with just 0,S, or best to start with 0,S,<.

[snip]

We immediately have a not uninteresting situation. What do we need to
prove the basic facts about < and for that matter, what are these
basic facts?

[snip]
We want to get that < is a strict linear ordering with obvious properties.

i. not(x < x)
ii. x < y implies not(y < x)
iii. x < y and y < z implies x < z

CRUDE QUESTIONS: What kind of inductions are needed to prove which of these?

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210321/249e99a3/attachment-0001.html>