[Agda] A philosophical question on absurd.

[David Banas]

Sorry, I just realized that I sent that last message w/o any context.
Here is what I was replying to:

> Hi,
> 
> One way to understand that you are not cheating when you pass an argument to absurd is to realise that this piece of code is already unreachable.
> Syntactically it seems that one could reach this part of the code with input values. However the whole system is designed such that it is not possible.
> 
> Nicolas

Thanks to all, who took time to respond!
This really is a wonderfully engaging community. :)

-db

> On Aug 28, 2020, at 9:07 AM, David Banas <capn.freako at gmail.com> wrote:
> 
> Ah, thank you; that helps.
> Sort of a back-propagation of absurdity, as it were?
> If something is calling absurd, then it must be absurd, as well; is that it?
> 
> Thanks!
> -db
> 
> 
>> On Aug 28, 2020, at 7:05 AM, Nicolas Pouillard <nicolas.pouillard+agda at gmail.com <mailto:nicolas.pouillard+agda at gmail.com>> wrote:
>> 
>> Hi,
>> 
>> One way to understand that you are not cheating when you pass an argument to absurd is to realise that this piece of code is already unreachable.
>> Syntactically it seems that one could reach this part of the code with input values. However the whole system is designed such that it is not possible.
>> 
>> Nicolas
>> 
>> On Fri, Aug 28, 2020 at 3:29 PM Manuel Bärenz <manuel at enigmage.de <mailto:manuel at enigmage.de>> wrote:
>> Hi,
>> 
>> I'm by no means an expert, but it seems to me that this "computational emptyness" of absurd is just corresponding to the fact that in constructive logic, you can't have proof by contradiction, only proof of negation. That is, at the end absurd will always prove a negation. It has type _|_ -> A for some A. You will never be able to construct an A with absurd, only ever its negation.
>> 
>> Manuel
>> 
>> On 28.08.20 15:11, David Banas wrote:
>>> 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
>>> 
>>> 
>>> 
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>> https://lists.chalmers.se/mailman/listinfo/agda <https://lists.chalmers.se/mailman/listinfo/agda>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>> https://lists.chalmers.se/mailman/listinfo/agda <https://lists.chalmers.se/mailman/listinfo/agda>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>> https://lists.chalmers.se/mailman/listinfo/agda
> 

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