Hilbert system

Hilbert calculi are axiomatic calculi for classical propositional logic or first-order predicate logic, ie calculi in which can be derived theorems and arguments of propositional logic or first-order predicate logic. The two main characteristics of Hilbert calculi are the presence of several axioms or axiom schemata and the small number of rules of inference - in the case of disclosure of axiom schemes often only a single rule, the ponendo modus ponens, and in the case of specification of axioms in addition to a substitution rule.

The term " Hilbert calculus " comes from the mathematician David Hilbert, of the Hilbert program has become known as and later by Gödel's incompleteness theorem aufstellte as unsolvable proven requirement to build all of mathematics and logic to a common uniform and complete axiom system. In a narrower sense, defined only by Hilbert calculi themselves are sometimes referred to as Hilbert calculi, in particular the specified together with Paul Bernays 1934 book " Foundations of Mathematics " axiomatic propositional calculus.

Since the work of Hilbert, in turn, are based on the Begriffsschrift by Gottlob Frege, these calculi are sometimes referred to as " Frege - calculi ".

A Hilbert calculus for classical propositional logic

Syntax

In addition to the statements variables and logical constants of the object plane of the calculus presented here contains the metalinguistic character ├ where A ├ B is read as "B is derivable from A ".

A Hilbert calculation is performed substantially by means of three elementary operations proof. Action ( 1) is to create an instance of an axiom schema. Action ( 2) is putting up a hypothesis, and action ( 3) is to use the modus ponens.

Axioms

To action (1): A Hilbert calculus used as an axiom schemata propositional tautologies, ie formulas that accept under any assignment of truth values ​​to the variables occurring in them set the value " true". Such a tautology, for example, the statement A → (B → A), which is used in many Hilbert calculi as an axiom or an axiom schema. To use it as an axiom schema, then function A and B is a placeholder which can be replaced with any other arbitrary atomic formula; they are used as an axiom, then one needs an additional rule of inference that allows the set variables A and B to be replaced by other formulas - a substitution rule.

Hypothesis

To action (2): As hypothesized refers to the act that derives a formula from a given set of formulas that is included in this set of formulas already. Since the formula given quantity is already deductible, must also each formula, the element of the set is to be derived. Example: One should derive any from the set of formulas M formula. The atomic formula A is element of the formula set M. If M is the set of formulas A deductible. So we can derive A from the formula amount.

Formal:

Let M = {A, B, C}.      Trivially have A ├ A.      Since element M A, M A is ├ ( hypothesis ). Mode ( ponendo ) ponens

The modus ponens to the conclusion of A → B ( "If A, then B " ) and A to B. In the illustrated calculus presents this rule as follows:

For better understanding of an example application. Given a Hilbert calculus with the following five axioms:

The task was to derive from the empty set of formulas (M = { }) the formula A → A, ie M ├ A → A.