Daniel Leivant, "Higher Order Logic." Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 2, p. 229-321.

Section 1: Introduction. He outlines what the next seven sections will cover. Sections 2-5 provide the "essential issues and facts of the topic." Sections 6-8 are more technical, dealing with restrictions of higher order logic, mathematical practice, and computation.

Section 2: The expressive power of second order logic. Second order logic (allowing quantifiers over relation and function variables) is introduced along with the idea of (standard) interpretations. Second order logic is contrasted with first order logic using standard examples. Finiteness is not first order definable (by compactness), but is second-order definable (by saying "all injective functions are surjective"). In fact, we can express each cardinal aleph_n using a second order formula. Similarly, we cannot characterize Ns (the natural numbers with zero and successor) up to isomorphism using first order logic, but can using a second order wff phi (using the intersection of Peano with second order induction--this characterization is attributed to Dedekind). Since we can define addition and multiplication using first-order formulas (conjoined to give D), we can determine the truth (in the standard model) of any wff psi in the language of PA by determining the validity of "phi and D imply psi." In fact, any free algebra is second order definable in an analogous way.

Other examples: Graph reachability is second order definable (by a single sentence), but not first order. We can assign each coherent equational program P over a free algebra A which describe a function f to a second order wff in such a way that the wff is valid iff the associated function is total. We cannot do the same in first order, because if we could then we could use it to enumerate the (codes of) total recursive functions--which is impossible by a diagonal argument.

Given the standard model of number theory with all total computable functions, a set is "arithmetical" if it is first order definable and "analytical" if it is second order definable. There are analytical sets which are not arithmetic [attributed to Kleene]. For example, consider the set of (codes of) sentences over a language containing 0, successor and finitely many functions which include those used to represent negation, disjunction, equality, universal quantification, and substitution in the coding of the language which are true in the standard model N of the language. This set is not arithmetical (by Tarski's Theorem). The set is analytical because we can write down in a wff what a relation would have to satisfy to include the codes of (first order) wff's paired with (finitely supported) assignments which satisfy the wff's in the model (the restriction to first order only becomes necessary because "coded" universal quantification is reflected by an actual universal quantifier). Then, a first order formula phi is true in N iff every such relation contains the pair <numeral(code(phi)),h> for every h (representing assignments). If phi is a sentence, we can replace h by 0 and forget quantifying over it. Also, since the functions we used are primitive recursive, we can provide definitions for them in the language of Ns (let D be the conjunction of these definitions) to obtain a second order truth definition in the language of Ns for first order truth in N.

Inductive definitions can be described as the inductive closure of an operator F on n-ary relations. Suppose F can be defined over a structure S expanded with an r-ary predicate symbol R (interpreted in the structure by Q). Then, the inductive closure of F is second order definable (since in second order we can describe a well ordering and use this to say that an r-tuple appears at some step in the ordinal induction). If F is a monotone operator (which is the case if R only appears positively in the definition of F--for first order definitions the converse holds), then the inductive closure is the least fixed point of F, and we can define the inductive closure using the more convenient method of intersecting fixed points.

Section 3: Canonical semantics of higher order logic. The standard (Tarskian) semantics of second order logic are given. While we can pass back and forth between functions and relations (by considering graphs), we can make finer distinctions by using only relations (namely, all Pi_1^1 sets are definable by formulas for the form "forall f exists x phi" [phi quantifier free] while sets definable by formulas of the form "forall R exists x phi" ["strict-Pi_1^1"/"computational"] are recursively enumerable [Kreisal 1968]--such formulas define the "operational semantics of a certain finite state machine" without depending upon a coding into the natural numbers).

Second order formulas can be transformed into prenex normal forms in the same way as first order formulas. Furthermore, we may ensure that second order quantifiers precede all first order quantifiers by adding the first order bound variables to the arguments of each second order bound variable which original followed them (though it requires a weak form of AC to prove the equivalence of these formulas). The same technique replaces any first order bound variables after the first [universal/existential] string of first order bound variables by second order bound variables preceding that first string. Using this normalization method, the classes Pi_m^1 [Sigma_m^1] are defined as the class of wff's in prenex normal form with m interchanges of second order quantifiers where the initial string of second order quantifiers is universal [existential]. Kleene proved that for each m > 0, there is a set Sm which is definable by a Pi_m^1 formula, but no Sigma_m^1 formula (hence no Pi{m-1}^1 formula). It follows that N-Sm is a set definable by a Sigma_m^1 formula, but no Pi_m^1 formula. In fact, Sm can be taken to be the "set of codes of Pi^1_m sentences that are true in N" (where N is as in the truth definition previously discussed). The same idea for a truth definition (restricting the number of quantifier interchanges) can be used to show this.

Finite order logic (omega-order logic, or type theory) [Church 1940] is introduced in the form of a relational variant [Schutte 1960] which is essentially Andrews F-omega. The standard interpretation is described. k'th order logic is defined by only allowing variables of type order k or less (note that he does not use the factor of 2 to distinguish between bound variables and free variables of different types). We can even extend to logics of transfinite ordinals [Andrews 1965] [Montague 1965a].

Church's formulation of functional types is described, using Currying [which he attributes to Curry instead of Schonfinkel). He claims "the well-known duality between functions and relations over basic objects extends to the entire type hierarchy," but only indicates that we can represent relations as functions to a propositional type o, and consider functions as their graph relations. He does not note that the arguments to a function may not be a relational type, as in a function of type i(ii).

Using the functional formulation, we can represent formulas as propositional functions. Here, the quantifiers are propositional functions. For each type a, we get a different universal quantifier (of type (o(oa))). In order to obtain a single universal quantifier, the type structure must be enriched, as in Girard's system F-omega in which forall [and exists] has the type "delta t. (t->o)->o." (In terms of the formulae-as-types paradigm this corresponds to having a type system with implication and universal quantification.) The functional formulation is the one used in many formal caculi in Computer Science and programming systems (namely, Calculus of Constructions, Edinburgh LEGO, Paulson's Isabelle, TPS, and Lambda-Prolog).

