Theorem natded 31019

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 set.mm). 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.

Name	Natural Deduction Rule	Translation	Recommendation	Comments
IT	Γ⊢ 𝜓 => Γ⊢ 𝜓	idi 1	nothing	Reiteration is always redundant in Metamath. Definition "new rule" in [Pfenning] p. 18, definition IT in [Clemente] p. 10.
∧I	Γ⊢ 𝜓 & Γ⊢ 𝜒 => Γ⊢ 𝜓 ∧ 𝜒	jca 521	jca 521, pm3.2i 476	Definition ∧I in [Pfenning] p. 18, definition I∧m,n in [Clemente] p. 10, and definition ∧I in [Indrzejczak] p. 34 (representing both Gentzen's system NK and Jaśkowski)
∧EL	Γ⊢ 𝜓 ∧ 𝜒 => Γ⊢ 𝜓	simpld 500	simpld 500, adantr 486	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 501	simpr 490, adantl 487	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 418	ex 418	Definition →I in [Pfenning] p. 18, definition I=>m,n in [Clemente] p. 11, and definition →I in [Indrzejczak] p. 33.
→E	Γ⊢ 𝜓 → 𝜒 & Γ⊢ 𝜓 => Γ⊢ 𝜒	mpd 16	ax-mp 5, mpd 16, mpdan 700, imp 412	Definition →E in [Pfenning] p. 18, definition E=>m,n in [Clemente] p. 11, and definition →E in [Indrzejczak] p. 33.
∨IL	Γ⊢ 𝜓 => Γ⊢ 𝜓 ∨ 𝜒	olcd 888	olc 882, olci 880, olcd 888	Definition ∨I in [Pfenning] p. 18, definition I∨n(1) in [Clemente] p. 12
∨IR	Γ⊢ 𝜒 => Γ⊢ 𝜓 ∨ 𝜒	orcd 887	orc 881, orci 879, orcd 887	Definition ∨IR in [Pfenning] p. 18, definition I∨n(2) in [Clemente] p. 12.
∨E	Γ⊢ 𝜓 ∨ 𝜒 & Γ, 𝜓⊢ 𝜃 & Γ, 𝜒⊢ 𝜃 => Γ⊢ 𝜃	mpjaodan 973	mpjaodan 973, jaodan 972, jaod 873	Definition ∨E in [Pfenning] p. 18, definition E∨m,n,p in [Clemente] p. 12.
¬I	Γ, 𝜓⊢ ⊥ => Γ⊢ ¬ 𝜓	inegd 1589	pm2.01d 192
¬I	Γ, 𝜓⊢ 𝜃 & Γ⊢ ¬ 𝜃 => Γ⊢ ¬ 𝜓	mtand 828	mtand 828	definition I¬m,n,p in [Clemente] p. 13.
¬I	Γ, 𝜓⊢ 𝜒 & Γ, 𝜓⊢ ¬ 𝜒 => Γ⊢ ¬ 𝜓	pm2.65da 829	pm2.65da 829	Contradiction.
¬I	Γ, 𝜓⊢ ¬ 𝜓 => Γ⊢ ¬ 𝜓	pm2.01da 811	pm2.01d 192, pm2.65da 829, pm2.65d 199	For an alternative falsum-free natural deduction ruleset
¬E	Γ⊢ 𝜓 & Γ⊢ ¬ 𝜓 => Γ⊢ ⊥	pm2.21fal 1591	pm2.21dd 198
¬E	Γ, ¬ 𝜓⊢ ⊥ => Γ⊢ 𝜓		pm2.21dd 198	definition →E in [Indrzejczak] p. 33.
¬E	Γ⊢ 𝜓 & Γ⊢ ¬ 𝜓 => Γ⊢ 𝜃	pm2.21dd 198	pm2.21dd 198, pm2.21d 122, pm2.21 124	For an alternative falsum-free natural deduction ruleset. Definition ¬E in [Pfenning] p. 18.
⊤I	Γ⊢ ⊤	trud 1579	tru 1573, trud 1579, mptru 1576	Definition ⊤I in [Pfenning] p. 18.
⊥E	Γ, ⊥⊢ 𝜃	falimd 1587	falim 1586	Definition ⊥E in [Pfenning] p. 18.
∀I	Γ⊢ [𝑎 / 𝑥]𝜓 => Γ⊢ ∀𝑥𝜓	alrimiv 1961	alrimiv 1961, ralrimiva 3158	Definition ∀Ia in [Pfenning] p. 18, definition I∀n in [Clemente] p. 32.
∀E	Γ⊢ ∀𝑥𝜓 => Γ⊢ [𝑡 / 𝑥]𝜓	spsbcd 3756	spcv 3563, rspcv 3576	Definition ∀E in [Pfenning] p. 18, definition E∀n,t in [Clemente] p. 32.
∃I	Γ⊢ [𝑡 / 𝑥]𝜓 => Γ⊢ ∃𝑥𝜓	spesbcd 3834	spcev 3564, rspcev 3580	Definition ∃I in [Pfenning] p. 18, definition I∃n,t in [Clemente] p. 32.
∃E	Γ⊢ ∃𝑥𝜓 & Γ, [𝑎 / 𝑥]𝜓⊢ 𝜃 => Γ⊢ 𝜃	exlimddv 1969	exlimddv 1969, exlimdd 2259, exlimdv 1967, rexlimdva 3167	Definition ∃Ea,u in [Pfenning] p. 18, definition E∃m,n,p,a in [Clemente] p. 32.
⊥C	Γ, ¬ 𝜓⊢ ⊥ => Γ⊢ 𝜓	efald 1590	efald 1590	Proof by contradiction (classical logic), definition ⊥C in [Pfenning] p. 17.
⊥C	Γ, ¬ 𝜓⊢ 𝜓 => Γ⊢ 𝜓	pm2.18da 812	pm2.18da 812, pm2.18d 128, pm2.18 129	For an alternative falsum-free natural deduction ruleset
¬ ¬C	Γ⊢ ¬ ¬ 𝜓 => Γ⊢ 𝜓	notnotrd 134	notnotrd 134, notnotr 131	Double negation rule (classical logic), definition NNC in [Pfenning] p. 17, definition E¬n in [Clemente] p. 14.
EM	Γ⊢ 𝜓 ∨ ¬ 𝜓	exmidd 909	exmid 908	Excluded middle (classical logic), definition XM in [Pfenning] p. 17, proof 5.11 in [Clemente] p. 14.
=I	Γ⊢ 𝐴 = 𝐴	eqidd 2764	eqid 2763, eqidd 2764	Introduce equality, definition =I in [Pfenning] p. 127.
=E	Γ⊢ 𝐴 = 𝐵 & Γ[𝐴 / 𝑥]𝜓 => Γ⊢ [𝐵 / 𝑥]𝜓	sbceq1dd 3748	sbceq1d 3747, 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 antecedent 𝜑 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 31020, ex-natded5.3 31023, ex-natded5.5 31026, ex-natded5.7 31027, ex-natded5.8 31029, ex-natded5.13 31031, ex-natded9.20 31033, and ex-natded9.26 31035.

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

Hypothesis

Ref	Expression
natded.1	⊢ 𝜑

Assertion

Ref	Expression
natded	⊢ 𝜑

Proof of Theorem natded

Step	Hyp	Ref	Expression
1		natded.1	1 ⊢ 𝜑

This theorem is used by: (None)