Why do we need to prove both proposition to apply Disjunction Elimination in Isabelle?

Question

I was seeing the proof rule for disjunction elimination and I noticed we have to prove BOTH statements to use it:

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

why is that? Like in normal logic if I knew ONE was true then I'd know the whole thing was true so who cares what the other's truth value is. Similarly if I can prove at least once why can't I eliminate the disjunction/or?

For context, I was trying to prove:

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

but eventually I got stuck in cycles and I don't know why:

 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)

proof seems obvious but can't get isabelle to comply...

Answer 1

I think explaining both OrE and AndE rules and comparing them is productive. Let's start with the Or (disjunction):

Disjunction Elimination

Recall the rule: disjE = OrE: ⟦ P ∨ Q; P ⟹ R; Q ⟹ R ⟧ ⟹ R. To explain it consider the following story:

You know P or Q but you don’t know which one. Assume this statement means that that cup P or cup Q has a $10 bill under it. If you want to conclude R using that fact (e.g. R = Buy lunch) then you must make sure you do indeed get the $10 bill. Since you do NOT know which one has the $10 bill you need to create a tool (i.e.) that lifts BOTH cups, to guarantee you do get the $10 bill. Thus, to use that fact in your proof you need to construct a proof for both P=>R and also Q=>R because you do not know which one is true.

now let's comapre it with conjuction elimination/AndE.

Conjunction Elimination

Recall the different ways the express the rule:

• AndEL [|P /\ Q; P=>R |] => R
• AndER [|P/\ Q; Q=>R|] => R
• conjE: ⟦ P ∧ Q; ⟦ P; Q ⟧ ⟹ R ⟧ ⟹ R

To explain consider the following story:

The $10 bill analogy. If we have P /\ Q then we know that there is a $10 dollar bill under both the P cup AND Q the cup. Thus, we only need a tool (i.e. a proof) to raise one to arrive at R (say buy lunch). Thus, for this rule since we know BOTH have $10 bills we only need to construct a tool (proof) to lift 1 of the cups. Therefore, that is why we need to only have a proof of ONE of the statements for the And E rule. In fact what isabelle does is compress the rule and say “if you raise either cup (i.e. ⟦ P; Q ⟧ which means you can use either assumption) then you can conclude R”.

note: note that ⟦ P; Q ⟧ ⟹ R actually means just having either of the assumptions P or Q to conclude R. So it’s a compressed way to have both AndE in one (because you might use either of the assumptions to conclude R).

Bonus: allE & exE

allE

• allE [| ∀x. ?P x ; (?P ?x ⟹ ?R) |] ⟹ ?R
  • this is an unbounded “conjunction”/AND. Basically to remove a forall then we just need one specific example (just like we eliminate a specific AND).
  • [| ∀x. ?P x ; (?P ?x ⟹ ?R) |] ⟹ ?R
    • the specific x that we need to “remove the unbounded AND" is ?x.

exE

• exE [|∃x. ?P x ; (⋀x. ?P x ⟹ ?Q)|] ⟹ ?Q
  • this is an unbounded “conjunction”/OR. Basically to remove we we’d need to prove it for all instances. Thus, the reason we use a meta-forall with the meta-abstraction /\ (and of course a fresh variable instance!) Because it has to hold for all of them regardless of what the specific term is (as long as we have not reference the term already).
  • [|∃x. ?P x ; (⋀x. ?P x ⟹ ?Q)|] ⟹ ?Q
    • the fresh variable we are introducing is ⋀x to remove the unbounded OR.

Answer 2

The rule you want to apply, namely disjunction elimination (disjE), allows you to eliminate a disjunction P ∨ Q in the premises without knowing a priori whether P or Q is true. In that situation, you need to consider both cases separately (i.e. assume P is true and assume Q is true) in order to safely eliminate the disjunction. More precisely, if you can prove a conclusion R in both cases, then you are safe to eliminate the disjunction P ∨ Q and conclude R. When you say "if I knew ONE was true then I'd know the whole thing was true so who cares what the other's truth value is" I think you are actually referring to disjunction introduction (disjI1 and disjI2, respectively ?P ⟹ ?P ∨ ?Q and ?Q ⟹ ?P ∨ ?Q).

Answer 3

Using auto in the middle of a hand-written detailed apply proof is very strange. Your problem is that you applied disjE too late: you need to apply it before impE and not after (it is an issue of --> vs ==>: with impE you commit to the choice 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

Here is another working proof that is closer to what you want on paper:

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

Remark that, unless you have a specific reason to do so, you should use by blast that solves the complete goal.