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

Theorem natded 27108
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 554 jca 554, pm3.2i 471 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 475 simpld 475, adantr 481 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 477, adantl 482 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 450 ex 450 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 701, imp 445 Definition E in [Pfenning] p. 18, definition E=>m,n in [Clemente] p. 11, and definition E in [Indrzejczak] p. 33.
IL Γ𝜓 => Γ𝜓𝜒 olcd 408 olc 399, olci 406, olcd 408 Definition I in [Pfenning] p. 18, definition In(1) in [Clemente] p. 12
IR Γ𝜒 => Γ𝜓𝜒 orcd 407 orc 400, orci 405, orcd 407 Definition IR in [Pfenning] p. 18, definition In(2) in [Clemente] p. 12.
E Γ𝜓𝜒 & Γ, 𝜓𝜃 & Γ, 𝜒𝜃 => Γ𝜃 mpjaodan 826 mpjaodan 826, jaodan 825, jaod 395 Definition E in [Pfenning] p. 18, definition Em,n,p in [Clemente] p. 12.
¬I Γ, 𝜓 => Γ¬ 𝜓 inegd 1500 pm2.01d 181
¬I Γ, 𝜓𝜃 & Γ¬ 𝜃 => Γ¬ 𝜓 mtand 690 mtand 690 definition I¬m,n,p in [Clemente] p. 13.
¬I Γ, 𝜓𝜒 & Γ, 𝜓¬ 𝜒 => Γ¬ 𝜓 pm2.65da 599 pm2.65da 599 Contradiction.
¬I Γ, 𝜓¬ 𝜓 => Γ¬ 𝜓 pm2.01da 458 pm2.01d 181, pm2.65da 599, pm2.65d 187 For an alternative falsum-free natural deduction ruleset
¬E Γ𝜓 & Γ¬ 𝜓 => Γ pm2.21fal 1502 pm2.21dd 186
¬E Γ, ¬ 𝜓 => Γ𝜓 pm2.21dd 186 definition E in [Indrzejczak] p. 33.
¬E Γ𝜓 & Γ¬ 𝜓 => Γ𝜃 pm2.21dd 186 pm2.21dd 186, pm2.21d 118, pm2.21 120 For an alternative falsum-free natural deduction ruleset. Definition ¬E in [Pfenning] p. 18.
I Γ a1tru 1497 tru 1484, a1tru 1497, trud 1490 Definition I in [Pfenning] p. 18.
E Γ, ⊥𝜃 falimd 1496 falim 1495 Definition E in [Pfenning] p. 18.
I Γ[𝑎 / 𝑥]𝜓 => Γ𝑥𝜓 alrimiv 1857 alrimiv 1857, ralrimiva 2965 Definition Ia in [Pfenning] p. 18, definition In in [Clemente] p. 32.
E Γ𝑥𝜓 => Γ[𝑡 / 𝑥]𝜓 spsbcd 3436 spcv 3290, rspcv 3296 Definition E in [Pfenning] p. 18, definition En,t in [Clemente] p. 32.
I Γ[𝑡 / 𝑥]𝜓 => Γ𝑥𝜓 spesbcd 3508 spcev 3291, rspcev 3300 Definition I in [Pfenning] p. 18, definition In,t in [Clemente] p. 32.
E Γ𝑥𝜓 & Γ, [𝑎 / 𝑥]𝜓𝜃 => Γ𝜃 exlimddv 1865 exlimddv 1865, exlimdd 2091, exlimdv 1863, rexlimdva 3029 Definition Ea,u in [Pfenning] p. 18, definition Em,n,p,a in [Clemente] p. 32.
C Γ, ¬ 𝜓 => Γ𝜓 efald 1501 efald 1501 Proof by contradiction (classical logic), definition C in [Pfenning] p. 17.
C Γ, ¬ 𝜓𝜓 => Γ𝜓 pm2.18da 459 pm2.18da 459, pm2.18d 124, pm2.18 122 For an alternative falsum-free natural deduction ruleset
¬ ¬C Γ¬ ¬ 𝜓 => Γ𝜓 notnotrd 128 notnotrd 128, notnotr 125 Double negation rule (classical logic), definition NNC in [Pfenning] p. 17, definition E¬n in [Clemente] p. 14.
EM Γ𝜓 ∨ ¬ 𝜓 exmidd 432 exmid 431 Excluded middle (classical logic), definition XM in [Pfenning] p. 17, proof 5.11 in [Clemente] p. 14.
=I Γ𝐴 = 𝐴 eqidd 2627 eqid 2626, eqidd 2627 Introduce equality, definition =I in [Pfenning] p. 127.
=E Γ𝐴 = 𝐵 & Γ[𝐴 / 𝑥]𝜓 => Γ[𝐵 / 𝑥]𝜓 sbceq1dd 3428 sbceq1d 3427, 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 27109, ex-natded5.3 27112, ex-natded5.5 27115, ex-natded5.7 27116, ex-natded5.8 27118, ex-natded5.13 27120, ex-natded9.20 27122, and ex-natded9.26 27124.

(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