农民航天中的一种逻辑

Question

在一部电影中有这样的逻辑，我不能很好地形式化(例如在Coq中)。

有人想在他的农场上发射火箭，监视现场的FBI人员正在互相谈论他们为什么会在那里。一个人说：

因为如果我们不在这里，他发射，我们将看起来像*s。

然后另一个人回应说

如果我们在这里而他发射了呢？

答：

我们看起来还是像*s。

这里的逻辑似乎是这样的：

A = we look foolish
B = he launches
C = we are not here.

我们有

 B /\ C -> A    and
 B /\ ~C -> A

此外，似乎C (我们在这里)是否成立并不重要。这一结论归结为B -> A。(如果他发射，我们就会显得愚蠢)。

我们能证明这个理由吗？

我试过：

Theorem farmer: forall A B C:Prop, 
(B /\ C -> A) -> (B /\ ~C -> A) -> (B -> A).
Proof.
intros. tauto.

那它就卡住了。我试着添加被排除的中间，但是tauto仍然不能证明它。

另一方面，在执行布尔代数时，我们有：

(~B + ~C + A)(~B + C + A) = 
(~B + A)C + (~B + A)~C + (~B +A) =
~B + A.

即

(B /\ C -> A) /\ (B /\ ~C -> A) = B -> A.

如何在Coq的逻辑中证明这一点，或者我得出的结论是错误的？

Answer 1

我不知道你为什么不遵守“排除中间定律”，因为证明这个命题就足够了：

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.

Answer 2

如果没有您的命题的可判定性，我不确定您是否能够证明您想要的:您仍然需要知道C是否是真的。然而，您的陈述需要复杂的命题相等，我建议您更确切地说：

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