[Agda] Classical Mathematics for a Constructive World

[Peter Divianszky]

Right.
I deleted the trivial theorems and uploaded the new version.

Thanks,
Peter

On 12/01/2013 11:16, Andreas Abel wrote:
> Hi, I looked at the updated definition of classical implication as A =>
> B = A -> not not B.  There is  a slide "Agda demonstration" after that.
>   Are not the last two theorems completely trivial (just the identity
> function) with the updated definition?  (Also r.a.a. is just the
> definition).
>
> Cheers
> Andreas
>
> On 11.01.13 9:19 PM, Peter Divianszky wrote:
>>  > 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
>>>>
>>>
>>
>>
>