Hilbert System - Formal Deductions

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 spiritual kinship between Lincoln and Whitman was founded upon their Americanism, their essential Westernism. Whitman had grown up without much formal education; Lincoln had scarcely any education. One had become the notable poet of the day; one the orator of the Gettsyburg Address. It was inevitable that Whitman as a poet should turn with a feeling of kinship to Lincoln, and even without any association or contact feel that Lincoln was his.
    Edgar Lee Masters (1869–1950)

    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)