= Hilbert-style first-order calculus
{c}
A Hilbert-style calculus specifies axiom schemes and a small collection of inference rules, typically implication elimination and universal <universal generalization rule>[generalization]. Equality and <quantifier> schemes include substitution and free-variable side conditions. Proofs are finite syntactic derivations; validity is separately defined using structures and assignments. A context-sensitive presentation restricts <universal generalization rule>[generalization] by its actual undischarged assumptions.
Back to article page
