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

Theorem natded 27603
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 Γ𝜓 => Γ𝜓 idi 2 nothing Reiteration is always redundant in Metamath. Definition "new rule" in [Pfenning] p. 18, definition IT in [Clemente] p. 10.
I Γ𝜓 & Γ𝜒 => Γ𝜓𝜒 jca 497 jca 497, pm3.2i 447 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 478 simpld 478, adantr 466 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 479 simpr 471, adantl 467 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 397 ex 397 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 5, mpd 15, mpdan 661, imp 393 Definition E in [Pfenning] p. 18, definition E=>m,n in [Clemente] p. 11, and definition E in [Indrzejczak] p. 33.
IL Γ𝜓 => Γ𝜓𝜒 olcd 855 olc 849, olci 847, olcd 855 Definition I in [Pfenning] p. 18, definition In(1) in [Clemente] p. 12
IR Γ𝜒 => Γ𝜓𝜒 orcd 854 orc 848, orci 846, orcd 854 Definition IR in [Pfenning] p. 18, definition In(2) in [Clemente] p. 12.
E Γ𝜓𝜒 & Γ, 𝜓𝜃 & Γ, 𝜒𝜃 => Γ𝜃 mpjaodan 933 mpjaodan 933, jaodan 932, jaod 840 Definition E in [Pfenning] p. 18, definition Em,n,p in [Clemente] p. 12.
¬I Γ, 𝜓 => Γ¬ 𝜓 inegd 1651 pm2.01d 181
¬I Γ, 𝜓𝜃 & Γ¬ 𝜃 => Γ¬ 𝜓 mtand 810 mtand 810 definition I¬m,n,p in [Clemente] p. 13.
¬I Γ, 𝜓𝜒 & Γ, 𝜓¬ 𝜒 => Γ¬ 𝜓 pm2.65da 811 pm2.65da 811 Contradiction.
¬I Γ, 𝜓¬ 𝜓 => Γ¬ 𝜓 pm2.01da 794 pm2.01d 181, pm2.65da 811, pm2.65d 187 For an alternative falsum-free natural deduction ruleset
¬E Γ𝜓 & Γ¬ 𝜓 => Γ pm2.21fal 1653 pm2.21dd 186
¬E Γ, ¬ 𝜓 => Γ𝜓 pm2.21dd 186 definition E in [Indrzejczak] p. 33.
¬E Γ𝜓 & Γ¬ 𝜓 => Γ𝜃 pm2.21dd 186 pm2.21dd 186, pm2.21d 119, pm2.21 121 For an alternative falsum-free natural deduction ruleset. Definition ¬E in [Pfenning] p. 18.
I Γ a1tru 1648 tru 1635, a1tru 1648, trud 1641 Definition I in [Pfenning] p. 18.
E Γ, ⊥𝜃 falimd 1647 falim 1646 Definition E in [Pfenning] p. 18.
I Γ[𝑎 / 𝑥]𝜓 => Γ𝑥𝜓 alrimiv 2007 alrimiv 2007, ralrimiva 3115 Definition Ia in [Pfenning] p. 18, definition In in [Clemente] p. 32.
E Γ𝑥𝜓 => Γ[𝑡 / 𝑥]𝜓 spsbcd 3602 spcv 3451, rspcv 3457 Definition E in [Pfenning] p. 18, definition En,t in [Clemente] p. 32.
I Γ[𝑡 / 𝑥]𝜓 => Γ𝑥𝜓 spesbcd 3672 spcev 3452, rspcev 3461 Definition I in [Pfenning] p. 18, definition In,t in [Clemente] p. 32.
E Γ𝑥𝜓 & Γ, [𝑎 / 𝑥]𝜓𝜃 => Γ𝜃 exlimddv 2015 exlimddv 2015, exlimdd 2244, exlimdv 2013, rexlimdva 3179 Definition Ea,u in [Pfenning] p. 18, definition Em,n,p,a in [Clemente] p. 32.
C Γ, ¬ 𝜓 => Γ𝜓 efald 1652 efald 1652 Proof by contradiction (classical logic), definition C in [Pfenning] p. 17.
C Γ, ¬ 𝜓𝜓 => Γ𝜓 pm2.18da 795 pm2.18da 795, pm2.18d 125, pm2.18 123 For an alternative falsum-free natural deduction ruleset
¬ ¬C Γ¬ ¬ 𝜓 => Γ𝜓 notnotrd 130 notnotrd 130, notnotr 128 Double negation rule (classical logic), definition NNC in [Pfenning] p. 17, definition E¬n in [Clemente] p. 14.
EM Γ𝜓 ∨ ¬ 𝜓 exmidd 873 exmid 872 Excluded middle (classical logic), definition XM in [Pfenning] p. 17, proof 5.11 in [Clemente] p. 14.
=I Γ𝐴 = 𝐴 eqidd 2772 eqid 2771, eqidd 2772 Introduce equality, definition =I in [Pfenning] p. 127.
=E Γ𝐴 = 𝐵 & Γ[𝐴 / 𝑥]𝜓 => Γ[𝐵 / 𝑥]𝜓 sbceq1dd 3594 sbceq1d 3593, 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 27604, ex-natded5.3 27607, ex-natded5.5 27610, ex-natded5.7 27611, ex-natded5.8 27613, ex-natded5.13 27615, ex-natded9.20 27617, and ex-natded9.26 27619.

(Contributed by DAW, 4-Feb-2017.) (New usage is discouraged.)

Hypothesis
Ref Expression
natded.1 𝜑
Assertion
Ref Expression
natded 𝜑

Proof of Theorem natded
StepHypRef Expression
1 natded.1 1 𝜑
Colors of variables: wff setvar class
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator