:''In
mathematical physics, ''Hilbert system'' is an infrequently used term for a physical system described by a
C*-algebra
In mathematics, specifically in functional analysis, a C∗-algebra (pronounced "C-star") is a Banach algebra together with an involution satisfying the properties of the adjoint. A particular case is that of a complex algebra ''A'' of continuou ...
.''
In
logic, especially
mathematical logic, a Hilbert system, sometimes called Hilbert calculus, Hilbert-style deductive system or Hilbert–Ackermann system, is a type of system of
formal deduction attributed to
Gottlob Frege[Máté & Ruzsa 1997:129] and
David Hilbert. These
deductive system
A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system.
A form ...
s are most often studied for
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifi ...
, but are of interest for other logics as well.
Most variants of Hilbert systems take a characteristic tack in the way they balance a
trade-off
A trade-off (or tradeoff) is a situational decision that involves diminishing or losing one quality, quantity, or property of a set or design in return for gains in other aspects. In simple terms, a tradeoff is where one thing increases, and anot ...
between
logical axiom
An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or ...
s and
rules of inference
In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of in ...
.
Hilbert systems can be characterised by the choice of a large number of
schemes of logical axioms and a small set of
rules of inference
In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of in ...
. Systems of
natural deduction In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use a ...
take the opposite tack, including many deduction rules but very few or no axiom schemes. The most commonly studied Hilbert systems have either just one rule of inference
modus ponens, for
propositional logics or two with
generalisation, to handle
predicate logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifi ...
s, as well and several infinite axiom schemes. Hilbert systems for propositional
modal logic
Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend other ...
s, sometimes called
Hilbert-Lewis systems, are generally axiomatised with two additional rules, the
necessitation rule and the
uniform substitution rule.
A characteristic feature of the many variants of Hilbert systems is that the ''context'' is not changed in any of their rules of inference, while both
natural deduction In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use a ...
and
sequent calculus
In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology i ...
contain some context-changing rules. Thus, if one is interested only in the derivability of
tautologies, no hypothetical judgments, then one can formalize the Hilbert system in such a way that its rules of inference contain only
judgments of a rather simple form. The same cannot be done with the other two deductions systems: as context is changed in some of their rules of inferences, they cannot be formalized so that hypothetical judgments could be avoided not even if we want to use them just for proving derivability of tautologies.
Formal deductions
In a Hilbert-style deduction system, a formal deduction is a finite sequence of formulas in which each formula is either an axiom or is obtained from previous formulas by a rule of inference. These formal deductions are meant to mirror natural-language proofs, although they are far more detailed.
Suppose
is a set of formulas, considered as hypotheses. For example,
could be a set of axioms for
group theory
In abstract algebra, group theory studies the algebraic structures known as groups.
The concept of a group is central to abstract algebra: other well-known algebraic structures, such as rings, fields, and vector spaces, can all be seen as ...
or
set theory. The notation
means that there is a deduction that ends with
using as axioms only logical axioms and elements of
. Thus, informally,
means that
is provable assuming all the formulas in
.
Hilbert-style deduction systems are characterized by the use of numerous schemes of logical axioms. An
axiom scheme In mathematical logic, an axiom schema (plural: axiom schemata or axiom schemas) generalizes the notion of axiom.
Formal definition
An axiom schema is a formula in the metalanguage of an axiomatic system, in which one or more schematic variables ap ...
is an infinite set of axioms obtained by substituting all formulas of some form into a specific pattern. The set of logical axioms includes not only those axioms generated from this pattern, but also any generalization of one of those axioms. A generalization of a formula is obtained by prefixing zero or more universal quantifiers on the formula; for example
is a generalization of
.
Logical axioms
There are several variant axiomatisations of predicate logic, since for any logic there is freedom in choosing axioms and rules that characterise that logic. We describe here a Hilbert system with nine axioms and just the rule modus ponens, which we call the one-rule axiomatisation and which describes classical equational logic. We deal with a minimal language for this logic, where formulas use only the connectives
and
and only the quantifier
. Later we show how the system can be extended to include additional logical connectives, such as
and
, without enlarging the class of deducible formulas.
The first four logical axiom schemes allow (together with modus ponens) for the manipulation of logical connectives.
:P1.
:P2.
:P3.
:P4.
The axiom P1 is redundant, as it follows from P3, P2 and modus ponens (see
proof). These axioms describe
classical propositional logic; without axiom P4 we get
positive implicational logic.
Minimal logic
Minimal logic, or minimal calculus, is a symbolic logic system originally developed by Ingebrigt Johansson. It is an intuitionistic and paraconsistent logic, that rejects both the law of the excluded middle as well as the principle of explosion ...
is achieved either by adding instead the axiom P4m, or by defining
as
.
:P4m.
Intuitionistic logic is achieved by adding axioms P4i and P5i to positive implicational logic, or by adding axiom P5i to minimal logic. Both P4i and P5i are theorems of classical propositional logic.
:P4i.
:P5i.
Note that these are axiom schemes, which represent infinitely many specific instances of axioms. For example, P1 might represent the particular axiom instance
, or it might represent
: the
is a place where any formula can be placed. A variable such as this that ranges over formulae is called a 'schematic variable'.
With a second rule of
uniform substitution (US), we can change each of these axiom schemes into a single axiom, replacing each schematic variable by some propositional variable that isn't mentioned in any axiom to get what we call the substitutional axiomatisation. Both formalisations have variables, but where the one-rule axiomatisation has schematic variables that are outside the logic's language, the substitutional axiomatisation uses propositional variables that do the same work by expressing the idea of a variable ranging over formulae with a rule that uses substitution.
:US. Let
be a formula with one or more instances of the propositional variable
, and let
be another formula. Then from
, infer
.
The next three logical axiom schemes provide ways to add, manipulate, and remove universal quantifiers.
:Q5.