在农民宇航员中形成逻辑

Question

电影中有这样的逻辑，我无法完全形式化（例如在 Coq 中）。

有人想在他的农场发射一枚火箭，监视该地点的联邦调查局人员正在互相讨论他们为什么在那里。一个人说：

因为如果我们不在这里而他发射了，我们就会看起来像*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).

Answer 3

这个讨论是没有意义的，因为如果他不启动，唯一发生的事情就是耕种耕种了1000次的田地……考虑到手段的目的，这并不是愚蠢的事情，但在我看来，关于你的等式的真正愚蠢的事情是他们不会帮助他发射，因为没有发射他们都还在这里。