Description:
Here are typical natural deduction (ND) rules in the style of Gentzen
and Jaśkowski, along with MPE translations of them. This also
shows the recommended theorems when you find yourself needing these
rules (the recommendations encourage a slightly different proof style
that works more naturally with metamath). A decent list of the standard
rules of natural deduction can be found beginning with definition /\I in
[Pfenning] p. 18. For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer. Many more citations could be added.
Name | Natural Deduction Rule | Translation |
Recommendation | Comments |
IT |
Γ⊢ 𝜓 => Γ⊢ 𝜓 |
idi 2 |
nothing | Reiteration is always redundant in Metamath.
Definition "new rule" in [Pfenning] p. 18,
definition IT in [Clemente] p. 10. |
∧I |
Γ⊢ 𝜓 & Γ⊢ 𝜒 => Γ⊢ 𝜓 ∧ 𝜒 |
jca 553 |
jca 553, pm3.2i 470 |
Definition ∧I in [Pfenning] p. 18,
definition I∧m,n in [Clemente] p. 10, and
definition ∧I in [Indrzejczak] p. 34
(representing both Gentzen's system NK and Jaśkowski) |
∧EL |
Γ⊢ 𝜓 ∧ 𝜒 => Γ⊢ 𝜓 |
simpld 474 |
simpld 474, adantr 480 |
Definition ∧EL in [Pfenning] p. 18,
definition E∧(1) in [Clemente] p. 11, and
definition ∧E in [Indrzejczak] p. 34
(representing both Gentzen's system NK and Jaśkowski) |
∧ER |
Γ⊢ 𝜓 ∧ 𝜒 => Γ⊢ 𝜒 |
simprd 478 |
simpr 476, adantl 481 |
Definition ∧ER in [Pfenning] p. 18,
definition E∧(2) in [Clemente] p. 11, and
definition ∧E in [Indrzejczak] p. 34
(representing both Gentzen's system NK and Jaśkowski) |
→I |
Γ, 𝜓⊢ 𝜒 => Γ⊢ 𝜓 → 𝜒 |
ex 449 | ex 449 |
Definition →I in [Pfenning] p. 18,
definition I=>m,n in [Clemente] p. 11, and
definition →I in [Indrzejczak] p. 33. |
→E |
Γ⊢ 𝜓 → 𝜒 & Γ⊢ 𝜓 => Γ⊢ 𝜒 |
mpd 15 | ax-mp 5, mpd 15, mpdan 699, imp 444 |
Definition →E in [Pfenning] p. 18,
definition E=>m,n in [Clemente] p. 11, and
definition →E in [Indrzejczak] p. 33. |
∨IL | Γ⊢ 𝜓 =>
Γ⊢ 𝜓 ∨ 𝜒 |
olcd 407 |
olc 398, olci 405, olcd 407 |
Definition ∨I in [Pfenning] p. 18,
definition I∨n(1) in [Clemente] p. 12 |
∨IR | Γ⊢ 𝜒 =>
Γ⊢ 𝜓 ∨ 𝜒 |
orcd 406 |
orc 399, orci 404, orcd 406 |
Definition ∨IR in [Pfenning] p. 18,
definition I∨n(2) in [Clemente] p. 12. |
∨E | Γ⊢ 𝜓 ∨ 𝜒 & Γ, 𝜓⊢ 𝜃 &
Γ, 𝜒⊢ 𝜃 => Γ⊢ 𝜃 |
mpjaodan 823 |
mpjaodan 823, jaodan 822, jaod 394 |
Definition ∨E in [Pfenning] p. 18,
definition E∨m,n,p in [Clemente] p. 12. |
¬I | Γ, 𝜓⊢ ⊥ => Γ⊢ ¬ 𝜓 |
inegd 1494 | pm2.01d 180 |
|
¬I | Γ, 𝜓⊢ 𝜃 & Γ⊢ ¬ 𝜃 =>
Γ⊢ ¬ 𝜓 |
mtand 689 | mtand 689 |
definition I¬m,n,p in [Clemente] p. 13. |
¬I | Γ, 𝜓⊢ 𝜒 & Γ, 𝜓⊢ ¬ 𝜒 =>
Γ⊢ ¬ 𝜓 |
pm2.65da 598 | pm2.65da 598 |
Contradiction. |
¬I |
Γ, 𝜓⊢ ¬ 𝜓 => Γ⊢ ¬ 𝜓 |
pm2.01da 457 | pm2.01d 180, pm2.65da 598, pm2.65d 186 |
For an alternative falsum-free natural deduction ruleset |
¬E |
Γ⊢ 𝜓 & Γ⊢ ¬ 𝜓 => Γ⊢ ⊥ |
pm2.21fal 1496 |
pm2.21dd 185 | |
¬E |
Γ, ¬ 𝜓⊢ ⊥ => Γ⊢ 𝜓 |
|
pm2.21dd 185 |
definition →E in [Indrzejczak] p. 33. |
¬E |
Γ⊢ 𝜓 & Γ⊢ ¬ 𝜓 => Γ⊢ 𝜃 |
pm2.21dd 185 | pm2.21dd 185, pm2.21d 117, pm2.21 119 |
For an alternative falsum-free natural deduction ruleset.
Definition ¬E in [Pfenning] p. 18. |
⊤I | Γ⊢ ⊤ |
a1tru 1491 | tru 1479, a1tru 1491, trud 1484 |
Definition ⊤I in [Pfenning] p. 18. |
⊥E | Γ, ⊥⊢ 𝜃 |
falimd 1490 | falim 1489 |
Definition ⊥E in [Pfenning] p. 18. |
∀I |
Γ⊢ [𝑎 / 𝑥]𝜓 => Γ⊢ ∀𝑥𝜓 |
alrimiv 1842 | alrimiv 1842, ralrimiva 2949 |
Definition ∀Ia in [Pfenning] p. 18,
definition I∀n in [Clemente] p. 32. |
∀E |
Γ⊢ ∀𝑥𝜓 => Γ⊢ [𝑡 / 𝑥]𝜓 |
spsbcd 3416 | spcv 3272, rspcv 3278 |
Definition ∀E in [Pfenning] p. 18,
definition E∀n,t in [Clemente] p. 32. |
∃I |
Γ⊢ [𝑡 / 𝑥]𝜓 => Γ⊢ ∃𝑥𝜓 |
spesbcd 3488 | spcev 3273, rspcev 3282 |
Definition ∃I in [Pfenning] p. 18,
definition I∃n,t in [Clemente] p. 32. |
∃E |
Γ⊢ ∃𝑥𝜓 & Γ, [𝑎 / 𝑥]𝜓⊢ 𝜃 =>
Γ⊢ 𝜃 |
exlimddv 1850 | exlimddv 1850, exlimdd 2075,
exlimdv 1848, rexlimdva 3013 |
Definition ∃Ea,u in [Pfenning] p. 18,
definition E∃m,n,p,a in [Clemente] p. 32. |
⊥C |
Γ, ¬ 𝜓⊢ ⊥ => Γ⊢ 𝜓 |
efald 1495 | efald 1495 |
Proof by contradiction (classical logic),
definition ⊥C in [Pfenning] p. 17. |
⊥C |
Γ, ¬ 𝜓⊢ 𝜓 => Γ⊢ 𝜓 |
pm2.18da 458 | pm2.18da 458, pm2.18d 123, pm2.18 121 |
For an alternative falsum-free natural deduction ruleset |
¬ ¬C |
Γ⊢ ¬ ¬ 𝜓 => Γ⊢ 𝜓 |
notnotrd 127 | notnotrd 127, notnotr 124 |
Double negation rule (classical logic),
definition NNC in [Pfenning] p. 17,
definition E¬n in [Clemente] p. 14. |
EM | Γ⊢ 𝜓 ∨ ¬ 𝜓 |
exmidd 431 | exmid 430 |
Excluded middle (classical logic),
definition XM in [Pfenning] p. 17,
proof 5.11 in [Clemente] p. 14. |
=I | Γ⊢ 𝐴 = 𝐴 |
eqidd 2611 | eqid 2610, eqidd 2611 |
Introduce equality,
definition =I in [Pfenning] p. 127. |
=E | Γ⊢ 𝐴 = 𝐵 & Γ[𝐴 / 𝑥]𝜓 =>
Γ⊢ [𝐵 / 𝑥]𝜓 |
sbceq1dd 3408 | sbceq1d 3407, equality theorems |
Eliminate equality,
definition =E in [Pfenning] p. 127. (Both E1 and E2.) |
Note that MPE uses classical logic, not intuitionist logic. As is
conventional, the "I" rules are introduction rules, "E" rules are
elimination rules, the "C" rules are conversion rules, and Γ
represents the set of (current) hypotheses. We use wff variable names
beginning with 𝜓 to provide a closer representation
of the Metamath
equivalents (which typically use the antedent 𝜑 to represent the
context Γ).
Most of this information was developed by Mario Carneiro and posted on
3-Feb-2017. For more information, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
For annotated examples where some traditional ND rules
are directly applied in MPE, see ex-natded5.2 26653, ex-natded5.3 26656,
ex-natded5.5 26659, ex-natded5.7 26660, ex-natded5.8 26662, ex-natded5.13 26664,
ex-natded9.20 26666, and ex-natded9.26 26668.
(Contributed by DAW, 4-Feb-2017.) (New usage is
discouraged.) |