CODEWITHSUNDEEP
logicboolean-logiccoq
thor
thor

Reputation: 22530

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?

Upvotes: 1

Views: 54

Answers (3)

Bradley Wildcard
Bradley Wildcard

Reputation: 1

The discussion is moot because if he doesn't launch the only thing that happens is plowing a feild cultivated 1000's of times... not nessarally foolish considering the ends to the means but the truly foolish thing in my opinion about your equation is that they don't help him launch because without the launch they are all still here.

Upvotes: 0

larsr
larsr

Reputation: 5811

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.

Upvotes: 1

Vinz
Vinz

Reputation: 6057

Without decidability of your proposition, I'm not sure you can prove what you want: you still need to know if C is true or not. However your statement requires complex propositional equality, I advise you to rather state:

forall A B C:Prop, ((B /\ C) -> A) /\ ((B /\ ~C) -> A) -> (B -> A).

Upvotes: 0

Related Questions