Metamath Proof Explorer


Theorem natded

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.

NameNatural Deduction RuleTranslation RecommendationComments
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

Proof

Step Hyp Ref Expression
1 natded.1
 |-  ph