Hilbert system: Information from Answers.com

In mathematical physics, Hilbert system is an infrequently used term for a physical system described by a C*-algebra.

This article or section appears to contradict itself. Please help fix this problem. (May 2009)

In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus or Hilbert–Ackermann system, is a type of system of formal deduction attributed to Gottlob Frege^[1] and David Hilbert. These deductive systems are most often studied for first-order logic, 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 between logical axioms and rules of inference.^[1] 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. 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 logics, as well— and several infinite axiom schemes. Hilbert systems for propositional modal logics, 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 and sequent calculus contain some context-changing rules. Thus, if we are interested only in the derivability of tautologies, no hypothetical judgments, then we 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.

Systems of natural deduction take the opposite tack, including many deduction rules but very few or no axiom schemes.

1 Formal deductions
- 1.1 Logical axioms
2 Conservative extensions
- 2.1 Existential quantification
- 2.2 Conjunction and Disjunction
3 Metatheorems
4 Further connections
5 Notes
6 References
7 External links

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 inferences. 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 or set theory. The notation $\Gamma \vdash \phi$ means that there is a deduction that ends with $φ$ using as axioms only logical axioms and elements of $Γ$ . Thus, informally, $\Gamma \vdash \phi$ 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 is an infinite set of axioms obtained by substituting all formulas of some form into a specific pattern. Not only are the axioms generated from this pattern, but also any generalization of one of these axioms, is included in the set of logical axioms. A generalization of a formula is obtained by prefixing zero or more universal quantifiers on the formula; thus

$\forall y ( \forall x Pxy \to Pty)$

is a generalization of $\forall x Pxy \to Pty$ .

Logical axioms

A common Hilbert-style system has six infinite axiom schemes and one additional axiom. In order to reduce the number of axiom schemes, this system assumes all formulas have been rewritten to use only the connectives $\lnot$ and $\to$ and only the quantifier $\forall$ . As discussed below, it is possible to extend the system to include additional logical connectives, such as $\land$ and $\lor$ , without enlarging the class of deducible formulas.

The first three logical axiom schemes allow (together with modus ponens) for the manipulation of logical connectives.

1. $\phi \to \left( \psi \to \phi \right)$

2. $\left ( \phi \to ( \psi \rightarrow \xi \right)) \to \left( \left( \phi \to \psi \right) \to \left( \phi \to \xi \right) \right)$

3. $\left ( \lnot \phi \to \lnot \psi \right) \to \left( \psi \to \phi \right)$

The fourth, fifth, and sixth logical axiom schemes provide ways to add, manipulate, and remove universal quantifiers.

4. $\forall x \left( \phi \right) \to \phi[x:=t]$ where t may be substituted for x in $\,\!\phi$

5. $\forall x \left( \phi \to \psi \right) \to \left( \forall x \left( \phi \right) \to \forall x \left( \psi \right) \right)$

6. $\phi \to \forall x \left( \phi \right)$ where x is not a free variable of $\,\!\phi$ .

The final axiom schemes are required to work with formulas involving the equality symbol.

x = x

for every variable x.

8. $\left( x = y \right) \to \left( \phi[z:=x] \to \phi[z:=y] \right)$

Conservative extensions

It is common to include in a Hilbert-style deduction system only axioms for implication and negation. Given these axioms, it is possible to form conservative extensions of the deduction theorem that permit the use of additional connectives. These extensions are called conservative because if a formula φ involving new connectives is rewritten as a logically equivalent formula θ involving only negation, implication, and universal quantification, then φ is derivable in the extended system if and only if θ is derivable in the original system. When fully extended, a Hilbert-style system will resemble more closely a system of natural deduction.

Existential quantification

Introduction

$\forall x(\phi \to \exists y(\phi[x:=y]))$

Elimination

$\forall x(\phi \to \psi) \to \exists x(\phi) \to \psi$ where

x

is not a free variable of

ψ

Conjunction and Disjunction

Conjunction introduction and elimination

introduction: $\alpha\to\beta\to\alpha\land\beta$

elimination left: $\alpha\wedge\beta\to\alpha$

elimination right: $\alpha\wedge\beta\to\beta$

Disjunction introduction and elimination

introduction left: $\alpha\to\alpha\vee\beta$

introduction right: $\beta\to\alpha\vee\beta$

