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

Theorem natded 21711
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 [Clemente] p. 10.
I & => jca 519 jca 519, pm3.2i 442 Definition I in [Pfenning] p. 18, definition Im,n in [Clemente] p. 10, and definition I in [Indrzejczak] p. 34 (representing both Gentzen's system NK and Jaśkowski)
EL => simpld 446 simpld 446, adantr 452 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 => simprd 450 simpr 448, adantl 453 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 => ex 424 ex 424 Definition I in [Pfenning] p. 18, definition I=>m,n in [Clemente] p. 11, and definition I in [Indrzejczak] p. 33.
E & => mpd 15 ax-mp 8, mpd 15, mpdan 650, imp 419 Definition E in [Pfenning] p. 18, definition E=>m,n in [Clemente] p. 11, and definition E in [Indrzejczak] p. 33.
IL => olcd 383 olc 374, olci 381, olcd 383 Definition I in [Pfenning] p. 18, definition In(1) in [Clemente] p. 12
IR => orcd 382 orc 375, orci 380, orcd 382 Definition IR in [Pfenning] p. 18, definition In(2) in [Clemente] p. 12.
E & & => mpjaodan 762 mpjaodan 762, jaodan 761, jaod 370 Definition E in [Pfenning] p. 18, definition Em,n,p in [Clemente] p. 12.
I => inegd 1342 pm2.01d 163
I & => mtand 641 mtand 641 definition Im,n,p in [Clemente] p. 13.
I & => pm2.65da 560 pm2.65da 560 Contradiction.
I => pm2.01da 430 pm2.01d 163, pm2.65da 560, pm2.65d 168 For an alternative falsum-free natural deduction ruleset
E & => pm2.21fal 1344 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 1339 tru 1330, a1tru 1339, trud 1332 Definition I in [Pfenning] p. 18.
E falimd 1338 falim 1337 Definition E in [Pfenning] p. 18.
I => alrimiv 1641 alrimiv 1641, ralrimiva 2789 Definition Ia in [Pfenning] p. 18, definition In in [Clemente] p. 32.
E => spsbcd 3174 spcv 3042, rspcv 3048 Definition E in [Pfenning] p. 18, definition En,t in [Clemente] p. 32.
I => spesbcd 3243 spcev 3043, rspcev 3052 Definition I in [Pfenning] p. 18, definition In,t in [Clemente] p. 32.
E & => exlimddv 1648 exlimddv 1648, exlimdd 1912, exlimdv 1646, rexlimdva 2830 Definition Ea,u in [Pfenning] p. 18, definition Em,n,p,a in [Clemente] p. 32.
C => efald 1343 efald 1343 Proof by contradiction (classical logic), definition C in [Pfenning] p. 17.
C => pm2.18da 431 pm2.18da 431, 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 [Clemente] p. 14.
EM exmidd 406 exmid 405 Excluded middle (classical logic), definition XM in [Pfenning] p. 17, proof 5.11 in [Clemente] p. 14.
I eqidd 2437 eqid 2436, eqidd 2437 Introduce equality, definition =I in [Pfenning] p. 127.
E & => sbceq1dd 3167 sbceq1d 3166, 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 21712, ex-natded5.3 21715, ex-natded5.5 21718, ex-natded5.7 21719, ex-natded5.8 21721, ex-natded5.13 21723, ex-natded9.20 21725, and ex-natded9.26 21727.

(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 This theorem is referenced by:  ftc1anclem8  26287
 Copyright terms: Public domain W3C validator