Theorem natded

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.

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 _G represents the set of (current) hypotheses. We use wff variable names beginning with ps to provide a closer representation of the Metamath equivalents (which typically use the antedent ph to represent the context _G ).

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 , ex-natded5.3 , ex-natded5.5 , ex-natded5.7 , ex-natded5.8 , ex-natded5.13 , ex-natded9.20 , and ex-natded9.26 .

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

	Ref	Expression
Hypothesis	natded.1	$$⊢\phi$$
Assertion	natded	$$⊢\phi$$

Proof

Step	Hyp	Ref	Expression
1		natded.1	$$⊢\phi$$