Implication introduction assumes temporarily, derives , and discharges that assumption to conclude . Disjunction elimination starts from and derives the same conclusion in two separate branches, one assuming and the other assuming .
The boxes delimit subproofs: a locally assumed formula is available inside its box but cannot be used unconditionally outside it. Discharging a box records exactly which dependency has been removed. The proofs below use a vertical bar to mark each active box.
Apply negation introduction separately to the two disjuncts, then conjunction introduction:No assumption from either branch remains open in the conclusion apart from the original premise.
1 ¬(E ∨ F) premise
2 | E assumption
3 | E ∨ F ∨-intro-L 2
4 | ⊥ ¬-elim 3,1
5 ¬E ¬-intro 2–4
6 | F assumption
7 | E ∨ F ∨-intro-R 6
8 | ⊥ ¬-elim 7,1
9 ¬F ¬-intro 6–8
10 ¬E ∧ ¬F ∧-intro 5,9The derived proof by contradiction rule iswhere the displayed assumption is discharged. Replace each use by negation introduction, giving , followed by double-negation elimination, giving . Applying this replacement recursively removes all RAA occurrences while preserving the final conclusion and open premises. This uses the classical double-negation rule already supplied in the paper; it is not a general derivation of classical RAA from intuitionistic rules alone.
A derivation of the law of excluded middle using only the supplied primitive rules isBoth boxes have been discharged, so the final formula has no undischarged assumptions.
1 | ¬(A ∨ ¬A) assumption
2 | | A assumption
3 | | A ∨ ¬A ∨-intro-L 2
4 | | ⊥ ¬-elim 3,1
5 | ¬A ¬-intro 2–4
6 | A ∨ ¬A ∨-intro-R 5
7 | ⊥ ¬-elim 6,1
8 ¬¬(A ∨ ¬A) ¬-intro 1–7
9 A ∨ ¬A ¬¬-elim 8Split on the law of excluded middle for , then use disjunction elimination:The two occurrences of have identical type and depend only on the corresponding temporary branch assumption and the original premises.
1 D ∧ E premise
2 (A ∧ D) → B premise
3 (¬A ∧ E) → B premise
4 D ∧-elim-L 1
5 E ∧-elim-R 1
6 A ∨ ¬A excluded middle
7 | A assumption
8 | A ∧ D ∧-intro 7,4
9 | B →-elim 2,8
10 | ¬A assumption
11 | ¬A ∧ E ∧-intro 10,5
12 | B →-elim 3,11
13 B ∨-elim 6,7–9,10–12Now derive the needed or inside its respective subproof:Implication elimination supplies the branch-specific premise before conjunction introduction packages it for the final implication.
1 A → D premise
2 ¬A → E premise
3 (A ∧ D) → B premise
4 (¬A ∧ E) → B premise
5 A ∨ ¬A excluded middle
6 | A assumption
7 | D →-elim 1,6
8 | A ∧ D ∧-intro 6,7
9 | B →-elim 3,8
10 | ¬A assumption
11 | E →-elim 2,10
12 | ¬A ∧ E ∧-intro 10,11
13 | B →-elim 4,12
14 B ∨-elim 5,6–9,10–13 Articles by others on the same topic
There are currently no matching articles.