Definition:Natural Deduction/Derived Rules

From ProofWiki
Jump to navigation Jump to search


In practically working with natural deduction, the following derived rules are useful.

Rule of Substitution

Let $S$ be a sequent of propositional logic that has been proved.

Then we may infer any sequent $S'$ resulting from $S$ by substitutions for letters.

Rule of Sequent Introduction

Let the statements $P_1, P_2, \ldots, P_n$ be conclusions in a proof, on various assumptions.

Let $P_1, P_2, \ldots, P_n \vdash Q$ be a sequent for which we already have a proof.

Then we may infer, at any stage of a proof (citing SI), the conclusion $Q$ of the sequent already proved.

This conclusion depends upon the pool of assumptions upon which $P_1, P_2, \ldots, P_n$ rest.

Rule of Theorem Introduction

We may infer, at any stage of a proof (citing $\text {TI}$), a theorem already proved, together with a reference to the theorem that is being cited.