Jump to navigation Jump to search
Let $\LL$ be a formal language.
A deductive apparatus for $\LL$ is a formally specified system for deriving conclusions about the well-formed formulas of $\LL$.
In mathematics and logic, deductive apparatuses can by and large be divided into proof systems and formal semantics.
A proof system $\mathscr P$ for $\LL$ comprises:
- Axioms and/or axiom schemata;
- Rules of inference for deriving theorems.
It is usual that a proof system does this by declaring certain arguments concerning $\LL$ to be valid.
Informally, a proof system amounts to a precise account of what constitutes a (formal) proof.
A formal semantics for $\LL$ comprises:
Often, a formal semantics provides these by using a lot of auxiliary definitions.