Re: Derive ET from DN in calculus of constructions
"Albert Y. C. Lai" <[email protected]>
| Newsgroups | gmane.comp.lang.haskell.cafe |
|---|---|
| Message-ID | <[email protected]> |
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 <[email protected] > <mailto:[email protected]>> 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. _______________________________________________ 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.