Assumption Glossary
Definition
An assumption in the natural deduction calculus is a formula introduced into a derivation without any justification in terms of the formulae earlier in the sequence. Assumptions are annotated with 'A' and depend only on themselves.
Comments
Any assumption which is used in a proof and which is not one of the premises of the sequent being proved must be discharged. Otherwise the eventual conclusion will depend on it, and the proof will therefore not establish the desired sequent.
Assumption numbers are the numbers written to the left of each line of proof. They record which of the assumptions the line depends on. They can be seen as abbreviations (or code if we prefer) for the formulae assumed.
Examples
-
The rule of assumptions on its own can only establish
trivial sequents of the form A
⊢ A. The following one-line proof
illustrates: