Hilbert-style deduction system

From Wikipedia, the free encyclopedia

This article or section may need a complete rewrite.
Please discuss this issue on the talk page.

The phrase Hilbert-style deduction system denotes a specific formalization of the notion of deduction in first-order logic [1], attributed to Gottlob Frege and David Hilbert. In fact, various slightly different formalizations are termed under this name in the literature [2]. All of them feature a characteristic trade-off between logical axioms versus rules of inference, by using

For contrast, see natural deduction.

Contents

[edit] Formal description

With some details modified (compared to Frege's work), a detailed treatment can be read in [3]. Here in the article, some further formalizations are used (summarized as “notations”).

[edit] Logical axioms

With the sole exception of the seventh axiom, the other “axioms” are in fact axiom schemas, each embracing countably infinite “instances”. The whole kit of the axioms is understood as their union. It should be proven that it is a recursive set, thus, we can “use” it as we expect (informally: we can always decide in finite time, whether any given formula belongs to the set of axioms).

  1. \mathrm{UnivGen} \ ^* \left\{ \phi \to \left( \psi \to \phi \right) \mid \phi, \psi \in \mathbf{Form} \right\}
  2. \mathrm{UnivGen} \ ^* \left\{ \left( \phi \to \psi \rightarrow \xi \right) \to \left( \left( \phi \to \psi \right) \to \left( \phi \to \xi \right) \right) \mid \phi, \psi, \xi \in \mathbf{Form} \right\}
  3. \mathrm{UnivGen} \ ^* \left\{ \left( \lnot \phi \to \lnot \psi \right) \to \left( \psi \to \phi \right) \mid \phi, \psi \in \mathbf{Form} \right\}
  4. \mathrm{UnivGen} \ ^* \left\{ \forall x \left( \phi \right) \to \phi[x:=t] \mid \mathrm{Sbst} \left( \phi, x, t \right) \right\}
  5. \mathrm{UnivGen} \ ^* \left\{ \forall x \left( \phi \to \psi \right) \to \left( \forall x \left( \phi \right) \to \forall x \left( \psi \right) \right) \mid x \in \mathbf{Var} \land \phi, \psi \in \mathbf{Form} \right\}
  6. \mathrm{UnivGen} \ ^* \left\{ \phi \to \forall x \left( \phi \right) \mid \phi \in \mathbf{Form} \land x \in \mathbf{Var} \setminus \mathrm{FV} \left( \phi \right) \right\}
  7. \mathrm{UnivGen} \ ^* \left\{ \square = \square \right\}
  8. \mathrm{UnivGen} \ ^* \left\{ \left( x = y \right) \to \left( \phi[\square:=x] \to \psi[\square:=y] \right) \mid \mathrm{Sbst} \left( \phi, \square, x \right) \land \mathrm{Sbst} \left( \phi, \square, y \right) \right\}

[edit] Rules of inference

Modus ponens is the sole rule of inference in [3] treatment.

[edit] Deduction

Deduction can be defined

  • either by structural induction [3] (if parametrized over the set of formulae we begin with)
  • or by using appropriate auxiliary notions (sequence, tree etc.).

[edit] Structural induction

Note: parametrized over Γ.

Base (logical axioms, parameter are contained)
\mathrm{LogAx} \subseteq \mathrm{Ded} \left( \Gamma \right)
\Gamma \subseteq \mathrm{Ded} \left( \Gamma \right)
Rule of induction (modus ponens)
If \phi \to \psi \in \mathrm{Ded} \left( \Gamma \right) and \phi \in \mathrm{Ded} \left( \Gamma \right) then \psi \in \mathrm{Ded}\left(A\right)
Closure
No alien objects

[edit] Notations used here

Frege used a non-linear (two-dimensional) notation, which is not followed nowadays. See details on his symbolism in his book titled Begriffsschrift.

A right associative notation is used for material conditional (signed here as \to).

Here, in this article, for brevity's sake and to achieve complete formalization, some additional notations and auxiliary concepts are used, too. Most of them are the straightforward formalizations of their corresponding description mentioned in literature. E.g., universal generalization is mentioned in [3] and also in Alfred Tarski's works, and for brevity's sake and to achieve complete formalization, it is abbreviated here in the article as a function, called “UnivGen”.

\square \in \mathbf{Var}
we use it to emphasize the fact that in the case of the seventh axiom, no meta-variables (over object language variables) are needed: in this sole case, a fixed object language variable can be used.
Var, Term, Form
set of all variables, terms, formulas of the object language
\mathrm{FV} : \mathbf{Form} \cup \mathbf{Term} \to \mathbf{Var}
the set of free variables of a term or formula
\mathrm{Sbst} \subseteq \mathbf{Form} \times \mathbf{Var} \times \mathbf{Term}
a relation for formalizing the notion of “allowed substitution”
\mathrm{UnivGen} : \mathrm{Form} \to \mathrm{Form}
universal generalization of a formula (with all possible allowed variables, iterated as many times as we please)
f \ ^* A \in 2^B where f : A \to B
a notation used in [4], f \ ^* A = \left\{ f \left( a \right) \in B \mid a \in A \right\}

[edit] Further connections

Axiom 1, 2 together with deduction rule modus ponens, corresponds to combinatory logic base combinators K, S together with the notion of application. See also Curry-Howard correspondence.

[edit] Notes

  1. ^ or sometimes its straightforward restriction to propositional calculus
  2. ^ Ferenczi, Miklós: Matematikai logika. Műszaki Könyvkiadó, Budapest, 2002.
  3. ^ a b c d Ruzsa, Imre and Máté, András: Bevezetés a modern logikába. Osiris Kiadó, Budapest, 1997.
  4. ^ Monk, J. Donald: Mathematical Logic. Springer-Verlag, New York • Heidelberg • Berlin, 1976.

[edit] External links

W.M Farmer: Propositional logic describes (among others) a part of the Hilbert-style deduction system (restricted to propositional calculus).

Retrieved from "http://en.wikipedia.org../../../h/i/l/Hilbert-style_deduction_system.html"