[TYPES] teaching discrete math and logic to undergraduates

[Derek Dreyer]

Olivier's example brings up an important point that as a student I
remember being confused about.  It's possible that Jean's very
interesting notes already discuss this point, but at first glance I
didn't notice it.

Proof by contradiction (and law of excluded middle) are perfectly
valid principles even in constructive logic, for SOME propositions of
interest.  In the Minesweeper example, a critical axiom of the game is
that every cell is in one of two states: either it contains a mine or
it is empty, but not both.  Given this axiom, the student's intuitive
proof-by-contradiction or excluded-middle-elimination strategy for
Minesweeper is perfectly constructive, since the proposition in
question (whether a cell contains a mine) is known constructively to
be either true or false.

For me, the important moral is to be aware that when you do proof by
contradiction, you should have a pretty good reason to believe that
the theorem you are proving is actually either true or false.

Derek

On Sat, Aug 22, 2009 at 5:33 AM, Olivier Danvy<danvy at brics.dk> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
>> 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
>