Let $\mathcal L$ be a formal language.
A deductive apparatus for $\mathcal L$ is a formally specified system for deriving conclusions about the well-formed formulas of $\mathcal L$.
A proof system $\mathscr P$ for $\mathcal L$ comprises:
- Axioms and/or axiom schemata;
- Rules of inference for deriving theorems.
Informally, a proof system amounts to a precise account of what constitutes a (formal) proof.
A formal semantics for $\mathcal L$ comprises:
- A collection of objects called structures;
- A notion of validity of $\mathcal L$-WFFs in these structures.
Often, a formal semantics provides these by using a lot of auxiliary definitions.