Enhanced vegetation index

2014-01-05T07:49:21Z

84.149.209.142: /* Two-band EVI */

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

{{Expert-subject|Mathematics|talk=Article is a mess...|date=March 2011}}

In [[logic]], especially [[mathematical logic]], a '''Hilbert system''', sometimes called '''Hilbert calculus''' or '''Hilbert–Ackermann system''', is a type of system of [[Deductive reasoning|formal deduction]] attributed to [[Gottlob Frege]]<ref name="Máté & Ruzsa 1997">Máté & Ruzsa 1997:129</ref> and [[David Hilbert]]. These [[deductive system]]s 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 axiom]]s and [[Rule of inference|rules of inference]].<ref name="Máté & Ruzsa 1997"/> Hilbert systems can be characterised by the choice of a large number of [[axiom schema|schemes]] of logical axioms and a small set of [[Rule of inference|rules of inference]]. Systems of [[natural deduction]] take the opposite tack, including many deduction rules but very few or no axiom schemes. The most commonly studied Hilbert systems have either just one rule of inference — [[modus ponens]], for [[propositional logic]]s — or two — with [[generalization (logic)|generalisation]], to handle [[predicate logic]]s, as well — and several infinite axiom schemes. Hilbert systems for propositional [[modal logic]]s, sometimes called [[Hilbert-Lewis system]]s, 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 [[tautology (logic)|tautologies]], no hypothetical judgments, then we can formalize the Hilbert system in such a way that its rules of inference contain only [[Judgment (mathematical logic)|judgment]]s 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.

== Formal deductions ==

[[File:Deduction architecture.png|right|300px|A graphic representation of the deduction system]]

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 inference. These formal deductions are meant to mirror natural-language proofs, although they are far more detailed.

Suppose <math>\Gamma</math> is a set of formulas, considered as '''hypotheses'''. For example <math>\Gamma</math> could be a set of axioms for [[group theory]] or [[set theory]]. The notation <math>\Gamma \vdash \phi</math> means that there is a deduction that ends with <math>\phi</math> using as axioms only '''logical axioms''' and elements of <math>\Gamma</math>. Thus, informally, <math>\Gamma \vdash \phi</math> means that <math>\phi</math> is provable assuming all the formulas in <math>\Gamma</math>.

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. The set of logical axioms includes not only those axioms generated from this pattern, but also any generalization of one of those axioms. A generalization of a formula is obtained by prefixing zero or more universal quantifiers on the formula; thus
:<math>\forall y ( \forall x Pxy \to Pty)</math>
is a generalization of <math>\forall x Pxy \to Pty</math>.

=== Logical axioms ===

There are several variant axiomatisations of predicate logic, since for any logic there is freedom in choosing axioms and rules that characterise that logic. We describe here a Hilbert system with nine axioms and just the rule modus ponens, which we call the one-rule axiomatisation and which describes classical equational logic. We deal with a minimal language for this logic, where formulas use only the connectives <math>\lnot</math> and <math>\to</math> and only the quantifier <math>\forall</math>. Later we show how the system can be extended to include additional logical connectives, such as <math>\land</math> and <math>\lor</math>, without enlarging the class of deducible formulas.

The first four logical axiom schemes allow (together with modus ponens) for the manipulation of logical connectives.
:P1. <math>\phi \to \phi </math>
:P2. <math>\phi \to \left( \psi \to \phi \right) </math>
:P3. <math>\left ( \phi \to ( \psi \rightarrow \xi \right)) \to \left( \left( \phi \to \psi \right) \to \left( \phi \to \xi \right) \right)</math>
:P4. <math>\left ( \lnot \phi \to \lnot \psi \right) \to \left( \psi \to \phi \right) </math>

The axiom P1 is redundant, as it follows from P3, P2 and modus ponens. These axioms describe [[classical propositional logic]]; without axiom P4 we get [[minimal logic]]. [[Intuitionistic logic]] is achieved by adding instead the axiom P4i for ex falso quodlibet, which is an axiom of classical propositional logic.
:P4i. <math>\lnot\phi \to \left( \phi \to \psi \right) </math>

Note that these are axiom schemes, which represent infinitely many specific instances of axioms. For example, P1 might represent the particular axiom instance <math>p \to p </math>, or it might represent <math>\left( p \to q \right) \to \left( p \to q \right) </math>: the <math>\phi</math> is a place where any formula can be placed. A variable such as this that ranges over formulae is called a 'schematic variable'.

With a second rule of [[uniform substitution]] (US), we can change each of these axiom schemes into a single axiom, replacing each schematic variable by some propositional variable that isn't mentioned in any axiom to get what we call the substitutional axiomatisation. Both formalisations have variables, but where the one-rule axiomatisation has schematic variables that are outside the logic's language, the substitutional axiomatisation uses propositional variables that do the same work by expressing the idea of a variable ranging over formulae with a rule that uses substitution.

:US. Let <math>\phi(p)</math> be a formula with one or more instances of the propositional variable <math>p</math>, and let <math>\psi</math> be another formula. Then from <math>\phi(p)</math>, infer <math>\phi(\psi)</math>.

