Expand three cases as two applications of disjunction elimination rule. For the association , the first outer branch assumes and applies the given and subproofs to obtain . The other outer branch is the given subproof. In schematic natural deduction form:
1 (φ ∨ ψ) ∨ ρ given
2 | φ ∨ ψ first outer case
3 | | φ first inner case
4 | | κ given φ-subproof
5 | | ψ second inner case
6 | | κ given ψ-subproof
7 | κ ∨-elim, 2, cases 3–4 and 5–6
8 | ρ second outer case
9 | κ given ρ-subproof
10 κ ∨-elim, 1, cases 2–7 and 8–9All three case assumptions are discharged and common surrounding assumptions remain. If the original three-way logical disjunction is parsed as , use the subproof as the first outer branch and eliminate inside the second. Thus either binary association has the asserted three-case disjunction elimination, without presupposing an unproved associativity.
Articles by others on the same topic
There are currently no matching articles.