Using ideas similar to the truth definition given in second order logic for first order truth (in N), k'th order truth in N is k+1'st order definable [note: if the factor of two enters, this may become k+2'nd order definable]. There is no such k'th order truth definition, by the same diagonal argument for Tarski's Theorem given in first order. Also, there is no finite order truth definition in finite order logic. However, in transfinite type theory, finite order truth is definable [Andrews 1965].

Section 4: Proof theory. Second order validity (in the standard sense) is not second order definable, hence is not recursively enumerable. This is because second order truth of wff's in the language of PA in the standard model is reducible to validity of certain (effectively recognizable) second order wff's (using the fact that we can characterize the standard model in second order). Since second order validity (in the standard sense) is not recursively enumerable, we cannot have a complete, effective proof theory for second order logic, or any higher order logic which includes second order. However, we can extend the notion of provability in first order logic to the higher order setting by generalizing the quantifier rules and including axioms of comprehension (note that extensionality is not necessary because we are working with a relational formulation). The resulting system for n'th order logic is called L_n, and for finite order logic is called L_omega.

Comprehension (as a set existence principle) implies existence of the empty-set, union, separation and replacement. The power set is not guaranteed to exist in second order logic, but does exist as a set of higher type in finite order logic. The axiom of choice can be formulated (in various ways--giving the graph of a "choice" function) at arbitrary types. Choice can be reformulated as axioms of collection [Hilbert, Ackerman 1928].

We can also formulate intuitionistic proof calculi for higher order logics, by the usual restrictions, giving systems IL_n and IL_omega. We can interpret L_2 in IL_2 in the sense that for every phi we can form phi' ("by double-negating every atomic, disjunctive, and existential subformula of phi") so that L_2 proves phi<->phi' and L_2 proves phi iff IL_2 proves phi' (this process, where a judgement of phi' represents a judgement of the "pseudotruth" of phi, is attributed to Kolmogorov [1925]). Note that classical second order propositional logic (L_2^0) is decidable (in fact, is poly-space complete), but IL_2^0 is undecidable (in fact, provability in classical first order can be reduced to provability in IL_2^0). While, in first order constructive logic the logical constants {not, forall, exists, or, and, implies} are not interdefinable, in IL_2, they are all definable (including the constant false as "forall X X") in terms of implication and forall [Prawitz 1965] (which could have interesting implications w.r.t. the Curry-Howard correspondence [polymorphic lambda calculus!]).

