Roger,

> On 12 Mar 2016, at 17:30, Roger Bishop Jones <r...@rbjones.com> wrote:
> 
> David,
> 
> This is not an alph-conversion error.
> The reference to apha conversion is a normal qualifier when
> any rule doesn't get what it needs, since in general a statement of of what
> is needed need only be complied with "up to alpha conversion".
> 
> The real problem here (I guess since I can't actually see the command
> which caused the error, and I can't see the error message), is that you
> have not supplied the arguments required by the rule you are using.
> 
> You have to give it a theorem with a disjunction in the conclusion and a 
> theorem
> whose conclusion is the negation of one of the disjuncts.

Yes. David was optimistically expecting q in the conclusion of L3 to hook up 
with ¬ q
in the conclusion of L4, but, as Mark pointed out, you need to use  ¬_¬_intro 
to change
the conclusion of L3 to ¬ ¬ q to get this to work.

Regards,

Rob. 


_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to