[Agda] A philosophical question on absurd.

[Manuel Bärenz]

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
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200828/a844704b/attachment.html>