David,
I don't quite understand what you are trying to do here.
On the face of it you want a rule:
p
------ false-intro
false
But this is not possible, because it is not sound.
As far as I can see Woodcock does not have a false-intro rule,
he has only a false-elim rule, is that what you want to reproduce?
Woodcock, so far as I can see, introduces false by using ¬-elim.
Could you clarify what you are looking for?
Roger
On 14/08/2016 01:21, David Topham wrote:
Roger (or Rob), I have been studying "UsingZ" by Jim Woodcock and JIm
Davies. They use the "sequent" method and show a proof that derives
"false". In looking through the inference rules in USR029 I don't see
a rule that matches "false-intro". Can you suggest how to approach
this type of proof (it is for my Discrete Match course). -Dave
i.e. What rule would I replace ??? with for L6
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
