Theorem natded 29687

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 513	jca 513, pm3.2i 472	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 496	simpld 496, adantr 482	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 497	simpr 486, adantl 483	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 414	ex 414	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 686, imp 408	Definition →E in [Pfenning] p. 18, definition E=>m,n in [Clemente] p. 11, and definition →E in [Indrzejczak] p. 33.
∨IL	Γ⊢ 𝜓 => Γ⊢ 𝜓 ∨ 𝜒	olcd 873	olc 867, olci 865, olcd 873	Definition ∨I in [Pfenning] p. 18, definition I∨n(1) in [Clemente] p. 12
∨IR	Γ⊢ 𝜒 => Γ⊢ 𝜓 ∨ 𝜒	orcd 872	orc 866, orci 864, orcd 872	Definition ∨IR in [Pfenning] p. 18, definition I∨n(2) in [Clemente] p. 12.
∨E	Γ⊢ 𝜓 ∨ 𝜒 & Γ, 𝜓⊢ 𝜃 & Γ, 𝜒⊢ 𝜃 => Γ⊢ 𝜃	mpjaodan 958	mpjaodan 958, jaodan 957, jaod 858	Definition ∨E in [Pfenning] p. 18, definition E∨m,n,p in [Clemente] p. 12.
¬I	Γ, 𝜓⊢ ⊥ => Γ⊢ ¬ 𝜓	inegd 1562	pm2.01d 189
¬I	Γ, 𝜓⊢ 𝜃 & Γ⊢ ¬ 𝜃 => Γ⊢ ¬ 𝜓	mtand 815	mtand 815	definition I¬m,n,p in [Clemente] p. 13.
¬I	Γ, 𝜓⊢ 𝜒 & Γ, 𝜓⊢ ¬ 𝜒 => Γ⊢ ¬ 𝜓	pm2.65da 816	pm2.65da 816	Contradiction.
¬I	Γ, 𝜓⊢ ¬ 𝜓 => Γ⊢ ¬ 𝜓	pm2.01da 798	pm2.01d 189, pm2.65da 816, pm2.65d 195	For an alternative falsum-free natural deduction ruleset
¬E	Γ⊢ 𝜓 & Γ⊢ ¬ 𝜓 => Γ⊢ ⊥	pm2.21fal 1564	pm2.21dd 194
¬E	Γ, ¬ 𝜓⊢ ⊥ => Γ⊢ 𝜓		pm2.21dd 194	definition →E in [Indrzejczak] p. 33.
¬E	Γ⊢ 𝜓 & Γ⊢ ¬ 𝜓 => Γ⊢ 𝜃	pm2.21dd 194	pm2.21dd 194, pm2.21d 121, pm2.21 123	For an alternative falsum-free natural deduction ruleset. Definition ¬E in [Pfenning] p. 18.
⊤I	Γ⊢ ⊤	trud 1552	tru 1546, trud 1552, mptru 1549	Definition ⊤I in [Pfenning] p. 18.
⊥E	Γ, ⊥⊢ 𝜃	falimd 1560	falim 1559	Definition ⊥E in [Pfenning] p. 18.
∀I	Γ⊢ [𝑎 / 𝑥]𝜓 => Γ⊢ ∀𝑥𝜓	alrimiv 1931	alrimiv 1931, ralrimiva 3147	Definition ∀Ia in [Pfenning] p. 18, definition I∀n in [Clemente] p. 32.
∀E	Γ⊢ ∀𝑥𝜓 => Γ⊢ [𝑡 / 𝑥]𝜓	spsbcd 3792	spcv 3596, rspcv 3609	Definition ∀E in [Pfenning] p. 18, definition E∀n,t in [Clemente] p. 32.
∃I	Γ⊢ [𝑡 / 𝑥]𝜓 => Γ⊢ ∃𝑥𝜓	spesbcd 3878	spcev 3597, rspcev 3613	Definition ∃I in [Pfenning] p. 18, definition I∃n,t in [Clemente] p. 32.
∃E	Γ⊢ ∃𝑥𝜓 & Γ, [𝑎 / 𝑥]𝜓⊢ 𝜃 => Γ⊢ 𝜃	exlimddv 1939	exlimddv 1939, exlimdd 2214, exlimdv 1937, rexlimdva 3156	Definition ∃Ea,u in [Pfenning] p. 18, definition E∃m,n,p,a in [Clemente] p. 32.
⊥C	Γ, ¬ 𝜓⊢ ⊥ => Γ⊢ 𝜓	efald 1563	efald 1563	Proof by contradiction (classical logic), definition ⊥C in [Pfenning] p. 17.
⊥C	Γ, ¬ 𝜓⊢ 𝜓 => Γ⊢ 𝜓	pm2.18da 799	pm2.18da 799, pm2.18d 127, pm2.18 128	For an alternative falsum-free natural deduction ruleset
¬ ¬C	Γ⊢ ¬ ¬ 𝜓 => Γ⊢ 𝜓	notnotrd 133	notnotrd 133, notnotr 130	Double negation rule (classical logic), definition NNC in [Pfenning] p. 17, definition E¬n in [Clemente] p. 14.
EM	Γ⊢ 𝜓 ∨ ¬ 𝜓	exmidd 895	exmid 894	Excluded middle (classical logic), definition XM in [Pfenning] p. 17, proof 5.11 in [Clemente] p. 14.
=I	Γ⊢ 𝐴 = 𝐴	eqidd 2734	eqid 2733, eqidd 2734	Introduce equality, definition =I in [Pfenning] p. 127.
=E	Γ⊢ 𝐴 = 𝐵 & Γ[𝐴 / 𝑥]𝜓 => Γ⊢ [𝐵 / 𝑥]𝜓	sbceq1dd 3784	sbceq1d 3783, 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 29688, ex-natded5.3 29691, ex-natded5.5 29694, ex-natded5.7 29695, ex-natded5.8 29697, ex-natded5.13 29699, ex-natded9.20 29701, and ex-natded9.26 29703.

(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 referenced by: (None)