HOME

TheInfoList



OR:

:''In
mathematical physics Mathematical physics refers to the development of mathematics, mathematical methods for application to problems in physics. The ''Journal of Mathematical Physics'' defines the field as "the application of mathematics to problems in physics and t ...
, ''Hilbert system'' is an infrequently used term for a physical system described by a
C*-algebra In mathematics, specifically in functional analysis, a C∗-algebra (pronounced "C-star") is a Banach algebra together with an involution satisfying the properties of the adjoint. A particular case is that of a complex algebra ''A'' of continu ...
.'' In
logic Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premis ...
, especially
mathematical logic Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal ...
, a Hilbert system, sometimes called Hilbert calculus, Hilbert-style deductive system or Hilbert–Ackermann system, is a type of system of formal deduction attributed to
Gottlob Frege Friedrich Ludwig Gottlob Frege (; ; 8 November 1848 – 26 July 1925) was a German philosopher, logician, and mathematician. He was a mathematics professor at the University of Jena, and is understood by many to be the father of analytic ph ...
Máté & Ruzsa 1997:129 and David Hilbert. These
deductive system A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A fo ...
s are most often studied for
first-order logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quanti ...
, 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 A trade-off (or tradeoff) is a situational decision that involves diminishing or losing one quality, quantity, or property of a set or design in return for gains in other aspects. In simple terms, a tradeoff is where one thing increases, and anot ...
between logical axioms and
rules of inference In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of ...
. 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 In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of ...
. Systems of
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 Hilbert-style systems, which instead use a ...
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 Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations ...
s or two with
generalisation A generalization is a form of abstraction whereby common properties of specific instances are formulated as general concepts or claims. Generalizations posit the existence of a domain or set theory, set of elements, as well as one or more commo ...
, to handle
predicate logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quanti ...
s, 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 A uniform is a variety of clothing worn by members of an organization while participating in that organization's activity. Modern uniforms are most often worn by armed forces and paramilitary organizations such as police, emergency services, ...
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 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 Hilbert-style systems, which instead use a ...
and
sequent calculus In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology ...
contain some context-changing rules. Thus, if one is interested only in the derivability of tautologies, no hypothetical judgments, then one can formalize the Hilbert system in such a way that its rules of inference contain only
judgment Judgement (or US spelling judgment) is also known as '' adjudication'', which means the evaluation of evidence to make a decision. Judgement is also the ability to make considered decisions. The term has at least five distinct uses. Aristotle s ...
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

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 \Gamma is a set of formulas, considered as hypotheses. For example, \Gamma could be a set of axioms for
group theory In abstract algebra, group theory studies the algebraic structures known as group (mathematics), groups. The concept of a group is central to abstract algebra: other well-known algebraic structures, such as ring (mathematics), rings, field ...
or
set theory Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly concer ...
. 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. 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; for example \forall y ( \forall x Pxy \to Pty) is a generalization of \forall x Pxy \to Pty.


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 \lnot and \to and only the quantifier \forall. Later we show how the system can be extended to include additional logical connectives, such as \land and \lor, 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. \phi \to \phi :P2. \phi \to \left( \psi \to \phi \right) :P3. \left( \phi \to \left( \psi \rightarrow \xi \right) \right) \to \left( \left( \phi \to \psi \right) \to \left( \phi \to \xi \right) \right) :P4. \left ( \lnot \phi \to \lnot \psi \right) \to \left( \psi \to \phi \right) The axiom P1 is redundant, as it follows from P3, P2 and modus ponens (see
proof Proof most often refers to: * Proof (truth), argument or sufficient evidence for the truth of a proposition * Alcohol proof, a measure of an alcoholic drink's strength Proof may also refer to: Mathematics and formal logic * Formal proof, a con ...
). These axioms describe classical propositional logic; without axiom P4 we get positive implicational logic. Minimal logic is achieved either by adding instead the axiom P4m, or by defining \lnot \phi as \phi \to \bot. :P4m. \left( \phi \to \psi \right) \to \left(\left(\phi \to \lnot \psi \right) \to \lnot \phi \right)
Intuitionistic logic Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, system ...
is achieved by adding axioms P4i and P5i to positive implicational logic, or by adding axiom P5i to minimal logic. Both P4i and P5i are theorems of classical propositional logic. :P4i. \left(\phi \to \lnot \phi\right) \to \lnot \phi :P5i. \lnot\phi \to \left( \phi \to \psi \right) Note that these are axiom schemes, which represent infinitely many specific instances of axioms. For example, P1 might represent the particular axiom instance p \to p , or it might represent \left( p \to q \right) \to \left( p \to q \right) : the \phi 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 A uniform is a variety of clothing worn by members of an organization while participating in that organization's activity. Modern uniforms are most often worn by armed forces and paramilitary organizations such as police, emergency services, ...
(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 \phi(p) be a formula with one or more instances of the propositional variable p, and let \psi be another formula. Then from \phi(p), infer \phi(\psi). The next three logical axiom schemes provide ways to add, manipulate, and remove universal quantifiers. :Q5. \forall x \left( \phi \right) \to \phi :=t/math> where ''t'' may be substituted for ''x'' in \,\!\phi :Q6. \forall x \left( \phi \to \psi \right) \to \left( \forall x \left( \phi \right) \to \forall x \left( \psi \right) \right) :Q7. \phi \to \forall x \left( \phi \right) where ''x'' is not free in \phi. These three additional rules extend the propositional system to axiomatise
classical predicate logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
. Likewise, these three rules extend system for intuitionstic propositional logic (with P1-3 and P4i and P5i) to
intuitionistic predicate logic In the philosophy of mathematics, intuitionism, or neointuitionism (opposed to preintuitionism), is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of fu ...
. Universal quantification is often given an alternative axiomatisation using an extra rule of generalisation (see the section on Metatheorems), in which case the rules Q6 and Q7 are redundant. The final axiom schemes are required to work with formulas involving the equality symbol. :I8. x = x for every variable ''x''. :I9. \left( x = y \right) \to \left( \phi :=x\to \phi :=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 In mathematical logic, a deduction theorem is a metatheorem that justifies doing conditional proofs—to prove an implication ''A'' → ''B'', assume ''A'' as an hypothesis and then proceed to derive ''B''—in systems that do not have an ...
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 Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises ...
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 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 Hilbert-style systems, which instead use a ...
.


Existential quantification

* Introduction : \forall x(\phi \to \exists y(\phi :=y) * Elimination : \forall x(\phi \to \psi) \to \exists x(\phi) \to \psi where x is not a
free variable In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a free variable is a notation (symbol) that specifies places in an expression where substitution may take place and is n ...
of \psi.


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 In mathematical logic, a deduction theorem is a metatheorem that justifies doing conditional proofs—to prove an implication ''A'' → ''B'', assume ''A'' as an hypothesis and then proceed to derive ''B''—in systems that do not have an ...
: \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 A generalization is a form of abstraction whereby common properties of specific instances are formulated as general concepts or claims. Generalizations posit the existence of a domain or set of elements, as well as one or more common character ...
: If \Gamma \vdash \phi and ''x'' does not occur free in any formula of \Gamma then \Gamma \vdash \forall x \phi.


Some useful theorems and their proofs

Following are several theorems in propositional logic, along with their proofs (or links to these proofs in other articles). Note that since (P1) itself can be proved using the other axioms, in fact (P2), (P3) and (P4) suffice for proving all these theorems. :(HS1) (q \to r) \to ((p \to q) \to (p \to r)) -
Hypothetical syllogism In classical logic, a hypothetical syllogism is a valid argument form, a syllogism with a conditional statement for one or both of its premises. An example in English: :If I do not wake up, then I cannot go to work. :If I cannot go to work, th ...
, see
proof Proof most often refers to: * Proof (truth), argument or sufficient evidence for the truth of a proposition * Alcohol proof, a measure of an alcoholic drink's strength Proof may also refer to: Mathematics and formal logic * Formal proof, a con ...
. :(L1) p \to ((p \to q) \to q) - proof: ::(1) ((p \to q) \to (p \to q)) \to (((p \to q) \to p) \to ((p \to q) \to q))       (instance of (P3)) ::(2) (p \to q) \to (p \to q)       (instance of (P1)) ::(3) ((p \to q) \to p) \to ((p \to q) \to q)       (from (2) and (1) by modus ponens) ::(4) (((p \to q) \to p) \to ((p \to q) \to q)) \to ((p \to ((p \to q) \to p)) \to (p \to ((p \to q) \to q)))       (instance of (HS1)) ::(5) (p \to ((p \to q) \to p)) \to (p \to ((p \to q) \to q))       (from (3) and (4) by modus ponens) ::(6) p \to ((p \to q) \to p)       (instance of (P2)) ::(7) p \to ((p \to q) \to q)       (from (6) and (5) by modus ponens) The following two theorems are known together as Double negation: : (DN1) \neg \neg p \to p : (DN2) p \to \neg \neg p : See proofs. :(L2) (p \to (q \to r)) \to (q \to (p \to r)) - for this proof we use the method of the hypothetical syllogism metatheorem as a shorthand for several proof steps: ::(1) (p \to (q \to r)) \to ((p \to q) \to (p \to r))       (instance of (P3)) ::(2) ((p \to q) \to (p \to r)) \to ((q \to (p \to q)) \to (q \to (p \to r)))       (instance of (HS1)) ::(3) (p \to (q \to r)) \to ((q \to (p \to q)) \to (q \to (p \to r)))       (from (1) and (2) using the hypothetical syllogism metatheorem) ::(4) ((p \to (q \to r)) \to ((q \to (p \to q)) \to (q \to (p \to r)))) \to (((p \to (q \to r)) \to (q \to (p \to q))) \to ((p \to (q \to r)) \to (q \to (p \to r))))       (instance of (P3)) ::(5) ((p \to (q \to r)) \to (q \to (p \to q))) \to ((p \to (q \to r)) \to (q \to (p \to r)))       (from (3) and (4) using modus ponens) ::(6) q \to (p \to q)       (instance of (P2)) ::(7) (q \to (p \to q)) \to ((p \to (q \to r)) \to (q \to (p \to q)))       (instance of (P2)) ::(8) (p \to (q \to r)) \to (q \to (p \to q))       (from (6) and (7) using modus ponens) ::(9) (p \to (q \to r)) \to (q \to (p \to r))       (from (8) and (5) using modus ponens) :(HS2) (p \to q) \to ((q \to r) \to (p \to r)) - an alternative form of the
hypothetical syllogism In classical logic, a hypothetical syllogism is a valid argument form, a syllogism with a conditional statement for one or both of its premises. An example in English: :If I do not wake up, then I cannot go to work. :If I cannot go to work, th ...
. proof: ::(1) (q \to r) \to ((p \to q) \to (p \to r))       (instance of (HS1)) ::(2) ((q \to r) \to ((p \to q) \to (p \to r))) \to ((p \to q) \to ((q \to r) \to (p \to r)))       (instance of (L2)) ::(3) (p \to q) \to ((q \to r) \to (p \to r)) (from (1) and (2) by modus ponens) :(TR1) (p \to q) \to (\neg q \to \neg p) - Transposition, see
proof Proof most often refers to: * Proof (truth), argument or sufficient evidence for the truth of a proposition * Alcohol proof, a measure of an alcoholic drink's strength Proof may also refer to: Mathematics and formal logic * Formal proof, a con ...
(the other direction of transposition is (P4)). :(TR2) (\neg p \to q) \to (\neg q \to p) - another form of transposition; proof: ::(1) (\neg p \to q) \to (\neg q \to \neg \neg p)       (instance of (TR1)) ::(2) \neg \neg p \to p       (instance of (DN1)) ::(3) (\neg \neg p \to p) \to ((\neg q \to \neg \neg p) \to (\neg q \to p))       (instance of (HS1)) ::(4) (\neg q \to \neg \neg p) \to (\neg q \to p)       (from (2) and (3) by modus ponens) ::(5) (\neg p \to q) \to (\neg q \to p)       (from (1) and (4) using the hypothetical syllogism metatheorem) :(L3) (\neg p \to p) \to p - proof: ::(1) \neg p \to (\neg \neg (q \to q) \to \neg p)       (instance of (P2)) ::(2) (\neg \neg (q \to q) \to \neg p) \to (p \to \neg (q \to q))       (instance of (P4)) ::(3) \neg p \to (p \to \neg (q \to q))       (from (1) and (2) using the hypothetical syllogism metatheorem) ::(4) (\neg p \to (p \to \neg (q \to q))) \to ((\neg p \to p) \to (\neg p \to \neg (q \to q)))       (instance of (P3)) ::(5) (\neg p \to p) \to (\neg p \to \neg (q \to q))       (from (3) and (4) using modes ponens) ::(6) (\neg p \to \neg (q \to q)) \to ((q \to q) \to p)       (instance of (P4)) ::(7) (\neg p \to p) \to ((q \to q) \to p)       (from (5) and (6) using the hypothetical syllogism metatheorem) ::(8) q \to q       (instance of (P1)) ::(9) (q \to q) \to (((q \to q) \to p) \to p)       (instance of (L1)) ::(10) ((q \to q) \to p) \to p       (from (8) and (9) using modes ponens) ::(11) (\neg p \to p) \to p       (from (7) and (10) using the hypothetical syllogism metatheorem)


Alternative axiomatizations

The axiom 3 above is credited to
Łukasiewicz Łukasiewicz is a Polish surname. It comes from the given name Łukasz (Lucas). It is found across Poland, particularly in central regions. It is related to the surnames Łukaszewicz and Lukashevich. People * Antoni Łukasiewicz (born 1983), ...
.A. Tarski, Logic, semantics, metamathematics, Oxford, 1956 The original system by Frege had axioms P2 and P3 but four other axioms instead of axiom P4 (see Frege's propositional calculus).
Russell Russell may refer to: People * Russell (given name) * Russell (surname) * Lady Russell (disambiguation) * Lord Russell (disambiguation) Places Australia *Russell, Australian Capital Territory *Russell Island, Queensland (disambiguation) **Ru ...
and 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 In the philosophy of mathematics, intuitionism, or neointuitionism (opposed to preintuitionism), is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of fu ...
), correspond to
combinatory logic Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of compu ...
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 In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relat ...
.


See also

*
List of Hilbert systems This article contains a list of sample Hilbert-style deductive systems for propositional logics. Classical propositional calculus systems Classical propositional calculus is the standard propositional logic. Its intended semantics is bivalen ...
*
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 Hilbert-style systems, which instead use a ...


Notes


References

* * * * It is a Hungarian translation of
Alfred Tarski Alfred Tarski (, born Alfred Teitelbaum;School of Mathematics and Statistics, University of St Andrews ''School of Mathematics and Statistics, University of St Andrews''. January 14, 1901 – October 26, 1983) was a Polish-American logician ...
'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: ** ** 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) * **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

* * It describes (among others) a part of the Hilbert-style deduction system (restricted to
propositional calculus Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations ...
). {{DEFAULTSORT:Hilbert System Proof theory Logical calculi Automated theorem proving