logicboolean-logiccoq

Formualting a logic in farmer astronaught


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?


Solution

  • 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.