[Agda] Classical Mathematics for a Constructive World

[Peter Divianszky]

 > Nice slides, Peter!

Thanks!

I corrected the slides and I made them available here:

http://people.inf.elte.hu/divip/Agda.pdf

 >    If you start with conjunction and negation, should not be classical
 > implication be defined as
 >
 >     not (A and not B)

Now I define classical connectives on the slides with corresponding 
constructive connectives and double negation.

Cheers,
Peter


On 17/12/2012 21:13, Andreas Abel wrote:
> Nice slides, Peter!
>
> Here are some remarks that came to me while reading your slides.
> Cheers,
> Andreas
>
> slide 21
>
>    It does not make much sense to define a Top-elimination rule.  In
> natural deduction, there is no such rule; it is an artifact of defining
> Top as a data type.  The definition as record
>
>    record Top : P where
>
> clearly does not give an elimination rule.  (I understand that you do
> not want to go into records in this tutorial, but maybe drop the
> Top-elim rule.)
>
> slide 22
>
>    If you start with conjunction and negation, should not be classical
> implication be defined as
>
>     not (A and not B)
>
> slide 34 3rd bullet
>
>    n * 3 == n + n + n  needs induction on n, the wording on the slide is
> a bit misleading.  Simplification alone does not suffice.
>
> On 17.12.12 2:53 PM, Peter Divianszky wrote:
>> Hi,
>>
>> I have advertised Agda, I presented the attached slides for approx. 30
>> mathematicians in Debrecen, Hungary, 20 of them were students.
>> One of my students in Budapest translated the slides to English so I can
>> present them to you.
>>
>> Your answers for my questions in this mailing list helped me a lot too,
>> thank you very much.
>>
>> (I hope I didn't claim any false statement about Agda, please tell me if
>> you find so.)
>>
>> Cheers,
>> Peter
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>