Hi Mario,
I want to do it mainly because I want to prove things in the form of ~~A,
which means that I need to prove things like (A ==> F) ==> F. There comes
the problem you see.
Any advice?
Cheers!
Regards,
Robert
On 22 May 2015 at 01:31, Mario Carneiro <di.g...@gmail.com> wrote:
> Hi Robert,
>
> This is more a pure logic answer than a HOL-specific one, but... The
> reason why (((A==>B)==> C)==> D)==> E is hard to prove is because it is has
> a very awkward interpretation, especially in intuitionistic logic (where I
> expect the statement is unprovable unless it trivialises in some way). In
> classical logic, since the statement is equivalent to (A \/ C \/ E) /\ (!B
> \/ C \/ E) /\ (!D /\ E) in CNF, you could reduce the goal to proving (!A /\
> !C) ==> E, (B /\ !C) ==> E, D ==> E which lend themselves more easily to
> the usual methods of natural deduction. (I'm no HOL expert, but you could
> make the given transformation using TAUT and simplify from there.)
>
> Why are you faced with such an unusual goal shape? Such statements do not
> often appear in the course of a larger natural deduction proof.
>
> Mario Carneiro
>
> On Thu, May 21, 2015 at 4:10 PM, Robert White <
> ai.robert.wangsh...@gmail.com> wrote:
>
>> (sorry. I just sent the previous email by mistake, here is the complete
>> version)
>> Dear all,
>>
>> I wonder if there is better way to handle proofs like (((A==>B)==> C)==>
>> D)==> E (in top-down proofs, I also wonder how I should do it in bottom up
>> proofs),
>>
>> After doing a UNDISCH, all the A...D will go to the hypothesis part. I
>> understand that in natural deduction, we don't do much on the hypothesis
>> side. So apart from doing MP to get:
>>
>> K ==> (((A==>B)==> C)==> D)==> E K
>> ---------------------------------------------------------- MP
>> (((A==>B)==> C)==> D)==> E
>>
>> and EQ_MP (which is similar as above), what else could I do to make a
>> less painful proof?
>>
>> Sorry again for sending the previous email a few sec ago unexpectedly.
>> Thanks very much.
>> --
>>
>> Regards,
>> Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
>> INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
>>
>>
>> ------------------------------------------------------------------------------
>> One dashboard for servers and applications across Physical-Virtual-Cloud
>> Widest out-of-the-box monitoring support with 50+ applications
>> Performance metrics, stats and reports that give you Actionable Insights
>> Deep dive visibility with transaction tracing using APM Insight.
>> http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
>> _______________________________________________
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>
--
Regards,
Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
