[TYPES] teaching discrete math and logic to undergraduates

[Derek Dreyer]

Yes, of course.  My point was simply that, for certain classes of
propositions A, "A or not A" is constructively true (e.g. if A is "x =
some particular algebraically constructed value").  Thus, having a
step in one's proof that says "we know that either A or not A" does
not imply that one's proof is classical.

This is obvious to people here, but I'm not sure it's obvious to many
students, especially when they see proofs written out informally.  (I
certainly remember being confused about it a long time ago and having
to just figure it out for myself.)

It's very common, for example, in metatheory appearing in PL papers to
see things like "either e is a term of the form e1(e2) or it is
not...Case 1: suppose it is...Case 2: suppose it isn't..."  Writing
that in one's proof does not mean that one has relied on excluded
middle, it just means that in the informal proof one has skipped the
step where one constructively proved the either/or using a case
distinction on the structure of terms.  However, to the student, such
an informal constructive proof may appear indistinguishable from the
non-constructive proof of the irrational example.  I think it's worth
at least pointing this out to students, by way of noting that most of
the intuitive reasoning they do is in fact intuitionistic.

Derek

On Sat, Aug 22, 2009 at 10:25 PM, Marco
Devillers<marco.devillers at gmail.com> wrote:
> 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
>>>
>>
>