## FANDOM

174 Pages

A deduction from a set is a sequence of well-formed formulas with each element being justified as a tautology or the result of a rule of inference. A deduction from the empty set is a proof.

## Formal definitionEdit

Let $\mathcal{S}$ be a formal system and let $\mathcal{L}$ be it's underlying formal language and let $\Delta \subseteq \mathcal{L}$

Then a deduction of $S_n$ from $\Delta$is a sequence $S_1,\ldots,S_n$ of well-formed formulas such that one of the following holds for $1\leq i \leq n$:

1. $\vdash S_i$
2. $S_i \in \Delta$
3. $S_i$ is justified by a rule of inference of $\mathcal{S}$.

A deduction of $S_n$ from $\Delta$ is a proof if and only if $\Delta = \emptyset$.