[Agda] A philosophical question on absurd.

[Sandro Stucki]

Hi David,

I can offer a few perspectives. Whether or not you find them
convincing will depend on your prior beliefs.

(BTW, I assume that your definition of "absurd" is similar to the one
in Haskell's Data.Void or that of ⊥-elim from the Data.Empty module in
the Agda stdlib)

First, if you already believe that the Curry-Howard isomorphism is
true, then the logical interpretation of ⊥-elim is just that anything
follows from falsehood (aka, the explosion principle, or "ex falso
quodlibet") which is an important principle of both classical and
intuitionistic logic. See e.g.
https://en.wikipedia.org/wiki/Principle_of_explosion But that's not
very convincing if you're trying to justify Curry-Howard rather than
taking it at face value.

The second perspective is set-theoretic. If you believe that lambda
terms can be interpreted (at least intuitively) as set-theoretic
functions, then "⊥-elim {A}" is a function from the empty set to some
arbitrary set A. Since set-theoretic functions are relations mapping
every element in their domain to exactly one element in their
codomain, ⊥-elim is simply the empty relation. There are no elements
in the domain, so no mapping is required. This is true no matter what
the codomain A is.

A similar perspective is to interpret "⊥-elim {A}" as a proof of the
predicate "∀ x ∈ ⊥. A(x)", which holds vacuously, simply because the
"set" ⊥ is empty so A(x) trivially holds for all elements of ⊥.

Finally, if you are a fan of category theory and you believe in the
last part of the Curry-Howard-Lambek correspondence, then ⊥ has the
property of being initial (in some suitably chosen bicartesian-closed
category) and hence there is a unique morphism from ⊥ to any Object A.

Hope that helps
/Sandro

On Fri, Aug 28, 2020 at 3:12 PM David Banas <capn.freako at gmail.com> 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