There is this logic in a movie which I can't quite formalize (e.g. in Coq).
Some one wanted to launch a rocket on his farm, the FBI guys monitoring the site are talking to one another about why they are there. One guy said:
Because if we are not here and he launches, we will look like as*s.
Then the other guy responded
what if we are here and he launches?
answer:
we'll still look like as*s.
It seems that the logic here is this: Given:
A = we look foolish
B = he launches
C = we are not here.
We have
B /\ C -> A and
B /\ ~C -> A
Furthermore, it seems that whether C (we are here) holds does not matter. The conclusion boils down to B -> A. (If he launches, we will look foolish).
Can we prove this reasoning?
I tried:
Theorem farmer: forall A B C:Prop,
(B /\ C -> A) -> (B /\ ~C -> A) -> (B -> A).
Proof.
intros. tauto.
Then it's stuck. I tried adding the excluded middle, but tauto still can't prove it.
On the other hand, doing boolean algebra, we have:
(~B + ~C + A)(~B + C + A) =
(~B + A)C + (~B + A)~C + (~B +A) =
~B + A.
i.e.
(B /\ C -> A) /\ (B /\ ~C -> A) = B -> A.
How can this be proved in Coq's logic, or did I derive it wrong?
I don't know why you failed with Law of excluded middle, because it is sufficient to prove the proposition:
Axiom LEM: forall P:Prop, P \/ ~P.
Theorem farmer: forall A B C:Prop,
(B /\ C -> A) -> (B /\ ~C -> A) -> (B -> A).
intros.
destruct (LEM C); tauto.
Qed.