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 set.mm). 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 1 |
nothing | Reiteration is always redundant in Metamath.
Definition "new rule" in [Pfenning] p. 18,
definition IT in [Clemente] p. 10. |
∧I |
Γ⊢ 𝜓 & Γ⊢ 𝜒 => Γ⊢ 𝜓 ∧ 𝜒 |
jca 513 |
jca 513, pm3.2i 472 |
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 496 |
simpld 496, adantr 482 |
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 497 |
simpr 486, adantl 483 |
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 414 | ex 414 |
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 686, imp 408 |
Definition →E in [Pfenning] p. 18,
definition E=>m,n in [Clemente] p. 11, and
definition →E in [Indrzejczak] p. 33. |
∨IL | Γ⊢ 𝜓 =>
Γ⊢ 𝜓 ∨ 𝜒 |
olcd 873 |
olc 867, olci 865, olcd 873 |
Definition ∨I in [Pfenning] p. 18,
definition I∨n(1) in [Clemente] p. 12 |
∨IR | Γ⊢ 𝜒 =>
Γ⊢ 𝜓 ∨ 𝜒 |
orcd 872 |
orc 866, orci 864, orcd 872 |
Definition ∨IR in [Pfenning] p. 18,
definition I∨n(2) in [Clemente] p. 12. |
∨E | Γ⊢ 𝜓 ∨ 𝜒 & Γ, 𝜓⊢ 𝜃 &
Γ, 𝜒⊢ 𝜃 => Γ⊢ 𝜃 |
mpjaodan 958 |
mpjaodan 958, jaodan 957, jaod 858 |
Definition ∨E in [Pfenning] p. 18,
definition E∨m,n,p in [Clemente] p. 12. |
¬I | Γ, 𝜓⊢ ⊥ => Γ⊢ ¬ 𝜓 |
inegd 1562 | pm2.01d 189 |
|
¬I | Γ, 𝜓⊢ 𝜃 & Γ⊢ ¬ 𝜃 =>
Γ⊢ ¬ 𝜓 |
mtand 815 | mtand 815 |
definition I¬m,n,p in [Clemente] p. 13. |
¬I | Γ, 𝜓⊢ 𝜒 & Γ, 𝜓⊢ ¬ 𝜒 =>
Γ⊢ ¬ 𝜓 |
pm2.65da 816 | pm2.65da 816 |
Contradiction. |
¬I |
Γ, 𝜓⊢ ¬ 𝜓 => Γ⊢ ¬ 𝜓 |
pm2.01da 798 | pm2.01d 189, pm2.65da 816, pm2.65d 195 |
For an alternative falsum-free natural deduction ruleset |
¬E |
Γ⊢ 𝜓 & Γ⊢ ¬ 𝜓 => Γ⊢ ⊥ |
pm2.21fal 1564 |
pm2.21dd 194 | |
¬E |
Γ, ¬ 𝜓⊢ ⊥ => Γ⊢ 𝜓 |
|
pm2.21dd 194 |
definition →E in [Indrzejczak] p. 33. |
¬E |
Γ⊢ 𝜓 & Γ⊢ ¬ 𝜓 => Γ⊢ 𝜃 |
pm2.21dd 194 | pm2.21dd 194, pm2.21d 121, pm2.21 123 |
For an alternative falsum-free natural deduction ruleset.
Definition ¬E in [Pfenning] p. 18. |
⊤I | Γ⊢ ⊤ |
trud 1552 | tru 1546, trud 1552, mptru 1549 |
Definition ⊤I in [Pfenning] p. 18. |
⊥E | Γ, ⊥⊢ 𝜃 |
falimd 1560 | falim 1559 |
Definition ⊥E in [Pfenning] p. 18. |
∀I |
Γ⊢ [𝑎 / 𝑥]𝜓 => Γ⊢ ∀𝑥𝜓 |
alrimiv 1931 | alrimiv 1931, ralrimiva 3147 |
Definition ∀Ia in [Pfenning] p. 18,
definition I∀n in [Clemente] p. 32. |
∀E |
Γ⊢ ∀𝑥𝜓 => Γ⊢ [𝑡 / 𝑥]𝜓 |
spsbcd 3792 | spcv 3596, rspcv 3609 |
Definition ∀E in [Pfenning] p. 18,
definition E∀n,t in [Clemente] p. 32. |
∃I |
Γ⊢ [𝑡 / 𝑥]𝜓 => Γ⊢ ∃𝑥𝜓 |
spesbcd 3878 | spcev 3597, rspcev 3613 |
Definition ∃I in [Pfenning] p. 18,
definition I∃n,t in [Clemente] p. 32. |
∃E |
Γ⊢ ∃𝑥𝜓 & Γ, [𝑎 / 𝑥]𝜓⊢ 𝜃 =>
Γ⊢ 𝜃 |
exlimddv 1939 | exlimddv 1939, exlimdd 2214,
exlimdv 1937, rexlimdva 3156 |
Definition ∃Ea,u in [Pfenning] p. 18,
definition E∃m,n,p,a in [Clemente] p. 32. |
⊥C |
Γ, ¬ 𝜓⊢ ⊥ => Γ⊢ 𝜓 |
efald 1563 | efald 1563 |
Proof by contradiction (classical logic),
definition ⊥C in [Pfenning] p. 17. |
⊥C |
Γ, ¬ 𝜓⊢ 𝜓 => Γ⊢ 𝜓 |
pm2.18da 799 | pm2.18da 799, pm2.18d 127, pm2.18 128 |
For an alternative falsum-free natural deduction ruleset |
¬ ¬C |
Γ⊢ ¬ ¬ 𝜓 => Γ⊢ 𝜓 |
notnotrd 133 | notnotrd 133, notnotr 130 |
Double negation rule (classical logic),
definition NNC in [Pfenning] p. 17,
definition E¬n in [Clemente] p. 14. |
EM | Γ⊢ 𝜓 ∨ ¬ 𝜓 |
exmidd 895 | exmid 894 |
Excluded middle (classical logic),
definition XM in [Pfenning] p. 17,
proof 5.11 in [Clemente] p. 14. |
=I | Γ⊢ 𝐴 = 𝐴 |
eqidd 2734 | eqid 2733, eqidd 2734 |
Introduce equality,
definition =I in [Pfenning] p. 127. |
=E | Γ⊢ 𝐴 = 𝐵 & Γ[𝐴 / 𝑥]𝜓 =>
Γ⊢ [𝐵 / 𝑥]𝜓 |
sbceq1dd 3784 | sbceq1d 3783, 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 29657, ex-natded5.3 29660,
ex-natded5.5 29663, ex-natded5.7 29664, ex-natded5.8 29666, ex-natded5.13 29668,
ex-natded9.20 29670, and ex-natded9.26 29672.
(Contributed by DAW, 4-Feb-2017.) (New usage is
discouraged.) |