= Hilbert proof system
{c}
= Hilbert calculus
{synonym}
A <Hilbert proof system> specifies <axiom>[axiom schemes] and <inference rules>, commonly including <modus ponens rule>[modus ponens]. A <formal proof> is a finite <sequence> of <axiom>[axiom instances], permitted assumptions and conclusions obtained from preceding lines by those rules. <soundness theorem for propositional logic>[Soundness] and completeness compare this syntactic <formal proof>[derivability] with semantic validity or <semantic entailment>. These properties concern the particular chosen <axioms> and rules.
Back to article page
