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 514 |
jca 514, pm3.2i 473 |
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 497 |
simpld 497, adantr 483 |
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 498 |
simpr 487, adantl 484 |
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 415 | ex 415 |
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 685, imp 409 |
Definition →E in [Pfenning] p. 18,
definition E=>m,n in [Clemente] p. 11, and
definition →E in [Indrzejczak] p. 33. |
∨IL | Γ⊢ 𝜓 =>
Γ⊢ 𝜓 ∨ 𝜒 |
olcd 870 |
olc 864, olci 862, olcd 870 |
Definition ∨I in [Pfenning] p. 18,
definition I∨n(1) in [Clemente] p. 12 |
∨IR | Γ⊢ 𝜒 =>
Γ⊢ 𝜓 ∨ 𝜒 |
orcd 869 |
orc 863, orci 861, orcd 869 |
Definition ∨IR in [Pfenning] p. 18,
definition I∨n(2) in [Clemente] p. 12. |
∨E | Γ⊢ 𝜓 ∨ 𝜒 & Γ, 𝜓⊢ 𝜃 &
Γ, 𝜒⊢ 𝜃 => Γ⊢ 𝜃 |
mpjaodan 955 |
mpjaodan 955, jaodan 954, jaod 855 |
Definition ∨E in [Pfenning] p. 18,
definition E∨m,n,p in [Clemente] p. 12. |
¬I | Γ, 𝜓⊢ ⊥ => Γ⊢ ¬ 𝜓 |
inegd 1557 | pm2.01d 192 |
|
¬I | Γ, 𝜓⊢ 𝜃 & Γ⊢ ¬ 𝜃 =>
Γ⊢ ¬ 𝜓 |
mtand 814 | mtand 814 |
definition I¬m,n,p in [Clemente] p. 13. |
¬I | Γ, 𝜓⊢ 𝜒 & Γ, 𝜓⊢ ¬ 𝜒 =>
Γ⊢ ¬ 𝜓 |
pm2.65da 815 | pm2.65da 815 |
Contradiction. |
¬I |
Γ, 𝜓⊢ ¬ 𝜓 => Γ⊢ ¬ 𝜓 |
pm2.01da 797 | pm2.01d 192, pm2.65da 815, pm2.65d 198 |
For an alternative falsum-free natural deduction ruleset |
¬E |
Γ⊢ 𝜓 & Γ⊢ ¬ 𝜓 => Γ⊢ ⊥ |
pm2.21fal 1559 |
pm2.21dd 197 | |
¬E |
Γ, ¬ 𝜓⊢ ⊥ => Γ⊢ 𝜓 |
|
pm2.21dd 197 |
definition →E in [Indrzejczak] p. 33. |
¬E |
Γ⊢ 𝜓 & Γ⊢ ¬ 𝜓 => Γ⊢ 𝜃 |
pm2.21dd 197 | pm2.21dd 197, pm2.21d 121, pm2.21 123 |
For an alternative falsum-free natural deduction ruleset.
Definition ¬E in [Pfenning] p. 18. |
⊤I | Γ⊢ ⊤ |
trud 1547 | tru 1541, trud 1547, mptru 1544 |
Definition ⊤I in [Pfenning] p. 18. |
⊥E | Γ, ⊥⊢ 𝜃 |
falimd 1555 | falim 1554 |
Definition ⊥E in [Pfenning] p. 18. |
∀I |
Γ⊢ [𝑎 / 𝑥]𝜓 => Γ⊢ ∀𝑥𝜓 |
alrimiv 1928 | alrimiv 1928, ralrimiva 3182 |
Definition ∀Ia in [Pfenning] p. 18,
definition I∀n in [Clemente] p. 32. |
∀E |
Γ⊢ ∀𝑥𝜓 => Γ⊢ [𝑡 / 𝑥]𝜓 |
spsbcd 3786 | spcv 3606, rspcv 3618 |
Definition ∀E in [Pfenning] p. 18,
definition E∀n,t in [Clemente] p. 32. |
∃I |
Γ⊢ [𝑡 / 𝑥]𝜓 => Γ⊢ ∃𝑥𝜓 |
spesbcd 3866 | spcev 3607, rspcev 3623 |
Definition ∃I in [Pfenning] p. 18,
definition I∃n,t in [Clemente] p. 32. |
∃E |
Γ⊢ ∃𝑥𝜓 & Γ, [𝑎 / 𝑥]𝜓⊢ 𝜃 =>
Γ⊢ 𝜃 |
exlimddv 1936 | exlimddv 1936, exlimdd 2220,
exlimdv 1934, rexlimdva 3284 |
Definition ∃Ea,u in [Pfenning] p. 18,
definition E∃m,n,p,a in [Clemente] p. 32. |
⊥C |
Γ, ¬ 𝜓⊢ ⊥ => Γ⊢ 𝜓 |
efald 1558 | efald 1558 |
Proof by contradiction (classical logic),
definition ⊥C in [Pfenning] p. 17. |
⊥C |
Γ, ¬ 𝜓⊢ 𝜓 => Γ⊢ 𝜓 |
pm2.18da 798 | pm2.18da 798, pm2.18d 127, pm2.18 128 |
For an alternative falsum-free natural deduction ruleset |
¬ ¬C |
Γ⊢ ¬ ¬ 𝜓 => Γ⊢ 𝜓 |
notnotrd 135 | notnotrd 135, notnotr 132 |
Double negation rule (classical logic),
definition NNC in [Pfenning] p. 17,
definition E¬n in [Clemente] p. 14. |
EM | Γ⊢ 𝜓 ∨ ¬ 𝜓 |
exmidd 892 | exmid 891 |
Excluded middle (classical logic),
definition XM in [Pfenning] p. 17,
proof 5.11 in [Clemente] p. 14. |
=I | Γ⊢ 𝐴 = 𝐴 |
eqidd 2822 | eqid 2821, eqidd 2822 |
Introduce equality,
definition =I in [Pfenning] p. 127. |
=E | Γ⊢ 𝐴 = 𝐵 & Γ[𝐴 / 𝑥]𝜓 =>
Γ⊢ [𝐵 / 𝑥]𝜓 |
sbceq1dd 3778 | sbceq1d 3777, 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 28183, ex-natded5.3 28186,
ex-natded5.5 28189, ex-natded5.7 28190, ex-natded5.8 28192, ex-natded5.13 28194,
ex-natded9.20 28196, and ex-natded9.26 28198.
(Contributed by DAW, 4-Feb-2017.) (New usage is
discouraged.) |