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 | _G |- ps => _G |- ps | idi | nothing | Reiteration is always redundant in Metamath. Definition "new rule" in Pfenning p. 18, definition IT in Clemente p. 10. |
| /\I | _G |- ps & _G |- ch => _G |- ps /\ ch | jca | jca , pm3.2i | 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 | _G |- ps /\ ch => _G |- ps | simpld | simpld , adantr | 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 | _G |- ps /\ ch => _G |- ch | simprd | simpr , adantl | 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 | _G , ps |- ch => _G |- ps -> ch | ex | ex | Definition ->I in Pfenning p. 18, definition I=>m,n in Clemente p. 11, and definition ->I in Indrzejczak p. 33. |
| ->E | _G |- ps -> ch & _G |- ps => _G |- ch | mpd | ax-mp , mpd , mpdan , imp | Definition ->E in Pfenning p. 18, definition E=>m,n in Clemente p. 11, and definition ->E in Indrzejczak p. 33. |
| \/IL | _G |- ps => _G |- ps \/ ch | olcd | olc , olci , olcd | Definition \/I in Pfenning p. 18, definition I\/n(1) in Clemente p. 12 |
| \/IR | _G |- ch => _G |- ps \/ ch | orcd | orc , orci , orcd | Definition \/IR in Pfenning p. 18, definition I\/n(2) in Clemente p. 12. |
| \/E | _G |- ps \/ ch & _G , ps |- th & _G , ch |- th => _G |- th | mpjaodan | mpjaodan , jaodan , jaod | Definition \/E in Pfenning p. 18, definition E\/m,n,p in Clemente p. 12. |
| -.I | _G , ps |- F. => _G |- -. ps | inegd | pm2.01d | |
| -.I | _G , ps |- th & _G |- -. th => _G |- -. ps | mtand | mtand | definition I-.m,n,p in Clemente p. 13. |
| -.I | _G , ps |- ch & _G , ps |- -. ch => _G |- -. ps | pm2.65da | pm2.65da | Contradiction. |
| -.I | _G , ps |- -. ps => _G |- -. ps | pm2.01da | pm2.01d , pm2.65da , pm2.65d | For an alternative falsum-free natural deduction ruleset |
| -.E | _G |- ps & _G |- -. ps => _G |- F. | pm2.21fal | pm2.21dd | |
| -.E | _G , -. ps |- F. => _G |- ps | pm2.21dd | definition ->E in Indrzejczak p. 33. | |
| -.E | _G |- ps & _G |- -. ps => _G |- th | pm2.21dd | pm2.21dd , pm2.21d , pm2.21 | For an alternative falsum-free natural deduction ruleset. Definition -.E in Pfenning p. 18. |
| T.I | _G |- T. | trud | tru , trud , mptru | Definition T.I in Pfenning p. 18. |
| F.E | _G , F. |- th | falimd | falim | Definition F.E in Pfenning p. 18. |
| A.I | _G |- [ a / x ] ps => _G |- A. x ps | alrimiv | alrimiv , ralrimiva | Definition A.Ia in Pfenning p. 18, definition IA.n in Clemente p. 32. |
| A.E | _G |- A. x ps => _G |- [ t / x ] ps | spsbcd | spcv , rspcv | Definition A.E in Pfenning p. 18, definition EA.n,t in Clemente p. 32. |
| E.I | _G |- [ t / x ] ps => _G |- E. x ps | spesbcd | spcev , rspcev | Definition E.I in Pfenning p. 18, definition IE.n,t in Clemente p. 32. |
| E.E | _G |- E. x ps & _G , [ a / x ] ps |- th => _G |- th | exlimddv | exlimddv , exlimdd , exlimdv , rexlimdva | Definition E.Ea,u in Pfenning p. 18, definition EE.m,n,p,a in Clemente p. 32. |
| F.C | _G , -. ps |- F. => _G |- ps | efald | efald | Proof by contradiction (classical logic), definition F.C in Pfenning p. 17. |
| F.C | _G , -. ps |- ps => _G |- ps | pm2.18da | pm2.18da , pm2.18d , pm2.18 | For an alternative falsum-free natural deduction ruleset |
| -. -.C | _G |- -. -. ps => _G |- ps | notnotrd | notnotrd , notnotr | Double negation rule (classical logic), definition NNC in Pfenning p. 17, definition E-.n in Clemente p. 14. |
| EM | _G |- ps \/ -. ps | exmidd | exmid | Excluded middle (classical logic), definition XM in Pfenning p. 17, proof 5.11 in Clemente p. 14. |
| =I | _G |- A = A | eqidd | eqid , eqidd | Introduce equality, definition =I in Pfenning p. 127. |
| =E | _G |- A = B & _G [. A / x ]. ps => _G |- [. B / x ]. ps | sbceq1dd | sbceq1d , 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 _G represents the set of (current) hypotheses. We use wff variable names beginning with ps to provide a closer representation of the Metamath equivalents (which typically use the antedent ph to represent the context _G ).
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 , ex-natded5.3 , ex-natded5.5 , ex-natded5.7 , ex-natded5.8 , ex-natded5.13 , ex-natded9.20 , and ex-natded9.26 .
(Contributed by DAW, 4-Feb-2017) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | natded.1 | |- ph |
|
| Assertion | natded | |- ph |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | natded.1 | |- ph |