[TYPES] teaching discrete math and logic to undergraduates

[Marco Devillers]

Hi all, I usually don't post, so don't bother. But here I couldn't resist.

This is not law of the excluded middle but case distinction on
(algebraically?) constructed values. A logic is classic, or not, by
assuming propositions are, or are not, two-valued. Bringing those
values into the logic is what matters.

I don't think presenting case distinctions as law of excluded middle
makes sense.

Just 2 cents of thought. Bye all.

On Sat, Aug 22, 2009 at 10:39 AM, Derek Dreyer<dreyer at mpi-sws.org> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> 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
>>
>