# Hilbert-style deduction system

In

logic , especiallymathematical logic , a**"Hilbert-style deduction system**" is a type of system of "formal deduction" attributed toGottlob Frege Máté & Ruzsa 1997:129] andDavid Hilbert . Thesedeductive system s are most often studied forfirst-order logic , but are of interest for other logics as well.Most variants of Hilbert-style deductions systems take a characteristic tack the way they balance a

trade-off betweenlogical axiom s and rules of inference. Hilbert-style deduction systems can be characterized 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-style deduction system has just one rule of inference –modus ponens – and several infinite axiom schemes.A characteristic feature of the various variants of Hilbert-style deduction systems is that the "context" is not changed in any of their rules of inference, while both

natural deduction andsequent 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-style deduction 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.**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 $Gamma$ is a set of formulas, considered as

**hypotheses**. For example $Gamma$ could be a set of axioms forgroup theory orset theory . The notation $Gamma\; vdash\; phi$ means that there is a deduction that ends with $phi$ using as axioms only**logical axioms**and elements of $Gamma$. Thus, informally, $Gamma\; vdash\; phi$ means that $phi$ is provable assuming all the formulas in $Gamma$.Hilbert-style deduction systems are characterized by the use of numerous schemes of

**logical axioms**. Anaxiom 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\; o\; Pty)$is a generalization of $forall\; x\; Pxt\; o\; 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 $o$ 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\; o\; left(\; psi\; o\; phi\; ight)$:2. $left\; (\; phi\; o\; (\; psi\; ightarrow\; xi\; ight))\; o\; left(\; left(\; phi\; o\; psi\; ight)\; o\; left(\; phi\; o\; xi\; ight)\; ight)$:3. $left\; (\; lnot\; phi\; o\; lnot\; psi\; ight)\; o\; left(\; psi\; o\; phi\; ight)$

The fourth, fifth, and sixth logical axiom schemes provide ways to add, manipulate, and remove universal quantifiers.:4. $forall\; x\; left(\; phi\; ight)\; o\; phi\; [x:=t]$ where "t" may be substituted for "x" in $phi$:5. $forall\; x\; left(\; phi\; o\; psi\; ight)\; o\; left(\; forall\; x\; left(\; phi\; ight)\; o\; forall\; x\; left(\; psi\; ight)\; ight)$:6. $phi\; o\; forall\; x\; left(\; phi\; ight)$ where "x" is not a

free variable of $phi$.The final axiom schemes are required to work with formulas involving the equality symbol.:7. $x\; =\; x$ for every variable "x".:8. $left(\; x\; =\; y\; ight)\; o\; left(\; phi\; [z:=x]\; o\; phi\; [z:=y]\; ight)$

**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 extension s of thededuction 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 ofnatural deduction .**Existential quantification*** Introduction

* Elimination**Conjunction and disjunction*** Conjunction introduction and elimination

* Disjunction introduction and elimination**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\; o\; psi$.

* $Gamma\; vdash\; phi\; leftrightarrow\; psi$ if and only if $Gamma\; vdash\; phi\; o\; psi$ and $Gamma\; vdash\; psi\; o\; 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 $Gamma$ 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 alsoCurry-Howard correspondence .**Notes****References*** cite book

last = Curry

first = Haskell B.

coauthors = Robert Feys

title = Combinatory Logic Vol. I

volume = 1

year = 1958

publisher = North Holland

location = Amsterdam

*

*

* It is a Hungarian translation ofAlfred Tarski 's selected papers onsemantic theory of truth .**External links**cite web |last=Farmer |first=W. M |title=Propositional logic |url=http://www.cas.mcmaster.ca/~wmfarmer/SE-2F03-05/slides/02-prop-logic.pdf |format=pdf It describes (among others) a part of the Hilbert-style deduction system (restricted to

propositional calculus ).

*Wikimedia Foundation.
2010.*

### Look at other dictionaries:

**David Hilbert**— Hilbert redirects here. For other uses, see Hilbert (disambiguation). David Hilbert David Hilbert (1912) Born … Wikipedia**Axiomatic system**— In mathematics, an axiomatic system is any set of axioms from which some or all axioms can be used in conjunction to logically derive theorems. A mathematical theory consists of an axiomatic system and all its derived theorems. An axiomatic… … Wikipedia**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 the axiomatic systems which instead use… … Wikipedia**Formal system**— In formal logic, a formal system (also called a logical system,Audi, Robert (Editor). The Cambridge Dictionary of Philosophy . Second edition, Cambridge University Press, 1999. ISBN 978 0521631365 (hardcover) and ISBN 978 0521637220 (paperback).] … Wikipedia**Curry–Howard correspondence**— A proof written as a functional program: the proof of commutativity of addition on natural numbers in the proof assistant Coq. nat ind stands for mathematical induction, eq ind for substitution of equals and f equal for taking the same function… … Wikipedia**Curry-Howard correspondence**— The Curry Howard correspondence is the direct relationship between computer programs and mathematical proofs. Also known as Curry Howard isomorphism, proofs as programs correspondence and formulae as types correspondence, it refers to the… … Wikipedia**Propositional calculus**— In mathematical logic, a propositional calculus or logic (also called sentential calculus or sentential logic) is a formal system in which formulas of a formal language may be interpreted as representing propositions. A system of inference rules… … Wikipedia**Judgment (mathematical logic)**— In mathematical logic, a judgment can be for example an assertion about occurrence of a free variable in an expression of the object language, or about provability of a proposition (either as a tautology or from a given context); but judgments… … Wikipedia**List of mathematics articles (H)**— NOTOC H H cobordism H derivative H index H infinity methods in control theory H relation H space H theorem H tree Haag s theorem Haagerup property Haaland equation Haar measure Haar wavelet Haboush s theorem Hackenbush Hadamard code Hadamard… … Wikipedia**Boolean algebra (introduction)**— Boolean algebra, developed in 1854 by George Boole in his book An Investigation of the Laws of Thought , is a variant of ordinary algebra as taught in high school. Boolean algebra differs from ordinary algebra in three ways: in the values that… … Wikipedia