[Agda] Classical Mathematics for a Constructive World

[Andreas Abel]

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
>>>
>>
>
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/