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

Theorem natded 20806
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 518 jca 518, pm3.2i 441 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 445 simpld 445, adantr 451 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 449 simpr 447, adantl 452 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 423 ex 423 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 14 ax-mp 8, mpd 14, mpdan 649, imp 418 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 382 olc 373, olci 380, olcd 382 Definition  \/I in [Pfenning] p. 18, definition I \/n(1) in [Clemente] p. 12
 \/IR  _G |-  ch =>  _G |-  ps  \/  ch orcd 381 orc 374, orci 379, orcd 381 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 761 mpjaodan 761, jaodan 760, jaod 369 Definition  \/E in [Pfenning] p. 18, definition E \/m,n,p in [Clemente] p. 12.
 -.I  _G ,  ps |-  F. =>  _G |-  -.  ps inegd 1323 pm2.01d 161
 -.I  _G ,  ps |-  th &  _G |-  -.  th =>  _G |-  -.  ps mtand 640 mtand 640 definition I -.m,n,p in [Clemente] p. 13.
 -.I  _G ,  ps |-  ch &  _G ,  ps |-  -.  ch =>  _G |-  -.  ps pm2.65da 559 pm2.65da 559 Contradiction.
 -.I  _G ,  ps |-  -.  ps =>  _G |-  -.  ps pm2.01da 429 pm2.01d 161, pm2.65da 559, pm2.65d 166 For an alternative falsum-free natural deduction ruleset
 -.E  _G |-  ps &  _G |-  -.  ps =>  _G |-  F. pm2.21fal 1325 pm2.21dd 99
 -.E  _G ,  -.  ps |-  F. =>  _G |-  ps pm2.21dd 99 definition  ->E in [Indrzejczak] p. 33.
 -.E  _G |-  ps &  _G |-  -.  ps =>  _G |-  th pm2.21dd 99 pm2.21dd 99, pm2.21d 98, pm2.21 100 For an alternative falsum-free natural deduction ruleset. Definition  -.E in [Pfenning] p. 18.
 T.I  _G |-  T. a1tru 1321 tru 1312, a1tru 1321, trud 1314 Definition  T.I in [Pfenning] p. 18.
 F.E  _G ,  F.  |-  th falimd 1320 falim 1319 Definition  F.E in [Pfenning] p. 18.
 A.I  _G |-  [ a  /  x ] ps =>  _G |-  A. x ps alrimiv 1621 alrimiv 1621, ralrimiva 2639 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 3017 spcv 2887, rspcv 2893 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 3086 spcev 2888, rspcev 2897 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 1628 exlimddv 1628, exlimdd 1842, exlimdv 1626, rexlimdva 2680 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 1324 efald 1324 Proof by contradiction (classical logic), definition  F.C in [Pfenning] p. 17.
 F.C  _G ,  -.  ps |-  ps =>  _G |-  ps pm2.18da 430 pm2.18da 430, pm2.18d 103, pm2.18 102 For an alternative falsum-free natural deduction ruleset
 -.  -.C  _G |-  -.  -.  ps =>  _G |-  ps notnotrd 105 notnotrd 105, notnot2 104 Double negation rule (classical logic), definition NNC in [Pfenning] p. 17, definition E -.n in [Clemente] p. 14.
EM  _G |-  ps  \/  -.  ps exmidd 405 exmid 404 Excluded middle (classical logic), definition XM in [Pfenning] p. 17, proof 5.11 in [Clemente] p. 14.
 =I  _G |-  A  =  A eqidd 2297 eqid 2296, eqidd 2297 Introduce equality, definition =I in [Pfenning] p. 127.
 =E  _G |-  A  =  B &  _G [. A  /  x ]. ps =>  _G |-  [. B  /  x ]. ps sbceq1dd 3010 sbceq1d 3009, 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 20807, ex-natded5.3 20810, ex-natded5.5 20813, ex-natded5.7 20814, ex-natded5.8 20816, ex-natded5.13 20818, ex-natded9.20 20820, and ex-natded9.26 20822.

(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