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 is a set of formulas, considered as hypotheses. For example could be a set of axioms for group theory or set theory. The notation means that there is a deduction that ends with using as axioms only logical axioms and elements of . Thus, informally, 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. 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
is a generalization of .
Read more about this topic: Hilbert System
Famous quotes containing the words formal and/or deductions:
“The bed is now as public as the dinner table and governed by the same rules of formal confrontation.”
—Angela Carter (1940–1992)
“In the one instance, the dreamer ... loses sight of this object in a wilderness of deductions and suggestions ... until ... he finds the incitamentum, or first cause of his musings,... forgotten. In my case, the primary object was invariably frivolous, although assuming, through the medium of my distempered vision, a refracted and unreal importance.”
—Edgar Allan Poe (1809–1849)