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:
“We have been weakened in our resistance to the professional anti-Communists because we know in our hearts that our so-called democracy has excluded millions of citizens from a normal life and the normal American privileges of health, housing and education.”
—Agnes E. Meyer (1887–1970)
“The failure of women to produce genius of the first rank in most of the supreme forms of human effort has been used to block the way of all women of talent and ambition for intellectual achievement.”
—Anna Garlin Spencer (1851–1931)