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

Theorem natded 26391
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 552 jca 552, pm3.2i 469 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 473 simpld 473, adantr 479 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 477 simpr 475, adantl 480 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 448 ex 448 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 698, imp 443 Definition E in [Pfenning] p. 18, definition E=>m,n in [Clemente] p. 11, and definition E in [Indrzejczak] p. 33.
IL Γ𝜓 => Γ𝜓𝜒 olcd 406 olc 397, olci 404, olcd 406 Definition I in [Pfenning] p. 18, definition In(1) in [Clemente] p. 12
IR Γ𝜒 => Γ𝜓𝜒 orcd 405 orc 398, orci 403, orcd 405 Definition IR in [Pfenning] p. 18, definition In(2) in [Clemente] p. 12.
E Γ𝜓𝜒 & Γ, 𝜓𝜃 & Γ, 𝜒𝜃 => Γ𝜃 mpjaodan 822 mpjaodan 822, jaodan 821, jaod 393 Definition E in [Pfenning] p. 18, definition Em,n,p in [Clemente] p. 12.
¬I Γ, 𝜓 => Γ¬ 𝜓 inegd 1493 pm2.01d 179
¬I Γ, 𝜓𝜃 & Γ¬ 𝜃 => Γ¬ 𝜓 mtand 688 mtand 688 definition I¬m,n,p in [Clemente] p. 13.
¬I Γ, 𝜓𝜒 & Γ, 𝜓¬ 𝜒 => Γ¬ 𝜓 pm2.65da 597 pm2.65da 597 Contradiction.
¬I Γ, 𝜓¬ 𝜓 => Γ¬ 𝜓 pm2.01da 456 pm2.01d 179, pm2.65da 597, pm2.65d 185 For an alternative falsum-free natural deduction ruleset
¬E Γ𝜓 & Γ¬ 𝜓 => Γ pm2.21fal 1495 pm2.21dd 184
¬E Γ, ¬ 𝜓 => Γ𝜓 pm2.21dd 184 definition E in [Indrzejczak] p. 33.
¬E Γ𝜓 & Γ¬ 𝜓 => Γ𝜃 pm2.21dd 184 pm2.21dd 184, pm2.21d 116, pm2.21 118 For an alternative falsum-free natural deduction ruleset. Definition ¬E in [Pfenning] p. 18.
I Γ a1tru 1490 tru 1478, a1tru 1490, trud 1483 Definition I in [Pfenning] p. 18.
E Γ, ⊥𝜃 falimd 1489 falim 1488 Definition E in [Pfenning] p. 18.
I Γ[𝑎 / 𝑥]𝜓 => Γ𝑥𝜓 alrimiv 1808 alrimiv 1808, ralrimiva 2853 Definition Ia in [Pfenning] p. 18, definition In in [Clemente] p. 32.
E Γ𝑥𝜓 => Γ[𝑡 / 𝑥]𝜓 spsbcd 3320 spcv 3176, rspcv 3182 Definition E in [Pfenning] p. 18, definition En,t in [Clemente] p. 32.
I Γ[𝑡 / 𝑥]𝜓 => Γ𝑥𝜓 spesbcd 3392 spcev 3177, rspcev 3186 Definition I in [Pfenning] p. 18, definition In,t in [Clemente] p. 32.
E Γ𝑥𝜓 & Γ, [𝑎 / 𝑥]𝜓𝜃 => Γ𝜃 exlimddv 1816 exlimddv 1816, exlimdd 2121, exlimdv 1814, rexlimdva 2917 Definition Ea,u in [Pfenning] p. 18, definition Em,n,p,a in [Clemente] p. 32.
C Γ, ¬ 𝜓 => Γ𝜓 efald 1494 efald 1494 Proof by contradiction (classical logic), definition C in [Pfenning] p. 17.
C Γ, ¬ 𝜓𝜓 => Γ𝜓 pm2.18da 457 pm2.18da 457, pm2.18d 122, pm2.18 120 For an alternative falsum-free natural deduction ruleset
¬ ¬C Γ¬ ¬ 𝜓 => Γ𝜓 notnotrd 126 notnotrd 126, notnotr 123 Double negation rule (classical logic), definition NNC in [Pfenning] p. 17, definition E¬n in [Clemente] p. 14.
EM Γ𝜓 ∨ ¬ 𝜓 exmidd 430 exmid 429 Excluded middle (classical logic), definition XM in [Pfenning] p. 17, proof 5.11 in [Clemente] p. 14.
=I Γ𝐴 = 𝐴 eqidd 2515 eqid 2514, eqidd 2515 Introduce equality, definition =I in [Pfenning] p. 127.
=E Γ𝐴 = 𝐵 & Γ[𝐴 / 𝑥]𝜓 => Γ[𝐵 / 𝑥]𝜓 sbceq1dd 3312 sbceq1d 3311, 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 26392, ex-natded5.3 26395, ex-natded5.5 26398, ex-natded5.7 26399, ex-natded5.8 26401, ex-natded5.13 26403, ex-natded9.20 26405, and ex-natded9.26 26407.

(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