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:
“As blacks, we need not be afraid that encouraging moral development, a conscience and guilt will prevent social action. Black children without the ability to feel a normal amount of guilt will victimize their parents, relatives and community first. They are unlikely to be involved in social action to improve the black community. Their self-centered personalities will cause them to look out for themselves without concern for others, black or white.”
—James P. Comer (20th century)
“The soul of Man must quicken to creation.
Out of the formless stone, when the artist united himself with stone,
Spring always new forms of life....”
—T.S. (Thomas Stearns)