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 [Clemente] 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 [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 447 simpld 447, adantr 453 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 451 simpr 449, adantl 454 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 425 ex 425 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 16 ax-mp 10, mpd 16, mpdan 651, imp 420 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 384 olc 375, olci 382, olcd 384 Definition  \/I in [Pfenning] p. 18, definition I \/n(1) in [Clemente] 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 [Clemente] p. 12.
 \/E  _G |-  ps  \/  ch &  _G ,  ps |-  th &  _G ,  ch |-  th =>  _G |-  th mpjaodan 763 mpjaodan 763, jaodan 762, jaod 371 Definition  \/E in [Pfenning] p. 18, definition E \/m,n,p in [Clemente] p. 12.
 -.I  _G ,  ps |-  F. =>  _G |-  -.  ps inegd 1325 pm2.01d 163
 -.I  _G ,  ps |-  th &  _G |-  -.  th =>  _G |-  -.  ps mtand 642 mtand 642 definition I -.m,n,p in [Clemente] p. 13.
 -.I  _G ,  ps |-  ch &  _G ,  ps |-  -.  ch =>  _G |-  -.  ps pm2.65da 561 pm2.65da 561 Contradiction.
 -.I  _G ,  ps |-  -.  ps =>  _G |-  -.  ps pm2.01da 431 pm2.01d 163, pm2.65da 561, pm2.65d 168 For an alternative falsum-free natural deduction ruleset
 -.E  _G |-  ps &  _G |-  -.  ps =>  _G |-  F. pm2.21fal 1327 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 1323 tru 1314, a1tru 1323, trud 1316 Definition  T.I in [Pfenning] p. 18.
 F.E  _G ,  F.  |-  th falimd 1322 falim 1321 Definition  F.E in [Pfenning] p. 18.
 A.I  _G |-  [ a  /  x ] ps =>  _G |-  A. x ps alrimiv 1619 alrimiv 1619, ralrimiva 2629 Definition  A.Ia in [Pfenning] p. 18, definition I A.n in [Clemente] p. 32.
 A.E  _G |-  A. x ps =>  _G |-  [ t  /  x ] ps spsbcd 3007 spcv 2877, rspcv 2883 Definition  A.E in [Pfenning] p. 18, definition E A.n,t in [Clemente] p. 32.
 E.I  _G |-  [ t  /  x ] ps =>  _G |-  E. x ps spesbcd 3076 spcev 2878, rspcev 2887 Definition  E.I in [Pfenning] p. 18, definition I E.n,t in [Clemente] p. 32.
 E.E  _G |-  E. x ps &  _G ,  [ a  /  x ] ps |-  th =>  _G |-  th exlimddv 1668 exlimddv 1668, exlimdd 1834, exlimdv 1667, rexlimdva 2670 Definition  E.Ea,u in [Pfenning] p. 18, definition E E.m,n,p,a in [Clemente] p. 32.
 F.C  _G ,  -.  ps |-  F. =>  _G |-  ps efald 1326 efald 1326 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 [Clemente] p. 14.
EM  _G |-  ps  \/  -.  ps exmidd 407 exmid 406 Excluded middle (classical logic), definition XM in [Pfenning] p. 17, proof 5.11 in [Clemente] p. 14.
 =I  _G |-  A  =  A eqidd 2287 eqid 2286, eqidd 2287 Introduce equality, definition =I in [Pfenning] p. 127.
 =E  _G |-  A  =  B &  _G [. A  /  x ]. ps =>  _G |-  [. B  /  x ]. ps sbceq1dd 3000 sbceq1d 2999, 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 20813, ex-natded5.3 20816, ex-natded5.5 20819, ex-natded5.7 20820, ex-natded5.8 20822, ex-natded5.13 20824, ex-natded9.20 20826, and ex-natded9.26 20828.

(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