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?
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>
More information about the FOM
mailing list