Finally, we consider normalization (transformation of natural deduction proofs into those with no "detours," essentially nothing is introduced [generalized] and then eliminated [instantiated]) and cut-elimination (transformation of sequential proofs into those with no applications of cut). In higher order logic, eliminating detours of the form of relational universal generalization followed by a relational universal instantiation by substituting the instantiation throughout the derivation my replace one detour by larger ones. This complication prevents an induction on the syntactic size of formulas (as Gentzen did by using the "degree" [number of logical constants occurring in a formula] [recall that Gentzen did a double induction using "degree" and "rank"]). Despite this complication, Prawitz [1972] proved that every natural deduction proof in L_2 can be *effectively* normalized, and Martin-Lof [1973a] proved this for INTUITIONISTIC finite order logic. (Note that the fact that such proofs exist follow from the cut-elimination/Normal Form Theorems proven by Tait [1966] for second order and independently by Takahashi and Prawitz for finite order logic using 'partial valuations'--an idea attributed to Schutte [1960a]. [Also, Andrews proved cut elimination for Elementary Type Theory using Semantic Methods--Abstract Consistency and Smullyan's Unifying Principle.] The important difference is that the stronger results above give an effective transformation).

In first order logic, cut-elimination/normalization imply the important subformula property: "in a normal proof of a formula phi, every formula is a subformula of phi." Here, subformula is defined to include term substitutions. This bounds the logical complexity of formulas in a normal proof. However, in higher order logic, since term substitution for higher order variables can introduce arbitrarily more complicated formulas, the subformula property does not bound the complexity of formulas in a normal proof. [Think: primitive substitutions!]

Section 5: Ontology. There are many differences between first order and second order logic. The set of first order valid sentences is r.e., but the set of second order valid sentences (in the standard sense) is not even definable (not even in finite order logic [that is, there is no formula of finite order logic tau(x) so that every second order sentence phi is valid iff N|=tau(numeral(code(phi))) where N is the standard model with Di=naturals--contrast this with the fact that we can reduce finite order validity to validity of certain formulas in a second order theory]). First order logic is compact, but not second order. First order satisfies Upward and Downward Lowenheim-Skolem, but second order satisfies neither (consider that we can capture N and that we can express "at least aleph_n"). First order unification is decidable, but not second order unification. In first order, we have Fraisse's Theorem which states that properties of a model are first order definable iff "it can be recognized by a computation with a finite number of alternations between existential (nondeterministic) and universal (co-nondeterministic) guesses" [compare this to "finitely isomorphic" iff elementary equivalence for finite symbol sets]. Keissler has a result that relates first order definability to preservation under isomorphisms and ultraproducts. "First order logic satisfies a 0-1 law" which apparently means that if we count the number of non-isomorphic models of phi (over a language with no individual constants) of size n and divide by the total number of non-isomorphic such models of size n, and let n go to infinity, then the limit is 0 or 1. This fails in second-order because we can form a sentence which states "the universe is even."

In first order logic, the interpretation of the logical constants (including quantifiers) is invariant, while nonlogical constants is interpretation-dependent. Quine [1970] argued that logic should be ontologically neutral (not assume the existence of certain objects and structures). Once we lose ontological neutrality (by assuming infinity, for example), we have mathematics. Quine concludes that second order logic is a mathematical theory instead of a logic. This is supported by Lindstrom's Theorem which states that any logic satisfying compactness and downward Lowenheim-Skolem can be no stronger than first order logic. ("Compactness is the failure to distinguish between the finite and the infinite, and downwards Lowenheim-Skolem is the failure to distinguish between different infinities.") Girard suggested a logic must be cut-free and have no axioms (so there is no "communication" between formulas except by rules for the logical constants) [note that while we do have cut-elimination results for higher order logic, we certainly need axioms such as comprehension or lambda-conversion].

Hilbert and Ackerman [1928] noted, "the most basic notions of metamathematics of first order logic are second order" (since validity requires quantification over all universes). An alternative to second order logic is Henkin's partially ordered quantifiers. These can be used to capture infinity (by failure of the pigeonhole principle).

Henkin introduced a semantics for higher order logic in which the interpretation of quantifiers becomes interpretation-dependent. This is the notion of "general model" as in Andrews [1986], except for a relational formulation here. The Tarskian semantics corresponds to the special case of standard ("canonical") Henkin models. A Henkin-prestructure is a collection of appropriate domains for each type. A Henkin-structure is a prestructure closed under definability.

We can represent second order logic as a first order theory [this should not be surprising, since ZFC is a first order theory] and map any Henkin-prestructure to corresponding a first order model (in which individuals and sets and relations are all mapped to individuals, and we have predicates in the first order theory to distinguish them). A second order formula phi is true in a Henkin-prestructure H iff the corresponding first order sentence phi^S is true in the corresponding first order model S(H). It follows that if phi^S is valid, then phi is valid, but the converse fails because we may have first order models which do not correspond to Henkin-prestructures. We can overcome this difficulty by only considering models of the axioms of the first order theory (which all S(H) satisfy and which suffice to allow us to find a corresponding H for each first order model S). These axioms include V-correctness (to guarantee elements are well-typed), non-emptiness, disjointness, inclusion, elementhood, and extensionality. (Actually, if we drop inclusion we can still find an H for every S so that S(H) is a well-defined substructure of S. This is sufficient to obtain corresponding results for finite order logic.) Now we can say that every second order formula (he only works with monadic, but this is essentially unimportant) is true in all Henkin-prestructures iff the corresponding formula is true in all models of the theory above. We can also throw in comprehension axioms and we have that validity in Henkin-structures is equivalent to truth of the corresponding formula in all models this larger first order theory. We have corresponding results for finite order logic.

The principle of choice is not provable in L_2. He gives a proof of this by considering the Henkin structure with a three element universe and definable relations. Wait! How can this be? Aren't all finite models standard? Oh, but Henkin's proof that all finite models are standard makes heavy use of descriptions. His proof for L_2 assumes an empty signature (in particular, no descriptions).

The same construction which reduces finite order logic to a first order theory can be extended with second order (Pi^1_1) formulas which states that we have all relations. Any (standard) structure which satisfies the resulting second order theory would correspond to standard models of finite order logic. In fact, given any particular finite order logic formula phi, we can only consider the (finite number of) axioms concerning the types appearing in phi (to guarantee that these domains are standard) and obtain chi_phi. Thus, phi is valid [in the standard sense] iff the Sigma_1^1 formula "chi_phi implies phi^T" is valid [in the standard sense]. This should be contrasted with the fact that second order truth is not definable in second order logic (the difference being whether we consider all structures or just N). Now, we further have that second order truth is not definable even in finite order logic. (Suppose we had a finite order truth definition for second order logic. Then we could use it with the above results to obtain a finite order truth definition for finite order logic, contradicting Tarski's Theorem.)

Section 6: Restricted higher order logic. Higher order logic may be restricted in a number of ways. We may consider monadic second order logic (only allowing monadic relation [set] variables--note that we may have n-ary relation and function constants). Monadic first order logic and monadic second order logic without functions are both decidable. Monadic second order logic (with functions) permits the definition of N (since this second order definition is monadic). We can use this to show compactness fails, as do upward and downward Lowenheim-Skolem and Beth Definability. The set of valid monadic second order formulas is not analytical, hence not recursively enumerable. Certain monadic theories are decidable (e.g., the monadic second order theory of zero and successor [or even with two successors, giving binary trees]).

Another restriction is to consider first order logic with fixpoint operators, such as the least fixed point operator for monotone operators (where monotonicity is determined by a syntactic criteria such as requiring R to have only positive occurrences) giving FO-mu. We can express number theory in this language, from which it follows that the set of valid formulas is not arithmetical (hence, not recursively enumerable). Compactness and upward Lowenheim-Skolem fail, but FO-mu does satisfy downward Lowenheim-Skolem. First order deduction is supplemented with rules and axioms expressing that phi[mu[phi]](x) implies mu[phi](x) ("fixed point"), and [phi[psi](x) implies psi(x)] implies [mu[phi](x) implies psi(x)] ("least").

Another restriction is weak second order logic. Here we interpret quantification as being over finite sets and relations. We can still define the naturals (using an infinite number of formulas to express that s^n(x) is not x for each n) by a set Gamma. Graphs of primitive recursive functions can be defined. So, we can reduce truth of a first order number theoretic formula phi to Gamma |= phi in weak second order. The decision problem for f-validity is thus not arithmetical, hence not r.e. Also, we do not have upwards Lowenheim Skolem, compactness, but it does have downwards Lowenheim-Skolem. It follows that full second order logic cannot be interpreted in weak second order logic, and that f-validity of a second order formula is reducible to truth in N of a second order formula. We accomplish this by quantifying over all countable universes (up to isomorphism) by quantifying over subsets of N. It follows that the set of f-valid second order formulas is Pi_1^1. This should be contrasted with the set of valid second order formulas which is not even definable in finite order logic (type theory).

Finally, we may consider predicative logic (logic with restricted comprehension). Such logics arose due to the foundational crises created by the antimonies discovered at the turn of the century. One reaction was intuitionism (Brouwer). Another was the "predicativist program" which sought to restrict impredicative [a term attributed to Poincare 1910] definitions (those which define an object by referring to all objects in a collection which includes the one being defined). One option is to take a first order theory T and consider T^2, the second order theory with comprehension for first order formulas. T^2 is conservative over T (by considering a cut-free proof of a first order formula [which has the subformula property so that we can remove any second order formulas from the proof]). In fact, we can restrict comprehension to universal first order formulas (by performing comprehension at each step in the construction of the formula for which we really want comprehension). Using the same idea, if we are working with a finite vocabulary we can restrict ourselves to comprehension used to construct terms and formulas, and (an infinite number of) comprehension axioms used to rearrange arguments to relations (of each arity k). If we have pairing and projection functions, we can reduce the rearrangement comprehension axioms to those of arity 3. (These ideas show up in NGB set theory, where the second order comprehension axioms become first order class formation axioms--more on this is in Section 7.)

We can extend the logic further by stratifying abstraction into levels. We can allow comprehension first over first order formulas only. Then we can allow second order quantification over the relations defined by such comprehension and allow comprehension to get relations of the next higher level. This idea originated with Russell's Ramified Type Theory. This section gives a good intuitive feel for Ramified Type Theory. First, we consider finitely ramified second order logic [Church 1956]. Here we have second order variables ^l R^k of arity k and level l. The intended semantics is intertwined with the language. Each bound ^l R^k is interpreted as ranging over relations definable by a formula in which all variables are of level <= l (to actually specify this inductively, we must be more careful). Ramified finite order logic is more delicate. Each variable has a level and a type. The level of a formula is the least number (ordinal, in general) greater than the level of all bound variables and at least as large as the level of all free variables.

In the sense of Lindstrom's Theorem, Ramified Type Theory is equivalent to first order logic (i.e., Ramified Type Theory cannot distinguish between models if first order logic cannot). However, the higher order aspects do allow greater expressibility. Two examples (ramified second order number theory [in which we can quantify over first order definable relations] and ramified second order theory of dense linear orders) are listed.

Section 7: Mathematical practice. Although we can express second order notions in first order, it is at a cost. Jon Barwise is quoted [1985]: "As logicians, we do our subject a disservice by convincing others that logic is first order, and then convincing them that almost none of the concepts of modern mathematics can really be captured in first order logic."

A common method for handling second order axioms is to represent them as first order schemas. The most obvious examples are induction in PA and replacement in ZF. Given any first order theory T which is axiomatized by a finite number of axioms and by an axiom schema sigma[phi], we can let T^2 be the second order theory given by comprehension on first order formulas, the axioms above and the second order axiom "forall R sigma[R]." T^2 is conservative over T (this follows from the related result in the previous section).

Many first order theories axiomatized by such schemas cannot be finitely axiomatized in first order logic. Kreisel/Levy [1968] proved that if T is a first order theory that proves cut-elimination for first order logic (coded, of course), and if T has a provable truth definition for all formulas of complexity <= k (for each k), and if T proves induction for all formulas in the language, then T is not finitely axiomatizable. The idea is that if it were finitely axiomatizable, then we can reduce provability in the theory to validity of a formula (the axioms implying the original formula). We can bound the complexity of possible cut-free proofs of the formula, so that if there is no proof of that complexity then it is unprovable, allowing us to prove consistency of T. This contradicts Godel's Second Incompleteness Theorem. Both PA and ZF satisfy the conditions of this result, so that neither are finitely axiomatizable in first order logic. Also, PA [ZF] with an induction schema for all second order formulas is not a conservative extension of first order PA [ZF].

In Russell's Ramified Type Theory, there is no reason to stop iterating the power set operation at level omega. By continuing this iteration through "all" ordinals (collecting by union at limit ordinals), we obtain a set theoretical universe, which can be represented by a first order theory (such as ZF). So, consideration of higher order logic (which is needed for the higher order constructs of practical mathematics) leads to the notion of set theory as a first order theory. In second order ZF (with comprehension for first order formulas) we can talk about classes. This leads to "theories of classes" as in NBG set theory (where the second order character is hidden by rephrasing it as a first order theory). Allowing full comprehension for second order ZF gives theories such as those studied by Wang, Quine, Tarski, Kelley, and Morse. (The author calls such theories KM.) KM proves reflection for ZF, so is not a conservative extension of ZF and is not finitely axiomatizable.

The Montague-Levy reflection principle for set theory posits that if a formula phi is true in the universe of sets, then it is true if it is relativized to some universe V_alpha in the hierarchy. Such a principle implies the existence of large cardinals.

Infinite constructions in Analysis led to the canonical formulation as second order arithmetic [Hilbert and Bernays 1939]. (The idea of such a canonical formulation led Poincare to make the remark at the 1900 Congress of Mathematicians: "Today there remain in analysis only integers and finite or infinite systems [=sets] of integers . . . Mathematics has been arithmetized . . . We may say today that absolute rigor has been achieved." I find this last sentence amusing.) While today Analysis is formalized in set theory, some logicians advocate a more direct formalization in second order arithmetic [see Feferman 1977 for a survey of Analysis in finite order logic].

The desire to replace impredicative definitions in Analysis by predicative forms (or those which can be justified predicatively) led to predicative formalisms (such as Ramified Analysis, iterated comprehension, iterated inductive definitions, etc.). Such theories can be classified by their proof-theoretic strength (e.g., second order arithmetic with comprehension and induction for first order formulas is conservative over PA, and Zermelo set theory without the power set axiom is mutually interpretable with PA.)

The idea of predicatively justifying impredicative definitions relates to Hilbert's Program, which failed because "finitistic mathematics" [primitive recursiveness] is too weak.

The "degrees of predicativity" can be measured by proving certain theorems to be equivalent to impredicative axioms (such as AC). This is called "reverse mathematics."

Speedup:

Given two proof calculi F1 and F2, we can measure the proof speed-up of F2 over F1 by saying "F2 has a proof-length [size] speedup over F1 by a factor of h:N->N" if there is an infinite set of formulas Phi such that for every phi in Phi the length [size] of the shortest [smallest] proof of phi in F1 is greater than h of the length [size] of the shortest [smallest] proof of phi in F2]. Length is measured by the number of lines in the proof. Size is measured by the number of symbols. Note that there can only be a finite number of proofs of a given size [assuming a finite vocabulary].

Proof-size speedup (higher order arithmetic): For higher order arithmetic we can obtain amazing speedup.

If Z and Z' are sound extensions of PA, and Z' proves reflection for Z, then Z' has a proof-size speedup over Z of h for every computable (total) function h. (The author claims this implies PA_k+1 has such a speedup over PA_k.) This is proven by defining H to be total recursive so that H(n) > h(c+n) for all n>=c, for all c. We then form the formula phi(n) stating "phi('n') has no proof in Z smaller than H(n)" and consider the infinite collection of formulas phi('n'). Since Z' proves reflection for Z, we can formalize the proof that phi('n') must be true for each n and obtain a proof in Z' of "forall x phi(x)." Then each phi('n') is obtained by adding one line to the proof--giving a proof of size c+n. But, by the definition of phi, we know that the shortest proof of phi('n') >= H(n) > h(c+n) forall n>c.

Related results restricting our attention to Sigma_1^0 theorems, for Z and Z' as above, we have a proof-size speedup of a factor of h for Sigma_1^0 theorems for every provably recursive function h of Z' (not every recursive function as above), and this is the best we can expect [it's pretty good, right!] because whenever we get a speedup of a factor of h, h is majorized by a provably recursive function of Z'.

Proof-length speedup (higher order arithmetic): For each k, PA_k+1 has an unbounded speedup over PA_k (and this speedup is for Pi_1^0 formulas) [that is, there is an infinite set of formulas which require proofs of unbounded length in PA_k, but of a bounded length in PA_k+1].

Speedup of higher order logic: The speedup results for higher order logic are not as spectacular.

There is a provably recursive function h of third order arithmetic so that we cannot obtain a proof-size speedup of L_2 over L_1 by a factor of h. A similar result holds for proof-length. For finite order logic, there are actually linear functions h so that L_omega cannot have a proof-size or proof-length speedup over L_2 by a factor of h (for first order formulas!). If we consider second order formulas, then L_k+1 has a proof-size speedup over L_k of every recursive factor and an unbounded proof-length speedup. We also have that for every provably recursive function h of second order arithmetic, L_2 has a proof-size speedup over L_1 by a factor of h.

Section 8: Higher order logic in relation to computing and programming. Algol 60 was the first language which incorporated the entire type structure of finite order logic, with an explicit use of infinitely many types appearing first in Algol 68. Inheritance, subtypes and type intersection play a role in object oriented programming. Once we have types, we may treat them as data. Then the interplay between the two roles of types (as notations for functional behavior and as data) becomes involved. We may have types depend on objects (dependent types) as in Martin-Lof [1973b] type theory and AUTOMATH [Bruijn, 1980]. We may also have polymorphism, so that the type structure is enhanced with a "forall" operator and terms with such types must be first applied to types before being applied to terms. (Without some kind of polymorphism, we cannot define a single identity function for all types.) Both polymorphism and dependent types are merged in the Calculus of Constructions [Coquand, Huet]. Another use of higher order data is in database theory.

The Curry-Howard correspondence is described. One example is given in some detail: the duality of ML^0_2 (minimal second order propositional logic) and Girard-Reynolds second order lambda calculus is described. The point is that natural deduction derivations correspond to lambda term constructions [see Hindley 1997 for more details]. Note that normalization of natural deduction proofs corresponds to beta-reduction (of terms for modus ponens and of polymorphic types for universal generalization followed by instantiation).

Initial research in automated theorem proving was only in first-order logic. Andrews extended this to the higher order case using extensions of syntactic theorems of first order to higher order (cut elimination/normalization [Takahashi, 1967; Girard, 1972; Prawitz, 1968, 1972; Andrews, 1971], resolution [Andrews, 1971], Skolemization [Miller 1987], unification [Huet, 1975], and Herbrand's Theorem [Miller, 1987]). This research has led to the development of interactive software environments for the full formalization of mathematics. It has also led to research in logical frameworks (an example of "meta-programming").

Many computational complexity classes can be characterized by expressibility in certain classes of higher order formulas, and by function provability in higher order logics. Fagin's Theorem [1974] relates NP to definability by a purely existential second order formula. P and NL can be related to universal second order formulas with certain restrictions on the matrix. P-space and Exp can be characterized in third order logic. And definability in full finite order logic characterizes computability within "Kalmar-elementary resources" (i.e., "using time and space with is k-fold exponential in the size of the input, for some k [Leivant, 1987]"). Also, P is characterized by definability in FO-mu.

Another approach involves using proof-theory to characterize computational complexity classes. Given a formalism L for second order logic, we say a function f over a free algebra A is "provable in L" iff "it is computed by some coherent equational program (P,f) such that L proves A(x) implies A(f(x)) from the universal closures of the defining formulas in P." Now, for any collection of second order formulas Phi, let L_2(Phi) by second order logic with comprehension axioms for Phi. We can calibrate the computational complexity of f by asking how large Phi must be so that f is provable in L_2(Phi). "L_2(all second order formulas) gives precisely the provably-recursive functions of second order arithmetic." Comprehension for first order formulas gives the Kalmar-elementary functions. P is characterized using comprehension for positive existential formulas.