Disjunction Elimination: Make Both Branches Reach the Same Conclusion

Both cases must finish with the same sentence

Disjunction elimination requires a disjunction A∨B, a subproof from A to C, and a separate subproof from B to that same C. Then ∨E cites the disjunction and both complete ranges to conclude C outside the temporary case assumptions.

You are not allowed to choose the more convenient disjunct as an unconditional fact. Inclusive A∨B says at least one holds, but does not identify which. Proving C in both cases shows that the choice no longer matters to this conclusion.

Formal background: [1].

Our original proof derives R from (P→R)∧(Q→R) and P∨Q. It extracts both conditionals, uses one per case, and closes two sibling subproofs. A separate countervaluation shows why different case endpoints cannot simply be exported as R.

Plan one shared target before opening either block

The outer premises remain available in both cases. That is why each case can use the appropriate extracted conditional. But the temporary P assumption belongs only to the first block, and the temporary Q assumption belongs only to the second.

Write the shared goal R beside both planned endpoints. This makes a mismatch visible before you fill several lines. If one case naturally reaches S instead, you must find a shared conclusion supported in both cases, or add a justified step within that case to reach R.

Audit the two sibling blocks in nine lines

On a narrow screen, scroll inside this table. Keyboard users can focus the region and use the arrow keys.

Download both case ranges and the mismatch countervaluation

Line 7 starts a sibling block after the P case is closed. It does not add Q inside the P block. The second case therefore cannot use line 5 as an ordinary line citation. It can still use outer lines 1–4, which do not depend on P.

Line 9 is back at the outer level. Its justification names three things: the source disjunction, the complete first-case range, and the complete second-case range. Both ranges end in exactly R. The premises remain undischarged; the two temporary case assumptions are discharged.

The ∧E steps use the main conjunction of premise 1. Extracting a conjunct from an unrelated conjunction hidden inside a disjunction would not be licensed by this rule. Always match the connective to the whole cited formula.

Refute a tempting proof with mismatched endpoints

Different premises: (P → R) ∧ (Q → S), P ∨ Q
First case yields R; second case yields S.
Proposed conclusion: R

On a narrow screen, scroll inside this table. Keyboard users can focus the region and use the arrow keys.

With P=F, P→R is true even though R=F. With Q=T and S=T, Q→S is true. Their conjunction and the disjunction P∨Q are both true, but R is false. Thus these premises do not entail R.

The problem is not typography or an omitted label: one case genuinely fails to establish the proposed conclusion. If the task permits a weaker shared conclusion, both cases can establish R∨S using disjunction introduction. That yields R∨S, not R. State the changed target explicitly.

A source disjunction with complex disjuncts works the same way. The case assumptions must match its two whole disjuncts, and both endpoints must match the one exported sentence. Similar meaning guessed from prose is not a substitute for the formal match.

Explain why one successful case is insufficient

From P∨Q and P→R alone, the P case reaches R but the Q case need not. The assignment P=F,Q=T,R=F makes both available premises true and R false. The absence of the second conditional in our nine-line proof would therefore be a genuine gap.

If you already have ¬P as an additional premise, you can rule out the P alternative by appropriate rules and obtain Q. That is a different proof with an additional premise. It does not justify treating P∨Q as permission to assume Q unconditionally.

When a case leads to a contradiction, the classical package permits explosion to derive the shared target within that case. You still need the other case and the ∨E discharge. A contradiction in one temporary case does not automatically close every open assumption or make the other case unnecessary.

Formal background: [2] [1].

Check scope even when the final argument is valid

A valid argument can be presented with an invalid derivation. For example, using the closed first-case line 6 as an ordinary citation inside the second case would violate accessibility, even though the given outer premises happen to entail R by a correct proof. A semantic table alone would not catch that line-level mistake.

Check each range’s opening assumption, endpoint formula, and nesting level. The two ranges for ∨E are siblings at the current outer context. An endpoint inside an unfinished inner block is not yet the endpoint of the case itself.

After ∨E, cite the exported R rather than an internal case line for later ordinary steps. This keeps subsequent reasoning independent of which disjunct supplied R and makes the proof’s remaining premises clear.

Try six case-proof decisions

Keep case assumptions separate and inspect the exact shared endpoint.