elimination: $(\alpha\to\gamma)\to (\beta\to\gamma) \to \alpha\vee\beta \to \gamma$

Metatheorems

Because Hilbert-style systems have very few deduction rules, it is common to prove metatheorems that show that additional deduction rules add no deductive power, in the sense that a deduction using the new deduction rules can be converted into a deduction using only the original deduction rules.

Some common metatheorems of this form are:

The deduction theorem: $\Gamma;\phi \vdash \psi$ if and only if $\Gamma \vdash \phi \to \psi$ .
$\Gamma \vdash \phi \leftrightarrow \psi$ if and only if $\Gamma \vdash \phi \to \psi$ and $\Gamma \vdash \psi \to \phi$ .
Contraposition: If $\Gamma;\phi \vdash \psi$ then $\Gamma;\lnot \psi \vdash \lnot \phi$ .
Generalization: If $\Gamma \vdash \phi$ and x does not occur free in any formula of $Γ$ then $\Gamma \vdash \forall x \phi$ .

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.

Notes

^ ^a ^b Máté & Ruzsa 1997:129

References

Curry, Haskell B.; Robert Feys (1958). Combinatory Logic Vol. I. 1. Amsterdam: North Holland.
Monk, J. Donald (1976), Mathematical Logic, Graduate Texts in Mathematics, Berlin, New York: Springer-Verlag, ISBN 978-0-387-90170-1
Ruzsa, Imre; Máté, András (1997) (in Hungarian). Bevezetés a modern logikába. Budapest: Osiris Kiadó.
Tarski, Alfred (1990) (in Hungarian). Bizonyítás és igazság. Budapest: Gondolat. It is a Hungarian translation of Alfred Tarski's selected papers on semantic theory of truth.
David Hilbert (1927) "The foundations of mathematics", translated by Stephan Bauer-Menglerberg and Dagfinn Føllesdal (pp. 464–479). in:
- van Heijenoort, Jean (1967, 3rd printing 1976). From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931. Cambrdige MA: Harvard University Press. ISBN 0-674-32449-8 (pbk.).

Hilbert's 1927, Based on an earlier 1925 "foundations" lecture (pp. 367–392), presents his 17 axioms -- axioms of implication #1-4, axioms about & and V #5-10, axioms of negation #11-12, his logical ε-axiom #13, axioms of equality #14-15, and axioms of number #16-17 -- along with the other necessary elements of his Formalist "proof theory" -- e.g. induction axioms, recursion axioms, etc; he also offers up a spirited defense against L.E.J. Brouwer's Intuitionism. Also see Hermann Weyl's (1927) comments and rebuttal (pp. 480–484), Paul Bernay's (1927) appendix to Hilbert's lecture (pp. 485–489) and Luitzen Egbertus Jan Brouwer's (1927) response (pp. 490–495)

Kleene, Stephen Cole (1952, 10th impression with 1971 corrections). Introduction of Metamathematics. Amsterdam NY: North Holland Publishing Company. ISBN 0 7204 2103 9.

See in particular Chapter IV Formal System (pp. 69–85) wherein Kleene presents subchapters §16 Formal symbols, §17 Formation rules, §18 Free and bound variables (including substitution), §19 Transformation rules (e.g. modus ponens) -- and from these he presents 21 "postulates" -- 18 axioms and 3 "immediate-consequence" relations divided as follows: Postulates for the propostional calculus #1-8, Additional postulates for the predicate calculus #9-12, and Additional postulates for number theory #13-21.

External links

Farmer, W. M. "Propositional logic" (pdf). http://imps.mcmaster.ca/courses/SE-2F03-05/slides/02-prop-logic.pdf. It describes (among others) a part of the Hilbert-style deduction system (restricted to propositional calculus).

This entry is from Wikipedia, the leading user-contributed encyclopedia. It may not have been reviewed by professional editors (see full disclaimer)

Donate to Wikimedia

	bra vector (quantum mechanics)
	Hilbert space
	Judgment (mathematical logic)

	What are David Hilbert's accomplishments? Read answer...
	Did david hilbert have a sibling? Read answer...
	In what era did David Hilbert lived in? Read answer...

	Why is david hilbert's accomplishments important?
	What are david hilberts accomplishments?
	What is david hilberts contribuations?

Hilbert system

Contents