- a system of axioms equipped with rules of inference - which allow one to generate new theorems - the set of axioms must be finite - these rules of inference also must operate such that it can be mechanically decided if a proof is valid or not