870: Structural Proof Theory/2

[Mario Carneiro]

On Sun, Mar 21, 2021 at 9:56 PM Buzzard, Kevin M <k.buzzard at imperial.ac.uk>
wrote:

> KB: Commutativity is harder because it involves
> discovering an idea which you don't mention: Sa + b = S(a+b).
>

> KB: I would say that commutativity of addition requires an idea.
>
Try proving it by induction yourself -- you run into an issue.
> The art is to build up the right theorems in the right order.
>

I would say that commutativity can also be done by "following your nose",
but it requires some higher order thinking. Specifically, you can do the
straightforward proof by induction, and you will get stuck, and you can
isolate the issue to exactly the statement Sa + b = S(a+b). So you
conjecture it, see that it's true for small numbers, and then try to prove
it by induction, which succeeds. (I believe you have to do this in the base
case as well, where 0 + n = n shows up.) I'm not sure what the state of the
art is regarding deriving new conjectures from proof failures (which can be
tough because there are lots of reasons a proof can fail and most of them
are not interesting from a conjecture making POV). In this case it works
because everything else in the proof is very straightforward, there's just
the single missing link. I think humans, when they do this, will call on
their model of the natural numbers to find the conjectures, but every time
I do this commutativity exercise I always discover the 0+n=n and
Sa+b=S(a+b) lemmas after the fact in the course of the proof.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210322/e2936d89/attachment-0001.html>