The next three logical axiom schemes provide ways to add, manipulate, and remove universal quantifiers.
:Q5. <math> \forall x \left( \phi \right) \to \phi[x:=t]</math> where ''t'' may be substituted for ''x'' in <math>\,\!\phi</math>
:Q6. <math>\forall x \left( \phi \to \psi \right) \to \left( \forall x \left( \phi \right) \to \forall x \left( \psi \right) \right)</math>
:Q7. <math> \phi \to \forall x \left( \phi \right) </math> where ''x'' is not a [[free variable]] of <math>\,\!\phi</math>.

These three additional rules extend the propositional system to axiomatise [[classical predicate logic]]. Likewise, these three rules extend system for intuitionstic propositional logic (with P1-3 and P4i) to [[intuitionistic predicate logic]].

Universal quantification is often given an alternative axiomatisation using an extra rule of generalisation (see the section on Metatheorems), in which case the rules Q5 and Q6 are redundant.

The final axiom schemes are required to work with formulas involving the equality symbol.
:I8. <math>x = x</math> for every variable ''x''.
:I9. <math>\left( x = y \right) \to \left( \phi[z:=x] \to \phi[z:=y] \right)</math>

== 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 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 [[Logical equivalence|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
:<math> \forall x(\phi \to \exists y(\phi[x:=y])) </math>

* Elimination
:<math> \forall x(\phi \to \psi) \to \exists x(\phi) \to \psi </math> where <math>x</math> is not a [[free variable]] of <math>\psi</math>.

=== Conjunction and Disjunction ===

* Conjunction introduction and elimination
:introduction: <math> \alpha\to\beta\to\alpha\land\beta </math>
:elimination left: <math> \alpha\wedge\beta\to\alpha </math>
:elimination right: <math> \alpha\wedge\beta\to\beta </math>
* Disjunction introduction and elimination
:introduction left: <math> \alpha\to\alpha\vee\beta </math>
:introduction right: <math> \beta\to\alpha\vee\beta </math>
:elimination: <math> (\alpha\to\gamma)\to (\beta\to\gamma) \to \alpha\vee\beta \to \gamma </math>

== 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''': <math>\Gamma;\phi \vdash \psi</math> if and only if <math>\Gamma \vdash \phi \to \psi</math>.
* <math>\Gamma \vdash \phi \leftrightarrow \psi</math> if and only if <math>\Gamma \vdash \phi \to \psi</math> and <math>\Gamma \vdash \psi \to \phi</math>.
* Contraposition: If <math>\Gamma;\phi \vdash \psi</math> then <math>\Gamma;\lnot \psi \vdash \lnot \phi</math>.
* Generalization: If <math>\Gamma \vdash \phi</math> and ''x'' does not occur free in any formula of <math>\Gamma</math> then <math>\Gamma \vdash \forall x \phi</math>.

== Alternative axiomatizations ==
{{see|List of logic systems}}

The axiom 3 above is credited to [[Jan Łukasiewicz|Łukasiewicz]].<ref name="Tarski">A. Tarski, Logic, semantics, metamathematics, Oxford, 1956</ref> The original system by [[Gottlob Frege|Frege]] had axioms P2 and P3 but four other axioms instead of axiom P4 (see [[Frege's propositional calculus]]).
[[Bertrand Russell|Russell]] and [[Alfred North Whitehead|Whitehead]] also suggested a system with five propositional axioms.

== Further connections ==

Axioms P1, P2 and P3, with the deduction rule modus ponens (formalising [[intuitionistic propositional logic]]), correspond to [[combinatory logic]] base combinators '''I''', '''K''' and '''S''' with the application operator. Proofs in the Hilbert system then correspond to combinator terms in combinatory logic. See also [[Curry-Howard correspondence]].

== Notes ==

<references/>

== 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
}}
* {{Cite book | last1=Monk | first1=J. Donald | title=Mathematical Logic | publisher=[[Springer-Verlag]] | location=Berlin, New York | series=Graduate Texts in Mathematics | isbn=978-0-387-90170-1 | year=1976 | postscript=.}}
* {{cite book |last=Ruzsa |first=Imre |coauthors=Máté, András |title=Bevezetés a modern logikába |publisher=Osiris Kiadó |location=Budapest |year=1997 |language=Hungarian}}
* {{cite book |last=Tarski |first=Alfred |title=Bizonyítás és igazság |publisher=Gondolat |location=Budapest |year=1990 |language=Hungarian}} 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:
** {{cite book
| last = van Heijenoort
| first = Jean
| title = From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931
| year = 1967, 3rd printing 1976
| publisher = Harvard University Press
| location = Cambridge MA
| 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)
* {{cite book
| last = Kleene
| first = Stephen Cole
| title = Introduction to Metamathematics
| year = 1952, 10th impression with 1971 corrections
| publisher = North Holland Publishing Company
| location = Amsterdam NY
| 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 ==

{{cite web |last=Farmer |first=W. M |title=Propositional logic |url=http://imps.mcmaster.ca/courses/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]]).

{{DEFAULTSORT:Hilbert System}}
[[Category:Proof theory]]
[[Category:Logical calculi]]
[[Category:Automated theorem proving]]

formulasearchengine - User contributions [en]

Enhanced vegetation index