[TYPES] teaching discrete math and logic to undergraduates

[Olivier Danvy]

> A lot of proofs by contradiction have this pattern:
> 
> I want to show A implies B.  So assume A and NOT-B.  Now prove B then 
> exclaim, contradiction!  OK, so I was half-joking.  I am sure none of 
> the readers of this group do this, but I have seen students do it.

Yet students who play the Minesweeper game
  http://en.wikipedia.org/wiki/Minesweeper_(computer_game)
do use proofs by contradiction once they can't use any further
modus-ponens proofs:

* The modus-ponens proofs pertain to saturation: if there is a 1 here and
  I know the neighbour which is a mine, all the other neighbours are not
  mines.

* The proofs by contradiction posit that there is a mine here, and then
  proceed by saturation; if saturation yields a contradiction, there was
  no mine here.  And the better players do it all the time, sometimes in
  a nested fashion.

We need to connect the intuitive, self-invented proofs by contradiction
of the students with the formal proofs by contradiction of the teachers
without removing the fun of playing Minesweeper and of doing formal
proofs.

-- Olivier