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.
Articles by others on the same topic
There are currently no matching articles.