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:
“If we focus exclusively on teaching our children to read, write, spell, and count in their first years of life, we turn our homes into extensions of school and turn bringing up a child into an exercise in curriculum development. We should be parents first and teachers of academic skills second.”
—Neil Kurshan (20th century)