Use only the displayed natural deduction rules. Let abbreviate . Indentation below marks temporary assumptions; the closing rule names the assumption discharged.
1 | ¬A assume
2 | | φ assume
3 | | A ∨-intro-L, 2
4 | | ⊥ ¬-elim, 3 and 1
5 | ¬φ ¬-intro, discharge 2–4
6 | A ∨-intro-R, 5
7 | ⊥ ¬-elim, 6 and 1
8 ¬¬A ¬-intro, discharge 1–7
9 A ¬¬-elim, 8There are no undischarged assumptions at line 9, so this proves the law of excluded middle. The use of double-negation elimination is explicit; an unproved appeal to the derived RAA rule is unnecessary.
Apply the complete logical derivation of the law of excluded middle in (a) to , obtaining . Then use the disjunction elimination rule, constructing each logical implication by an explicit hypothetical subproof:
1 Q ∨ ¬Q result of (a), φ := Q
2 | Q first case
3 | | P assume
4 | | Q available from 2
5 | P → Q →-intro, discharge 3–4
6 | (P → Q) ∨ (P → ¬Q) ∨-intro-L, 5
7 | ¬Q second case
8 | | P assume
9 | | ¬Q available from 7
10 | P → ¬Q →-intro, discharge 8–9
11 | (P → Q) ∨ (P → ¬Q) ∨-intro-R, 10
12 (P → Q) ∨ (P → ¬Q) ∨-elim, 1, cases 2–6 and 7–11Both case assumptions and both hypothetical assumptions have been discharged. Thus the conclusion is a theorem, not a logical implication that depends on assuming .
Retain the two given logical implications and temporarily assume their common starting proposition.
1 P → Q premise
2 Q → R premise
3 | P assume
4 | Q →-elim, 3 and 1
5 | R →-elim, 4 and 2
6 P → R →-intro, discharge 3–5Only the original premises remain undischarged, giving the required composition of logical implications.
The logical implication associates to the right. Assume its two antecedents, then use nested applications of the disjunction elimination rule.
1 | P ∨ Q assume
2 | | P ∨ ¬Q assume
3 | | | P first case of 1
4 | | | P available from 3
5 | | | Q second case of 1
6 | | | | P first case of 2
7 | | | | P available from 6
8 | | | | ¬Q second case of 2
9 | | | | ⊥ ¬-elim, 5 and 8
10 | | | | P ⊥-elim, 9
11 | | | P ∨-elim, 2, cases 6–7 and 8–10
12 | | P ∨-elim, 1, cases 3–4 and 5–11
13 | (P ∨ ¬Q) → P →-intro, discharge 2–12
14 (P ∨ Q) → ((P ∨ ¬Q) → P) →-intro, discharge 1–13This proof uses logical falsity elimination rule, but does not need law of excluded middle or double-negation elimination.
For implication creation rule, keep available and discharge an otherwise unused antecedent:
1 ψ given
2 | φ assume
3 | ψ available from 1
4 φ → ψ →-intro, discharge 2–3For implication distribution rule, write . The logical derivation below keeps available and discharges exactly the two temporary assumptions:
1 φ → (ψ → ρ) given
2 | φ → ψ assume
3 | | φ assume
4 | | ψ →-elim, 3 and 2
5 | | ψ → ρ →-elim, 3 and 1
6 | | ρ →-elim, 4 and 5
7 | φ → ρ →-intro, discharge 3–6
8 (φ → ψ) → (φ → ρ) →-intro, discharge 2–7These justify both derived inference rules using Figure 2 primitives. Their rule forms retain any other surrounding assumptions; they are not unconditionally asserted conclusions after the displayed numerator is forgotten.
Use the two derived inference rules whose complete proofs were supplied in (d). The following logical derivation has no nested hypothetical subproofs:
1 P → Q premise
2 Q → R premise
3 P → (Q → R) → creation from 2
4 (P → Q) → (P → R) → distribution from 3
5 P → R →-elim, 1 and 4The creation instance takes and . The distribution instance takes . The metarules are justified in (d); this requested flat use does not secretly invoke implication introduction rule in one of its own lines.
Articles by others on the same topic
There are currently no matching articles.