First and Higher-order Extensions
The logic of the earlier section is an example of a single-sorted logic, i.e., a logic with a single kind of object: propositions. Many extensions of this simple framework have been proposed; in this section we will extend it with a second sort of individuals or terms. More precisely, we will add a new kind of judgement, "t is a term" (or "t term") where t is schematic. We shall fix a countable set V of variables, another countable set F of function symbols, and construct terms as follows:
| v ∈ V ------ var-F v term | f ∈ F t1 term t2 term ... tn term ------------------------------------------ app-F f (t1, t2, ..., tn) term |
For propositions, we consider a third countable set P of predicates, and define atomic predicates over terms with the following formation rule:
| φ ∈ P t1 term t2 term ... tn term ------------------------------------------ pred-F φ (t1, t2, ..., tn) prop |
In addition, we add a pair of quantified propositions: universal (∀) and existential (∃):
| ------ u x term ⋮ A prop ---------- ∀Fu ∀x. A prop | ------ u x term ⋮ A prop ---------- ∃Fu ∃x. A prop |
These quantified propositions have the following introduction and elimination rules.
| ------ u a term ⋮ A true ------------ ∀Iu, a ∀x. A true | ∀x. A true t term -------------------- ∀E A true | |
| A true ------------ ∃I ∃x. A true | ------ u ------------ v a term A true ⋮ ∃x. A true C true -------------------------- ∃Ea, u,v C true |
In these rules, the notation A stands for the substitution of t for every (visible) instance of x in A, avoiding capture; see the article on lambda calculus for more detail about this standard operation. As before the superscripts on the name stand for the components that are discharged: the term a cannot occur in the conclusion of ∀I (such terms are known as eigenvariables or parameters), and the hypotheses named u and v in ∃E are localised to the second premise in a hypothetical derivation. Although the propositional logic of earlier sections was decidable, adding the quantifiers makes the logic undecidable.
So far the quantified extensions are first-order: they distinguish propositions from the kinds of objects quantified over. Higher-order logic takes a different approach and has only a single sort of propositions. The quantifiers have as the domain of quantification the very same sort of propositions, as reflected in the formation rules:
| ------ u p prop ⋮ A prop ---------- ∀Fu ∀p. A prop | ------ u p prop ⋮ A prop ---------- ∃Fu ∃p. A prop |
A discussion of the introduction and elimination forms for higher-order logic is beyond the scope of this article. It is possible to be in between first-order and higher-order logics. For example, second-order logic has two kinds of propositions, one kind quantifying over terms, and the second kind quantifying over propositions of the first kind.
Read more about this topic: Natural Deduction
Famous quotes containing the word extensions:
“The psychological umbilical cord is more difficult to cut than the real one. We experience our children as extensions of ourselves, and we feel as though their behavior is an expression of something within us...instead of an expression of something in them. We see in our children our own reflection, and when we don’t like what we see, we feel angry at the reflection.”
—Elaine Heffner (20th century)