Consistency, Completeness, and Normal Forms
A theory is said to be consistent if falsehood is not provable (from no assumptions) and is complete if every theorem is provable using the inference rules of the logic. These are statements about the entire logic, and are usually tied to some notion of a model. However, there are local notions of consistency and completeness that are purely syntactic checks on the inference rules, and require no appeals to models. The first of these is local consistency, also known as local reducibility, which says that any derivation containing an introduction of a connective followed immediately by its elimination can be turned into an equivalent derivation without this detour. It is a check on the strength of elimination rules: they must not be so strong that they include knowledge not already contained in its premises. As an example, consider conjunctions.
| ------ u ------ w A true B true ------------------ ∧I A ∧ B true ---------- ∧E1 A true | ⇒ | ------ u A true |
Dually, local completeness says that the elimination rules are strong enough to decompose a connective into the forms suitable for its introduction rule. Again for conjunctions:
| ---------- u A ∧ B true | ⇒ | ---------- u ---------- u A ∧ B true A ∧ B true ---------- ∧E1 ---------- ∧E2 A true B true ----------------------- ∧I A ∧ B true |
These notions correspond exactly to β-reduction (beta reduction) and η-conversion (eta conversion) in the lambda calculus, using the Curry–Howard isomorphism. By local completeness, we see that every derivation can be converted to an equivalent derivation where the principal connective is introduced. In fact, if the entire derivation obeys this ordering of eliminations followed by introductions, then it is said to be normal. In a normal derivation all eliminations happen above introductions. In most logics, every derivation has an equivalent normal derivation, called a normal form. The existence of normal forms is generally hard to prove using natural deduction alone, though such accounts do exist in the literature, most notably by Dag Prawitz in 1961; see his book Natural deduction: a proof-theoretical study, A&W Stockholm 1965, no ISBN. It is much easier to show this indirectly by means of a cut-free sequent calculus presentation.
Read more about this topic: Natural Deduction
Famous quotes containing the words normal and/or forms:
“Normality highly values its normal man. It educates children to lose themselves and to become absurd, and thus to be normal. Normal men have killed perhaps 100,000,000 of their fellow normal men in the last fifty years.”
—R.D. (Ronald David)
“The delicious faces of children, the beauty of school-girls, “the sweet seriousness of sixteen,” the lofty air of well-born, well-bred boys, the passionate histories in the looks and manners of youth and early manhood, and the varied power in all that well-known company that escort us through life,—we know how these forms thrill, paralyze, provoke, inspire, and enlarge us.”
—Ralph Waldo Emerson (1803–1882)