Theorem natded 28188

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 515	jca 515, pm3.2i 474	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 498	simpld 498, adantr 484	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 499	simpr 488, adantl 485	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 416	ex 416	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 410	Definition →E in [Pfenning] p. 18, definition E=>m,n in [Clemente] p. 11, and definition →E in [Indrzejczak] p. 33.
∨IL	Γ⊢ 𝜓 => Γ⊢ 𝜓 ∨ 𝜒	olcd 871	olc 865, olci 863, olcd 871	Definition ∨I in [Pfenning] p. 18, definition I∨n(1) in [Clemente] p. 12
∨IR	Γ⊢ 𝜒 => Γ⊢ 𝜓 ∨ 𝜒	orcd 870	orc 864, orci 862, orcd 870	Definition ∨IR in [Pfenning] p. 18, definition I∨n(2) in [Clemente] p. 12.
∨E	Γ⊢ 𝜓 ∨ 𝜒 & Γ, 𝜓⊢ 𝜃 & Γ, 𝜒⊢ 𝜃 => Γ⊢ 𝜃	mpjaodan 956	mpjaodan 956, jaodan 955, jaod 856	Definition ∨E in [Pfenning] p. 18, definition E∨m,n,p in [Clemente] p. 12.
¬I	Γ, 𝜓⊢ ⊥ => Γ⊢ ¬ 𝜓	inegd 1558	pm2.01d 193
¬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 193, pm2.65da 816, pm2.65d 199	For an alternative falsum-free natural deduction ruleset
¬E	Γ⊢ 𝜓 & Γ⊢ ¬ 𝜓 => Γ⊢ ⊥	pm2.21fal 1560	pm2.21dd 198
¬E	Γ, ¬ 𝜓⊢ ⊥ => Γ⊢ 𝜓		pm2.21dd 198	definition →E in [Indrzejczak] p. 33.
¬E	Γ⊢ 𝜓 & Γ⊢ ¬ 𝜓 => Γ⊢ 𝜃	pm2.21dd 198	pm2.21dd 198, pm2.21d 121, pm2.21 123	For an alternative falsum-free natural deduction ruleset. Definition ¬E in [Pfenning] p. 18.
⊤I	Γ⊢ ⊤	trud 1548	tru 1542, trud 1548, mptru 1545	Definition ⊤I in [Pfenning] p. 18.
⊥E	Γ, ⊥⊢ 𝜃	falimd 1556	falim 1555	Definition ⊥E in [Pfenning] p. 18.
∀I	Γ⊢ [𝑎 / 𝑥]𝜓 => Γ⊢ ∀𝑥𝜓	alrimiv 1928	alrimiv 1928, ralrimiva 3149	Definition ∀Ia in [Pfenning] p. 18, definition I∀n in [Clemente] p. 32.
∀E	Γ⊢ ∀𝑥𝜓 => Γ⊢ [𝑡 / 𝑥]𝜓	spsbcd 3734	spcv 3554, rspcv 3566	Definition ∀E in [Pfenning] p. 18, definition E∀n,t in [Clemente] p. 32.
∃I	Γ⊢ [𝑡 / 𝑥]𝜓 => Γ⊢ ∃𝑥𝜓	spesbcd 3812	spcev 3555, rspcev 3571	Definition ∃I in [Pfenning] p. 18, definition I∃n,t in [Clemente] p. 32.
∃E	Γ⊢ ∃𝑥𝜓 & Γ, [𝑎 / 𝑥]𝜓⊢ 𝜃 => Γ⊢ 𝜃	exlimddv 1936	exlimddv 1936, exlimdd 2218, exlimdv 1934, rexlimdva 3243	Definition ∃Ea,u in [Pfenning] p. 18, definition E∃m,n,p,a in [Clemente] p. 32.
⊥C	Γ, ¬ 𝜓⊢ ⊥ => Γ⊢ 𝜓	efald 1559	efald 1559	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 135	notnotrd 135, notnotr 132	Double negation rule (classical logic), definition NNC in [Pfenning] p. 17, definition E¬n in [Clemente] p. 14.
EM	Γ⊢ 𝜓 ∨ ¬ 𝜓	exmidd 893	exmid 892	Excluded middle (classical logic), definition XM in [Pfenning] p. 17, proof 5.11 in [Clemente] p. 14.
=I	Γ⊢ 𝐴 = 𝐴	eqidd 2799	eqid 2798, eqidd 2799	Introduce equality, definition =I in [Pfenning] p. 127.
=E	Γ⊢ 𝐴 = 𝐵 & Γ[𝐴 / 𝑥]𝜓 => Γ⊢ [𝐵 / 𝑥]𝜓	sbceq1dd 3726	sbceq1d 3725, 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 28189, ex-natded5.3 28192, ex-natded5.5 28195, ex-natded5.7 28196, ex-natded5.8 28198, ex-natded5.13 28200, ex-natded9.20 28202, and ex-natded9.26 28204.

(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)