为什么我们需要证明两个命题才能在Isabelle中应用析取消除？

Question

[我看到消除析取的证明规则，并且我注意到我们必须证明两个陈述才能使用它：

?P ∨ ?Q ⟹ (?P ⟹ ?R) ⟹ (?Q ⟹ ?R) ⟹ ?R

为什么？就像在正常逻辑中一样，如果我知道一个人是真实的，那么我会知道整个事情都是真实的，那么谁在乎另一个人的真实价值是什么。同样，如果我至少可以证明一次，为什么不能消除析取/或？

出于上下文，我试图证明：

proof (prove)
goal (1 subgoal):
 1. ∀s. P s ∨ Q s ⟹ ∀s. P s ⟶ R s ⟹ ∀s. Q s ⟶ R s ⟹ ∀s. R 

但是最终我陷入了循环，不知道为什么：

 apply (rule allI)
  apply (rule_tac P="λs. P s ∨ Q s" in allE)
   apply assumption
  apply (erule_tac P="λs. P s ⟶ R s" in allE)
  apply (erule_tac P="λs. Q s ⟶ R s" in allE)
  apply (erule impE)
   defer
   apply assumption
  apply auto
  apply (erule allE)
  apply (erule disjE)

证据似乎很明显，但无法让伊莎贝尔遵守...

Answer 1

在手写的详细申请证明中间使用自动，这很奇怪。您的问题是您应用disjE的时间太晚了：您需要在impE之前而不是之后应用它（这是-> vs ==>的问题：使用impE时，您会做出选择P）。

lemma ‹∀s. P s ∨ Q s ⟹ ∀s. P s ⟶ R s ⟹ ∀s. Q s ⟶ R s ⟹ ∀s. R s›
 apply (rule allI)
  apply (rule_tac P="λs. P s ∨ Q s" in allE)
   apply assumption
  apply (erule_tac P="λs. P s ⟶ R s" in allE)
  apply (erule_tac P="λs. Q s ⟶ R s" in allE)
  apply (erule disjE) 
  apply (erule impE)
    apply assumption+ 
  apply (rotate_tac 2)
  apply (erule impE)
    apply assumption+
  done

这里是另一个更接近您在纸上想要的工作证明：

lemma ‹∀s. P s ∨ Q s ⟹ ∀s. P s ⟶ R s ⟹ ∀s. Q s ⟶ R s ⟹ ∀s. R s›
  apply (rule allI)
  apply (drule_tac x=s in spec)
  apply (elim disjE)
  apply (drule_tac x=s in spec)
   apply (erule impE)
    apply assumption+
  apply (rotate_tac)
  apply (drule_tac x=s in spec)
   apply (erule impE)
    apply assumption+
  done