On Sat, May 23, 2015 at 5:35 PM, Albert Y. C. Lai <tre...@vex.net> wrote:
> On 2015-05-22 04:16 AM, Robert White wrote:
> > 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.
>
> In natural deduction forward order (HOL4 forward rules in parentheses):
>
> Prove ⊢A some way.
I'm not sure this is the best example, because if you are trying to prove
~~A then presumably A is not provable (or else you would use that instead
of the weaker ~~A). For example, take A = (B \/ ~B). Obviously this is not
provable in IL, but its double negation is. To prove ((B \/ ~B) ==> F) ==>
F, assume (B \/ ~B) ==> F:
(B \/ ~B) ==> F |- (B \/ ~B) ==> F
Now assume B and apply OR-introduction:
B |- (B \/ ~B)
so that by MP,
(B \/ ~B) ==> F, B |- F.
Discharge B to get
(B \/ ~B) ==> F |- B ==> F
and apply the definition of ~B:
(B \/ ~B) ==> F |- ~B
Then by OR introduction,
(B \/ ~B) ==> F |- (B \/ ~B)
so that by MP, ((B \/ ~B) ==> F) ==> F.
(Apologies for not knowing the HOL commands to replicate this natural
deduction derivation tree.)
Mario
------------------------------------------------------------------------------
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
