Theorem natded 30491

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 516	jca 516, pm3.2i 471	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 495	simpld 495, 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 496	simpr 485, 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 413	ex 413	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 693, imp 407	Definition →E in [Pfenning] p. 18, definition E=>m,n in [Clemente] p. 11, and definition →E in [Indrzejczak] p. 33.
∨IL	Γ⊢ 𝜓 => Γ⊢ 𝜓 ∨ 𝜒	olcd 880	olc 874, olci 872, olcd 880	Definition ∨I in [Pfenning] p. 18, definition I∨n(1) in [Clemente] p. 12
∨IR	Γ⊢ 𝜒 => Γ⊢ 𝜓 ∨ 𝜒	orcd 879	orc 873, orci 871, orcd 879	Definition ∨IR in [Pfenning] p. 18, definition I∨n(2) in [Clemente] p. 12.
∨E	Γ⊢ 𝜓 ∨ 𝜒 & Γ, 𝜓⊢ 𝜃 & Γ, 𝜒⊢ 𝜃 => Γ⊢ 𝜃	mpjaodan 966	mpjaodan 966, jaodan 965, jaod 865	Definition ∨E in [Pfenning] p. 18, definition E∨m,n,p in [Clemente] p. 12.
¬I	Γ, 𝜓⊢ ⊥ => Γ⊢ ¬ 𝜓	inegd 1567	pm2.01d 191
¬I	Γ, 𝜓⊢ 𝜃 & Γ⊢ ¬ 𝜃 => Γ⊢ ¬ 𝜓	mtand 821	mtand 821	definition I¬m,n,p in [Clemente] p. 13.
¬I	Γ, 𝜓⊢ 𝜒 & Γ, 𝜓⊢ ¬ 𝜒 => Γ⊢ ¬ 𝜓	pm2.65da 822	pm2.65da 822	Contradiction.
¬I	Γ, 𝜓⊢ ¬ 𝜓 => Γ⊢ ¬ 𝜓	pm2.01da 804	pm2.01d 191, pm2.65da 822, pm2.65d 197	For an alternative falsum-free natural deduction ruleset
¬E	Γ⊢ 𝜓 & Γ⊢ ¬ 𝜓 => Γ⊢ ⊥	pm2.21fal 1569	pm2.21dd 196
¬E	Γ, ¬ 𝜓⊢ ⊥ => Γ⊢ 𝜓		pm2.21dd 196	definition →E in [Indrzejczak] p. 33.
¬E	Γ⊢ 𝜓 & Γ⊢ ¬ 𝜓 => Γ⊢ 𝜃	pm2.21dd 196	pm2.21dd 196, pm2.21d 121, pm2.21 123	For an alternative falsum-free natural deduction ruleset. Definition ¬E in [Pfenning] p. 18.
⊤I	Γ⊢ ⊤	trud 1557	tru 1551, trud 1557, mptru 1554	Definition ⊤I in [Pfenning] p. 18.
⊥E	Γ, ⊥⊢ 𝜃	falimd 1565	falim 1564	Definition ⊥E in [Pfenning] p. 18.
∀I	Γ⊢ [𝑎 / 𝑥]𝜓 => Γ⊢ ∀𝑥𝜓	alrimiv 1934	alrimiv 1934, ralrimiva 3131	Definition ∀Ia in [Pfenning] p. 18, definition I∀n in [Clemente] p. 32.
∀E	Γ⊢ ∀𝑥𝜓 => Γ⊢ [𝑡 / 𝑥]𝜓	spsbcd 3737	spcv 3543, rspcv 3556	Definition ∀E in [Pfenning] p. 18, definition E∀n,t in [Clemente] p. 32.
∃I	Γ⊢ [𝑡 / 𝑥]𝜓 => Γ⊢ ∃𝑥𝜓	spesbcd 3815	spcev 3544, rspcev 3560	Definition ∃I in [Pfenning] p. 18, definition I∃n,t in [Clemente] p. 32.
∃E	Γ⊢ ∃𝑥𝜓 & Γ, [𝑎 / 𝑥]𝜓⊢ 𝜃 => Γ⊢ 𝜃	exlimddv 1942	exlimddv 1942, exlimdd 2232, exlimdv 1940, rexlimdva 3140	Definition ∃Ea,u in [Pfenning] p. 18, definition E∃m,n,p,a in [Clemente] p. 32.
⊥C	Γ, ¬ 𝜓⊢ ⊥ => Γ⊢ 𝜓	efald 1568	efald 1568	Proof by contradiction (classical logic), definition ⊥C in [Pfenning] p. 17.
⊥C	Γ, ¬ 𝜓⊢ 𝜓 => Γ⊢ 𝜓	pm2.18da 805	pm2.18da 805, 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 901	exmid 900	Excluded middle (classical logic), definition XM in [Pfenning] p. 17, proof 5.11 in [Clemente] p. 14.
=I	Γ⊢ 𝐴 = 𝐴	eqidd 2740	eqid 2739, eqidd 2740	Introduce equality, definition =I in [Pfenning] p. 127.
=E	Γ⊢ 𝐴 = 𝐵 & Γ[𝐴 / 𝑥]𝜓 => Γ⊢ [𝐵 / 𝑥]𝜓	sbceq1dd 3729	sbceq1d 3728, 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 30492, ex-natded5.3 30495, ex-natded5.5 30498, ex-natded5.7 30499, ex-natded5.8 30501, ex-natded5.13 30503, ex-natded9.20 30505, and ex-natded9.26 30507.

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