MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  natded Unicode version

Theorem natded 4
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.

NameNatural Deduction RuleTranslation RecommendationComments
IT  _G |-  ps =>  _G |-  ps idi 2 nothing Reiteration is always redundant in Metamath. Definition "new rule" in [Pfenning] p. 18, definition IT in [Laboreo] p. 10.
 /\I  _G |-  ps &  _G |-  ch =>  _G |-  ps  /\  ch jca 520 jca 520, pm3.2i 443 Definition  /\I in [Pfenning] p. 18, definition I /\m,n in [Laboreo] 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 447 simpld 447, adantr 453 Definition  /\EL in [Pfenning] p. 18, definition E /\(1) in [Laboreo] 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 451 simpr 449, adantl 454 Definition  /\ER in [Pfenning] p. 18, definition E /\(2) in [Laboreo] 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 425 ex 425 Definition  ->I in [Pfenning] p. 18, definition I=>m,n in [Laboreo] p. 11, and definition  ->I in [Indrzejczak] p. 33.
 ->E  _G |-  ps  ->  ch &  _G |-  ps =>  _G |-  ch mpd 16 ax-mp 10, mpd 16, mpdan 652, imp 420 Definition  ->E in [Pfenning] p. 18, definition E=>m,n in [Laboreo] p. 11, and definition  ->E in [Indrzejczak] p. 33.
 \/IL  _G |-  ps =>  _G |-  ps  \/  ch olcd 384 olc 375, olci 382, olcd 384 Definition  \/I in [Pfenning] p. 18, definition I \/n(1) in [Laboreo] p. 12
 \/IR  _G |-  ch =>  _G |-  ps  \/  ch orcd 383 orc 376, orci 381, orcd 383 Definition  \/IR in [Pfenning] p. 18, definition I \/n(2) in [Laboreo] p. 12.
 \/E  _G |-  ps  \/  ch &  _G ,  ps |-  th &  _G ,  ch |-  th =>  _G |-  th mpjaodan 764 mpjaodan 764, jaodan 763, jaod 371 Definition  \/E in [Pfenning] p. 18, definition E \/m,n,p in [Laboreo] p. 12.
 -.I  _G ,  ps |-  F. =>  _G |-  -.  ps inegd 1329 pm2.01d 163
 -.I  _G ,  ps |-  th &  _G |-  -.  th =>  _G |-  -.  ps mtand 643 mtand 643 definition I -.m,n,p in [Laboreo] p. 13.
 -.I  _G ,  ps |-  ch &  _G ,  ps |-  -.  ch =>  _G |-  -.  ps pm2.65da 562 pm2.65da 562 Contradiction.
 -.I  _G ,  ps |-  -.  ps =>  _G |-  -.  ps pm2.01da 431 pm2.01d 163, pm2.65da 562, pm2.65d 168 For an alternative falsum-free natural deduction ruleset
 -.E  _G |-  ps &  _G |-  -.  ps =>  _G |-  F. pm2.21fal 1331 pm2.21dd 101
 -.E  _G ,  -.  ps |-  F. =>  _G |-  ps pm2.21dd 101 definition  ->E in [Indrzejczak] p. 33.
 -.E  _G |-  ps &  _G |-  -.  ps =>  _G |-  th pm2.21dd 101 pm2.21dd 101, pm2.21d 100, pm2.21 102 For an alternative falsum-free natural deduction ruleset. Definition  -.E in [Pfenning] p. 18.
 T.I  _G |-  T. a1tru 1327 tru 1317, a1tru 1327, trud 1320 Definition  T.I in [Pfenning] p. 18.
 F.E  _G ,  F.  |-  th falimd 1326 falim 1325 Definition  F.E in [Pfenning] p. 18.
 A.I  _G |-  [ a  /  x ] ps =>  _G |-  A. x ps alrimiv 2013 alrimiv 2013, ralrimiva 2597 Definition  A.Ia in [Pfenning] p. 18, definition I A.n in [Laboreo] p. 32.
 A.E  _G |-  A. x ps =>  _G |-  [ t  /  x ] ps a4sbcd 2948 cla4v 2825, rcla4v 2831 Definition  A.E in [Pfenning] p. 18, definition E A.n,t in [Laboreo] p. 32.
 E.I  _G |-  [ t  /  x ] ps =>  _G |-  E. x ps a4esbcd 3017 cla4ev 2826, rcla4ev 2835 Definition  E.I in [Pfenning] p. 18, definition I E.n,t in [Laboreo] p. 32.
 E.E  _G |-  E. x ps &  _G ,  [ a  /  x ] ps |-  th =>  _G |-  th exlimddv 1935 exlimddv 1935, exlimdd 1934, exlimdv 1933, rexlimdva 2638 Definition  E.Ea,u in [Pfenning] p. 18, definition E E.m,n,p,a in [Laboreo] p. 32.
 F.C  _G ,  -.  ps |-  F. =>  _G |-  ps efald 1330 efald 1330 Proof by contradiction (classical logic), definition  F.C in [Pfenning] p. 17.
 F.C  _G ,  -.  ps |-  ps =>  _G |-  ps pm2.18da 432 pm2.18da 432, pm2.18d 105, pm2.18 104 For an alternative falsum-free natural deduction ruleset
 -.  -.C  _G |-  -.  -.  ps =>  _G |-  ps notnotrd 107 notnotrd 107, notnot2 106 Double negation rule (classical logic), definition NNC in [Pfenning] p. 17, definition E -.n in [Laboreo] p. 14.
EM  _G |-  ps  \/  -.  ps exmidd 407 exmid 406 Excluded middle (classical logic), definition XM in [Pfenning] p. 17, proof 5.11 in [Laboreo] p. 14.
 =I  _G |-  A  =  A eqidd 2257 eqid 2256, eqidd 2257 Introduce equality, definition =I in [Pfenning] p. 127.
 =E  _G |-  A  =  B &  _G [. A  /  x ]. ps =>  _G |-  [. B  /  x ]. ps sbceq1dd 2941 sbceq1d 2940, 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 20744, ex-natded5.3 20747, ex-natded5.5 20750, ex-natded5.7 20751, ex-natded5.8 20753, ex-natded5.13 20755, ex-natded9.20 20757, and ex-natded9.26 20759.

(Contributed by DAW, 4-Feb-2017.)

Hypothesis
Ref Expression
natded.1  |-  ph
Assertion
Ref Expression
natded  |-  ph

Proof of Theorem natded
StepHypRef Expression
1 natded.1 1  |-  ph
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator