Hilbert calculus

This article deals with axiomatic logical calculi. For the Hilbert calculus of geometry see Hilbert's system of axioms of Euclidean geometry

Hilbert calculi are axiomatic calculi for classical propositional logic or first-order predicate logic , i.e. calculi in which theorems and arguments of propositional logic or first-order predicate logic can be derived . The two main features of Hilbert calculi are the existence of a number of axioms or axiom schemes as well as the small number of inference rules - in the case of axiom schemes often only a single rule, the modus ponendo ponens , and in the case of axioms, an additional rule of substitution .

The name "Hilbertkalkül" goes back to the mathematician David Hilbert , who made what became known as the Hilbert program and later proved to be unsolvable by Gödel's incompleteness theorem , to build all mathematics and logic on a common, uniform and complete system of axioms . In a narrower sense, only the calculi given by Hilbert himself are sometimes referred to as Hilbert calculi, in particular the axiomatic propositional calculus given together with Paul Bernays in 1934 in the work "Fundamentals of Mathematics".

Again, since the works of Hilbert on the Begriffsschrift of Gottlob Frege based, these calculi are sometimes referred to as "Frege-calculi".

A Hilbert calculus for classical propositional logic

syntax

In addition to the statement variables and logical constants of the object level, the calculus presented here contains the metalinguistic sign , whereby it is read as “ can be derived from ”. ${\displaystyle \vdash }$ ${\displaystyle A\vdash B}$ ${\displaystyle B}$ ${\displaystyle A}$

In a Hilbert calculus, proof is essentially carried out with the help of three elementary operations. Action (1) is to create an instance of an axiom scheme. Action (2) is to hypothesize and action (3) is to use the ponens mode .

Axioms

Action (1): A Hilbert calculus uses propositional tautologies as axiom schemes, i.e. formulas that assume the value “true” under every assignment of truth values to the propositional variables occurring in them. Such a tautology is, for example, the statement which is used in many Hilbert calculi as an axiom or as an axiom scheme. If they are used as an axiom scheme, then A and B function as placeholders in them, which can be exchanged for any other atomic formula; if one uses it as an axiom, then one also needs an inference rule that allows the sentence variables A and B to be replaced by other formulas - a substitution rule. ${\displaystyle A\rightarrow (B\rightarrow A)}$

hypothesis

To action (2): The setting up of a hypothesis is the action that derives a formula from a given set of formulas that is already contained in this set of formulas. Since the given formula set can already be derived, every single formula that is an element of the set must also be deducible. Example: One should derive some formula from the formula set M. The atomic formula A is an element of the formula set M. Given the formula set M, A can be derived. So we can derive A from the formula set.

formally:

    Sei  ${\displaystyle M={A,B,C}}$. 
    Trivialerweise gilt  ${\displaystyle A\vdash A}$. 
    Da  ${\displaystyle A}$ Element von  ${\displaystyle M}$ ist, gilt  ${\displaystyle M\vdash A}$ (die Hypothese).

Modus (ponendo) ponens

The ponens mode allows the end of (“If A, then B”) and on . In the calculation presented here, this rule is presented as follows: ${\displaystyle A\rightarrow B}$ ${\displaystyle A}$ ${\displaystyle B}$

${\displaystyle M}$and be formula sets and and be formulas. ${\displaystyle N}$ ${\displaystyle A}$ ${\displaystyle B}$

If now from the formula amount of the formula is derivable from the formula and when amount of the formula is derivable, then from the union of and the formula derivable; in formal notation: ${\displaystyle M}$ ${\displaystyle A}$ ${\displaystyle N}$ ${\displaystyle A\rightarrow B}$ ${\displaystyle M}$ ${\displaystyle N}$ ${\displaystyle B}$

${\displaystyle M\vdash A}$

${\displaystyle N\vdash A\rightarrow B}$

${\displaystyle M\cup N\vdash B}$

An example of the application for a better understanding. A Hilbert calculus is given with the following five axioms:

1. ${\displaystyle F\rightarrow (G\rightarrow F)}$
2. ${\displaystyle (F\rightarrow (G\rightarrow H))\rightarrow ((F\rightarrow G)\rightarrow (F\rightarrow H))}$
3. ${\displaystyle (F\rightarrow G)\rightarrow (\neg G\rightarrow \neg F)}$
4. ${\displaystyle F\rightarrow (\neg F\rightarrow G)}$
5. ${\displaystyle (\neg F\rightarrow F)\rightarrow F}$

The task is to derive the formula from the empty formula set ( ) , that is . ${\displaystyle M=\{\}}$ ${\displaystyle A\rightarrow A}$ ${\displaystyle M\vdash A\rightarrow A}$

step	formula	Explanation
1	${\displaystyle M\vdash A\rightarrow ((B\rightarrow A)\rightarrow A)}$	Instance of axiom (1) ( replaced by , replaced by ) ${\displaystyle F}$ ${\displaystyle A}$ ${\displaystyle G}$ ${\displaystyle (B\rightarrow A)}$
2	${\displaystyle M\vdash (A\rightarrow ((B\rightarrow A)\rightarrow A))\rightarrow ((A\rightarrow (B\rightarrow A))\rightarrow (A\rightarrow A))}$	Instance of axiom (2) ( replaced by , replaced by , replaced by ) ${\displaystyle F}$ ${\displaystyle A}$ ${\displaystyle G}$ ${\displaystyle (B\rightarrow A)}$ ${\displaystyle H}$ ${\displaystyle A}$
3	${\displaystyle M\vdash (A\rightarrow (B\rightarrow A))\rightarrow (A\rightarrow A)}$	Modus ponens from steps 1 and 2.
4th	${\displaystyle M\vdash A\rightarrow (B\rightarrow A)}$	Instance of axiom (1) ( replaced by , replaced by ) ${\displaystyle F}$ ${\displaystyle A}$ ${\displaystyle G}$ ${\displaystyle B}$
5	${\displaystyle M\vdash A\rightarrow A}$	Modus ponens from steps 3 and 4.

literature

• David Hilbert, Paul Bernays: Fundamentals of Mathematics . Volume 1 Berlin 1934, Volume 2 Berlin 1939
• H. Ehrig, B. Mahr, F. Cornelius, M. Grosse-Rhode, P. Zeitz: Mathematical-structural basics of computer science . Springer-Verlag, Berlin et al. 2001, ISBN 3-540-41923-3 .

Web links

• Formal predicate logic (PDF; 508 kB), a compilation of axioms, rules and propositions with formal proofs in the style of Hilbert

Individual evidence

1. ↑ Introduction to set theory: Georg Cantor's set theory and its axiomatization by Ernst Zermelo, Oliver Deiser, Gabler Wissenschaftsverlage, 2009, ISBN 3642014445 , limited preview in the Google book search