[Agda] A philosophical question on absurd.

[Thorsten Altenkirch]

The absurdity of absurd doesn’t only show up in the propositions-as-types explanation. Even purely logical the bottom elimination rule has the same counterintuitive property: ex falso quod libet, from false follows everything. The issue is rather linguistic in nature there isn’t really a counterpart to False in natural language. In my logic course I explained that False should be translated as “pigs can fly”. This also explains the definition of “not P” as “P -> False”. I used the following example: if a girl wants to say “I am not going to marry you”, she could say “If I am going to marry you then pigs can fly”. It means no. 😊

Thorsten

From: Agda <agda-bounces at lists.chalmers.se> on behalf of David Banas <capn.freako at gmail.com>
Date: Friday, 28 August 2020 at 14:12
To: Agda mailing list <agda at lists.chalmers.se>
Subject: [Agda] A philosophical question on absurd.

Hi all,

I'm brand new to Agda and the Curry-Howard isomorphism (and really loving this new exploration of both!), and I have a philosophical objection to how the absurd function is used to generate whatever we need to complete a proof.

I understand how we are able to satisfy the Agda compiler with the definition of absurd; my objection isn't mechanical/technical.

What bothers me is a feeling that I'm "cheating" when I use this function that can never be called, in order to "produce" that which I need to complete my proof.

I wonder if someone could offer a different perspective on this, for consideration.

Thanks!
-db




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200828/d801f991/attachment.html>