A Hilbert system is a style (formulation) of deductive system that emphasizes the role played by the axioms in the system. Typically, a Hilbert system has many axiom schemes, but only a few, sometimes one, rules of inference. As such, a Hilbert system is also called an axiom system. Below we list three examples of axiom systems in mathematical logic:
(classical predicate logic without equality)
rules of inference:
modus ponens, and
generalization: from , we may infer , where is free for in
(S4 modal propositional logic)
where above are well-formed formulas, are individual variables, and are binary, unary, and nullary logical connectives in the respective logical systems. The connective may be defined as for any formula .
Hilbert systems need not be unique for a given logical system. For example, see this link (http://planetmath.org/LogicalAxiom).
Since axioms are semantically valid statements, the use of Hilbert systems is more about deriving other semantically valid statements, or theorems, and less about the syntactical analysis of deductions themselves. Outside of structural proof theory, deductive systems a la Hilbert style are used almost exclusively everywhere in mathematics.
|Date of creation||2013-03-22 19:13:14|
|Last modified on||2013-03-22 19:13:14|
|Last modified by||CWoo (3771)|