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

[mukesh tiwari]

Hi Dmitriy, 


"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.” 


Yes, it is possible and below is a hint (in Coq). You can play this in online Coq compiler [2].

Definition DN_implies_EM : (forall q : Prop, ~~q -> q) -> (forall p : Prop, p \/ ~p).
Proof.
    refine
      (fun (Ha : forall q : Prop, ~ ~ q -> q) (p : Prop) =>
         Ha (p \/ ~ p)
         ((fun Hb : ~ (p \/ ~ p) => 
         Hb _ ) : ~ ~ (p \/ ~ p))).
Admitted.

The remaining goal is 

Ha : forall q : Prop, ~ ~ q -> q
p : Prop
Hb : ~ (p \/ ~ p)
============================
 p \/ ~ p

So can you see the proof now? Spoiler alert: complete proof [1].
 

Best, 
Mukesh 


[1] https://gist.github.com/mukeshtiwari/f3de83335830ce4e287f231499028d6f
[2] https://jscoq.github.io/scratchpad.html



> On 4 Nov 2024, at 21:24, Albert Y. C. Lai <trebla at vex.net> wrote:
> 
> 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.
> 
> _______________________________________________
> 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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20241105/99969726/attachment.html>