nLab
Hilbert system

Hilbert systems

Idea

A Hilbert system is a kind of deductive system characterized by the presence of many axioms and few rules?. Usually the only judgment form is “AtrueA \; true” for some proposition AA, which is usually written simply as “AA”. Thus, a Hilbert-style deduction is a tree whose edges are formulas, whose leaves are axioms, and whose nodes are one of a very small number of rules. The most common rule is modus ponens:

AAB B \array{\arrayopts{\rowlines{solid}} A \qquad A\to B \\ B }

and in many Hilbert systems this is the only rule, although sometimes one finds others in use. Then each logical connective is described by imposing axioms.

The role of implication

In many cases, the necessary axioms are obtained fairly straightforwardly from the corresponding rules by replacing derivability and entailment by the implication connective. For instance, the rules for disjunction are

ΓAΓABΓBΓABΓABΓ,ACΓ,BCΓC \frac{\Gamma\vdash A}{\Gamma\vdash A\vee B}\qquad \frac{\Gamma\vdash B}{\Gamma\vdash A\vee B} \qquad \frac{\Gamma\vdash A\vee B \quad \Gamma,A\vdash C \quad \Gamma,B\vdash C}{\Gamma\vdash C}

and the corresponding Hilbert-style axioms are

A(AB)B(AB)(AB)(AC)(BC)C. A\to (A\vee B) \qquad B\to (A\vee B) \qquad (A\vee B) \to (A\to C) \to (B\to C) \to C.

Of course, this gives a special role to implication. Its axioms are

PP P(QP) (P(QR))((PQ)(PR)). \array{ P \to P \\ P \to (Q\to P) \\ (P \to (Q\to R)) \to ((P \to Q) \to (P \to R)). }

Note that these are precisely the types of the basic combinators? in combinatory logic. In fact, under the propositions as types correspondence, Hilbert systems correspond to combinatory logic in the same way that natural deduction/sequent calculus corresponds to lambda-calculus.

On notation

In a Hilbert system one often writes rules and deductions using a turnstile \vdash instead of a horizontal bar. Thus, modus ponens would be written

A,ABB A, A\to B \vdash B

This can be somewhat confusing when comparing a Hilbert system to other systems such as sequent calculus or type theory in which \vdash appears as part of each judgment to specify the context of that judgment. Often the two meanings of \vdash can be conflated, but not always. For instance, in substructural logic such as linear logic or relevance logic, we may have a rule (not an axiom) such as

AB A&B \array{\arrayopts{\rowlines{solid}} A \qquad B \\ A\& B }

(where &\& represents the additive conjunction), which in a Hilbert system would be written as A,BA&BA,B\vdash A\& B. But the sequent A,BA&BA,B\vdash A\& B is not valid in the usual sequent-calculus presentations of such logics, because the comma in the sequent context (on the left) is usually a judgment-level version of the multiplicative conjunction.

Last revised on July 11, 2016 at 16:19:33. See the history of this page for a list of all contributions to it.