873: Structural Proof Theory/5

Buzzard, Kevin M k.buzzard at imperial.ac.uk
Sun Mar 21 05:54:16 EDT 2021

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


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.



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,<.


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?

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>

More information about the FOM mailing list