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.

IT => idi 2 nothing Reiteration is always redundant in Metamath. Definition "new rule" in [Pfenning] p. 18, definition IT in [Laboreo] p. 10.
I & => jca 520 jca 520, pm3.2i 443 Definition I in [Pfenning] p. 18, definition Im,n in [Laboreo] p. 10, and definition I in [Indrzejczak] p. 34 (representing both Gentzen's system NK and Jaśkowski)
EL => 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 => 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 => 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 & => 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 => olcd 384 olc 375, olci 382, olcd 384 Definition I in [Pfenning] p. 18, definition In(1) in [Laboreo] p. 12
IR => orcd 383 orc 376, orci 381, orcd 383 Definition IR in [Pfenning] p. 18, definition In(2) in [Laboreo] p. 12.
E & & => mpjaodan 764 mpjaodan 764, jaodan 763, jaod 371 Definition E in [Pfenning] p. 18, definition Em,n,p in [Laboreo] p. 12.
I => inegd 1329 pm2.01d 163
I & => mtand 643 mtand 643 definition Im,n,p in [Laboreo] p. 13.
I & => pm2.65da 562 pm2.65da 562 Contradiction.
I => pm2.01da 431 pm2.01d 163, pm2.65da 562, pm2.65d 168 For an alternative falsum-free natural deduction ruleset
E & => pm2.21fal 1331 pm2.21dd 101
E => pm2.21dd 101 definition E in [Indrzejczak] p. 33.
E & => 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.
I a1tru 1327 tru 1317, a1tru 1327, trud 1320 Definition I in [Pfenning] p. 18.
E falimd 1326 falim 1325 Definition E in [Pfenning] p. 18.
I => alrimiv 2012 alrimiv 2012, ralrimiva 2588 Definition Ia in [Pfenning] p. 18, definition In in [Laboreo] p. 32.
E => a4sbcd 2934 cla4v 2811, rcla4v 2817 Definition E in [Pfenning] p. 18, definition En,t in [Laboreo] p. 32.
I => a4esbcd 3003 cla4ev 2812, rcla4ev 2821 Definition I in [Pfenning] p. 18, definition In,t in [Laboreo] p. 32.
E & => exlimddv 1934 exlimddv 1934, exlimdd 1933, exlimdv 1932, rexlimdva 2629 Definition Ea,u in [Pfenning] p. 18, definition Em,n,p,a in [Laboreo] p. 32.
C => efald 1330 efald 1330 Proof by contradiction (classical logic), definition C in [Pfenning] p. 17.
C => pm2.18da 432 pm2.18da 432, pm2.18d 105, pm2.18 104 For an alternative falsum-free natural deduction ruleset
C => notnotrd 107 notnotrd 107, notnot2 106 Double negation rule (classical logic), definition NNC in [Pfenning] p. 17, definition En in [Laboreo] p. 14.
EM exmidd 407 exmid 406 Excluded middle (classical logic), definition XM in [Pfenning] p. 17, proof 5.11 in [Laboreo] p. 14.
I eqidd 2254 eqid 2253, eqidd 2254 Introduce equality, definition =I in [Pfenning] p. 127.
E & => sbceq1dd 2927 sbceq1d 2926, 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 represents the set of (current) hypotheses. We use wff variable names beginning with to provide a closer representation of the Metamath equivalents (which typically use the antedent to represent the context ).

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 20649, ex-natded5.3 20652, ex-natded5.5 20655, ex-natded5.7 20656, ex-natded5.8 20658, ex-natded5.13 20660, ex-natded9.20 20662, and ex-natded9.26 20664.

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

Hypothesis
Ref Expression
natded.1
Assertion
Ref Expression
natded

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