Email Gateway (Aug 18 2022 at 13:11): Email Gateway (Aug 18 2022 at 13:11):From: Peter Chapman <pc@cs.st-and.ac.uk>
Hi
I have the following premisses and goal (the details are unimportant,
it is the structure which is important):
[| [| A ; B |] ==> C ; D ; E ; A ==> D ; B ==> E |] ==> C
I think this should be provable, I rewrite using the A ==> D and B ==>
E inside the inner [| |] to get
[| [| D ; E |] ==> C ; D ; E |] ==> C
to
C
Is this logically sound? How can I rewrite the A and B within the
inner brackets?
Thanks in advance
Peter
Email Gateway (Aug 18 2022 at 13:11):From: Tjark Weber <webertj@in.tum.de>
Peter,
it's not. Isabelle finds a counterexample automatically:
Counterexample found:
A = False
B = False
C = False
D = True
E = True
If some of the implications are the other way round, the statement
becomes provable, e.g., by simp:
lemma "[| [| A ; B |] ==> C ; D ; E ; D ==> A ; E ==> B |] ==> C"
by simp
Regards,
Tjark
Email Gateway (Aug 18 2022 at 13:12):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hi Peter,
your reasoning is not sound: Take, e.g., A=B=C=False, and D=E=True.
Then, your goal reads
[| [| False ; False |] ==> False ; True ; True ; False ==> True ; False
==> True |] ==> False
which simplifies to False, whereas you want to rewrite this to
[| [| True; True |] ==> False; True; True |] ==> False
which is True. The problem is that you need both A and B to show C, but
you only have D and E, which are weaker than A and B.
Best regards,
Andreas
Peter Chapman schrieb:
Email Gateway (Aug 18 2022 at 13:12):From: Christian Doczkal <c.doczkal@stud.uni-saarland.de>
Am Montag, den 16.03.2009, 16:11 +0000 schrieb Peter Chapman:
Hi
I have the following premisses and goal (the details are unimportant,
it is the structure which is important):[| [| A ; B |] ==> C ; D ; E ; A ==> D ; B ==> E |] ==> C
I think this should be provable
Indeed it is not, if you enter
lemma "[| [| A ; B |] ==> C ; D ; E ; A ==> D ; B ==> E |] ==> C"
Isabelle answers
Counterexample found:
A = False
B = False
C = False
D = True
E = True
, I rewrite using the A ==> D and B ==>
E inside the inner [| |] to get[| [| D ; E |] ==> C ; D ; E |] ==> C
This is actually not sound as the occurrences of A and B are negative.
Just because you need A and A implies D you can't use D instead. On the
Other hand, if you have D and D implies A you may use A. If you reverse
the other implications the thing becomes provable.
lemma "[| [| A ; B |] ==> C ; D ; E ; D ==> A ; E ==> B |] ==> C"
by simp
to
C
Is this logically sound? How can I rewrite the A and B within the
inner brackets?Thanks in advance
Peter
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC