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:
“Freedom is poetry, taking liberties with words, breaking the rules of normal speech, violating common sense. Freedom is violence.”
—Norman O. Brown (b. 1913)
“The most passionate, consistent, extreme and implacable enemy of the Enlightenment and ... all forms of rationalism ... was Johann Georg Hamann. His influence, direct and indirect, upon the romantic revolt against universalism and scientific method ... was considerable and perhaps crucial.”
—Isaiah Berlin (b. 1909)