Hilbert proof system

A Hilbert proof system specifies axiom schemes and inference rules, commonly including modus ponens. A formal proof is a finite sequence of axiom instances, permitted assumptions and conclusions obtained from preceding lines by those rules. Soundness and completeness compare this syntactic derivability with semantic validity or semantic entailment. These properties concern the particular chosen axioms and rules.

One presentation of classical propositional logic uses the schemes $A\to (B\to A)$, $(A\to (B\to C))\to ((A\to (\neg B\to C))\to (A\to C))$, and $(A\to B)\to (A\to (\neg B\to C))$, together with modus ponens rule and the case rule from $A\to B$ and $\neg A\to B$ to $B$. Its deduction theorem for propositional logic follows by induction on logical derivations: conditional modus ponens handles a modus ponens rule line, and the second scheme handles a case-rule line.

Take precisely the propositional tautologies as axioms and supply no inference rules. A one-line proof then establishes exactly the valid propositional formulas, so this calculus is sound and complete for theoremhood. Its axiom set is decidable by finite truth tables. This construction does not by itself give strong completeness for consequence from arbitrary assumptions.