[Haskell-cafe] Derive ET from DN in calculus of constructions

[Albert Y. C. Lai]

Heh, I find it amusing. But I have had prior experience from figuring 
out a similar proof. I used Pierce's Law (aka call/cc), but it too 
unfolds into the same story when evaluated.

On 2024-11-02 17:02, Brent Yorgey wrote:
> You may find this helpful:
> 
> https://www.cs.cmu.edu/~cmartens/if/dem.html <https://www.cs.cmu.edu/ 
> ~cmartens/if/dem.html>
> 
> Actually, you probably won't find it helpful, but at least it is 
> amusing.  And after you figure out your proof, you can go back and 
> figure out what this story has to do with it.
> 
> -Brent
> 
> On Fri, Nov 1, 2024 at 8:45 AM Dmitriy Matrosov <sgf.dma at gmail.com 
> <mailto:sgf.dma at gmail.com>> wrote:
> 
>     Hi.
> 
>     I've reading "Type theory and formal proof, an introduction"
>     book and in chapter 7.4 authors say, that in constructive
>     logic plus either excluded third law (ET) or double negation
>     law (DN) we can derive the other. And then authors derive DN
>     from ET in calculus of constructions. But they didn't say
>     anything (yet?) about the vice versa: deriving ET from DN in
>     calculus of constructions.
> 
>     I've tried to do this, but the best i can come up with is
>     just case analysis:
>     - assume, that 'a' is true, then 'a or not a' is also true
>        (by 'or-intro' rule).
>     - or if after assuming that 'a' is true we can derive
>        bottom, then 'not a' is true (by 'not-intro' rule).
>        Then using the 'or-intro' rule we again end up with 'a or (not
>        a)' being true.
>     - assume 'not a' and if we can derive bottom again, then
>        'not (not a)' is true. Then by using DN we again end up
>        with 'a' being true.  etc.
> 
>     I.e. I may reduce any (not.. (n times) .. not a) into either
>     'a' or 'not a' by using DN and function composition. Thus, i
>     probable can derive ET from DN using induction, but i can't
>     code neither induction, nor above case analysis in calculus
>     of constructions.
> 
>     So, is it possible to derive ET from DN in calculus of
>     constructions? If it is, i'd appreciate not a direct answer,
>     but a hint on how to do this. And if it is not,
>     well, probably, authors will explain this later in the book
>     and I should just continue reading.
> 
>     Thanks.
>     _______________________________________________
>     Haskell-Cafe mailing list
>     To (un)subscribe, modify options or view archives go to:
>     http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>     <http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe>
>     Only members subscribed via the mailman list are allowed to post.
> 
> 
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.