How to Prove Higher Order Theorems in First Order Logic

1 Introduction

First order logic is a powerful tool for expressing and proving mathematical facts. Nevertheless higher order expressions are often better suited for the representation of mathematics and in fact almost all mathematical text books rely on some higher order fragments for expres­ siveness. In order to prove such theorems mechanically there are two options: either to have a theorem prover for higher order logic such as TPS [Andrews et al., 1990] or to translate the higher order constructs into corre­ sponding first order expressions and to use a first order theorem prover. As important as the first development is - which may be the way of the future - we follow the secon.d approach because strong first order theorem provers are available today.

The Limitations of First Order Logic

First order logic and the set theories of ZERMELO­ FRAENKEL or VON NEUMANN-GODEL-BERNAYS have been developed for the formalization of mathematical concepts and for reasoning about them. Other ap­ proaches are RUSSEL'S ramified theory of types and CHURCH's simple theory of types which formalize higher order logic. Mathematicians use a (compared to the formal approaches) informal te.chnical language "th~.t i,~ much closer to higher order log1c augmented by na1ve set theory than to first order logic. They know about the antinomies and avoid them, for example by the omission of expressions like "{ zlz fl. z }". They also know that there is a (hopefully) clean foundation of set theory, how this is done in detail is in general however not of much interest to a working mathematician (if he is not work­ ing on the foundations of mathematics like logic or set theory).

Formal set theory is of course a very strong tool, es­ pecially when higher concepts are introduced by abbre­ viations. Beginning with the binary relation "E" one can (and this is really done by N. BoURBAKI) define the concepts subset, intersection, union, function, relation, power set, and so on. The definition of a function as a left-total, right-unique relation is rather complex and remote from the construct of a function symbol that is provided originally in logic in order to express functions. The representation of concepts using functions is more adequate in a higher order language. For instance in higher order logic it is possible to write:

V + commutative(+) {::::::> Vz, y z + y = y + z or VP symmetric(P) {::::::> (Vz, y P(z, y) ===? P(y, z)) . Here P is a predicate variable, and symmetric is a predi­ cate constant, which expects a predicate term as its argu­ ment. This cannot be written immediately in first order logic, because we quantify over P, so P would have t~ be a variable. On the other hand it must be a predi­ cate because of the expression P(z, y), hence a predicate variable, and this is excluded in first order logic. Nev~r­ theless this definition is expressable in first order log1c. Many concepts cannot be axiomatized in first order logic at all, for example the set N of natural numbers is not first order characterizable: the induction axiom is second order. Another example of the inadequacy of first order logic comes from the theorem of LOWENHEIM-SKOLEM: For instance every first order axiomatization of the real numbers R has a countable model.

Why and How Translation

Representing knowledge in an adequate way - adequate with respect to the naturalness of the representation of the object - is one thing, the other thing is to have an adequate and strong form of reasoning. If one uses higher order logic there are two possibilities: either to build strong higher order theorem provers or to translate into first order logic. We shall follow the second approach in this paper.

1.1 Example: A common translation of our formula above in a first order logic is:

VP symmetric(P) {:::::::}

(Vx, y apply(P, x, y) => apply(P, y, x))

apply is a predicate; it is interpreted freely, although it is intended that it is true exactly when P holds for the other arguments.

The following problems occur:

• Under what conditions can such a translation be correct? That is, if we translate a formula and we obtain a tautology, when is the original formula a tautology too?
• In what sense can such a translation be complete? That is, if we translate a tautology, do we always obtain a tautology?

For general considerations concerning the expressive­ ness of higher order logic, it is obvious that if we find a translation from higher order to first order logic, it cannot be complete in the general sense, especially since the theorem of LOWENHEIM-SKOLEM must hold and be­ cause of GODEL's incompleteness result . In principle such a translation must be equivalent to some set the­ oretical formulation as stated in MosTOWSKI's isomor­ phism theorem [Mostowski, 1949].

Related Work

J . VAN BENTHEM and K. DOETS [1983] give a transla­ t ion of a restricted higher order logic without function symbols and without higher order constants and identi­ ties to a standard first order logic. They introduce the general idea of a translation, and its soundness and com­ pleteness. The translation to standard first order logic leads to more complicated formulae than the translation to a sorted version, because it is necessary to relativize quantification with respect to the corresponding type.

Of great influence for the present paper are the trans­ lation techniques of H. J . 0HLBACH [1989], who trans­ lates modal logics and other non-classical logics to a context logic, where contexts are restricted higher order expressions. These contexts are translated to an order sorted first order logic.

Here a translation of (almost) full higher order logic with function symbols to a many sorted first order logic with equality is given. We do not need a general order sorted logic as long as we do not use a sorted higher order source logic.

2 Higher Order Logic

In this section we define formally a higher order logic based on CHURCH's simple theory of types, much of the notation is taken from [Andrews, 1986]. However, we shall write the types in a different way. For example if P is a binary predicate symbol on individuals, we write its type as (t XL- o) instead of (ou) for better readability. Apologies to all who are familiar with CHURCH's original notation.

The Syntax

Let us introduce type symbols first, then define terms and formulae for the logics cw. The n-th order predicate logics en are then defined as subsets of c.w.

2.1 Definition (Types of c.w): t is a type of order 0 that denotes the type of the individuals. o is a type of order 1 and denotes the type of the truth values. If r1 , . . . , T m, and u are type symbols not equal to o (with m ~ 1) then (r1 X .. · x Tm - u) is a type of order 1 + maximum of the orders of Tt, . . · , T m, u. It denotes the type of m-ary functions with arguments of types r1 , ... ,Tm, respectively, and value of type u . If Tt, . . . , Tm are type symbols not equal too (with m ~ 1) then (r1 x · · · x Tm - o) is a type of order 1 + max­ imum of the orders of r1 , .. . , T m. It denotes the type of m-ary predicates with arguments of types Tt, . ·. , T m , respectively.

2.2 Definition (Signature of cw): The signature of a logic in cw is a set s = u,. s~on·t u u,. s;ar where each set s~on·t is a (possibly empty) set of constant symbols of type T and s;ar a countable infinite set of variable symbols of type T. We assume that the sets S,. are all disjoint, in addition we sometimes mark the elements of a set S,. by its type T as index. A logic in c.w is defined by its signatureS and is denoted c.w(S) . If there is only one signature we often write c.w instead of cw(s) .

2.3 Definition (Terms of cw):

1. Every variable or constant of a type T is a term.
2. If f(r 1 x···xr,.-+t7)> t,. 1 , ··· , t,.,. are terms of the types indicated by their subscripts, then we get a term of type u by !(r 1 x .. ·xr,.-+t7)(t,. 1 , · · · ,t,..,.) .

2.4 Definition (Formulae of cw):

1. Every term of type o is a formula.
2. If I{) and t/J are formulae and x is a variable of any type, then (-.1{)), (IP 1\ t/J), and (Vx~P) are formulae.

2.5 Definition(Cn, for n ~ 1): C. 2 n is a subset of cw so that every variable and every constant is of order less or equal to n, C 2 n-l is a subset of C. 2 n such that no variable of order n is quantified.

The Semantics

The standard semantics is due to TARSKI and has been extended by HENKIN [1950] to the general model seman­ tics, we shall follow these concepts.

We use the following notation: Let At, ... , Am, and B be sets, then .1"( A1, . .. , Am; B) denotes the set of all functions from A1 x · · · x Am to B.

2.6 Definition:

• A frame is a collection {'D,. },. of nonempty sets 1J,. , one for each type T, such that 1J0 = {T,F} and 1Jc,..x .. ·xr.,. ..... t7) ~ .1"(1J,.., ... ,1J,.,..;1Jt7)· The mem­ bers of 1J 0 are called truth values and the members of 1J, are called individuals.
• An interpretation ( {1J,. },. , .J} of cw consists of a frame and a function .J that maps each constant of type T of c.w to an element of 1J,. .

• An assignment into a frame {D.,.}.,. is a function e that maps each variable of type T of C"' to an element of V.,.. Given an assignment e, a variable z.,., and an element dE V.,., e(z.,. .-. d] is defined as e except for z.,. where it is d.

2. 7 Definition (Interpretation): An interpretation M = ({V.,. }.,., :T} is a weak interpretation (weak model, general model) for C"' iff there is a binary function vM SO that for every assignment e and term t of type T, Vtt E V.,. and the following conditions hold:

1. for all variables z.,., vtz.,. = ez.,.

It is a strong interpretation (strong model, standard model), if V.,. = :F(V.,. 1 , · ·· , V.,. ... ; V 17 ) for all occurring types T with T = (Tt X ···X Tm--+ u) .

1. Remark: It is easy to see that in C 1 for every weak model of a formula set there is a strong model with the same interpretation function :T.

Sorted Logics

Now we introduce our target language, a standard many­ sorted first order logic with equality predicates on all sorts. Let E be a (finite) set of sorts. We define the sig­ nature Sr. of a logic in C!ort as a union of possibly empty sets s<· .......... ):a (m-ary function constants), s<········m) (m-ary predicate constants), s:on·t (object constants), and the infinite countable sets s:a .. (object variables), where St, ... ,Bm,S E E. ln·each s<·.·) we have the bi­ nary predicate symbol :<·,·>. We index the elements of Sr. sometimes by their sorts. For instance a function symbol! of sort (s1 , ... ,sm): sis written as J<········m):.. Sorted terms and formulae can be defined as usual and we underly the usual semantics. For details see [Kerber, 1990].

The order sorted logic covers this simple situation and therefore the input language of a theorem prover like the Markgraf Karl Refutation Procedure [MKRP, 1984] is well-suited for dealing with the defined logic.

3 Logic Morphisms

Now we shall define those concepts that are necessary to describe the relation between formalizations in different logics. The important concepts are: logic, morphism, quasi-homomorphism, and soundness and completeness of a morphism.

1. Definition (Morphism of Logics): Let :F 1 and :F 2 be two logical systems (C"', r,n, or C!ort), then a

·we use the connectives and quantifiers in a naive way at the meta-level.

• morphism e is a mapping that maps the signature s of a logic :F 1 (S) in :F 1 to a signature of a logic :F 2 (9(S)) in :F 2 and that maps every formula set in :F 1 (S) to a formula set in :F2(9(S)).·
• Definition (Soundness): Let e be a morphism from :F 1 to :F2. e is called strongly (weakly) sound iff the following condition holds for every formula set r in :F 1 : if r has a strong (weak) model in :F 1 then there is a strong (weak) model of e(r) in :F2.
• Definition(Completeness): Let e be amorphism from :F 1 to :F2. e is called strongly (weakly) complete iff the following condition holds for every formula set r in :F 1 : if e(r) has a strong (weak) model in :F2 then there is a strong (weak) model of r in :F 1 .
• Definition (Quasi-Homomorphism): Let :Fl(St) and :F2(S2 ) be two logics. A mapping e that maps every formula and every term of :F 1 (S1) to a formula respec­ tively to a term of :F 2 (S2) is called a quasi-homomor­ phism iff the following conditions are satisfied:

1. For all terms:

1. if z is a variable of :F 1 ( St) then 9( z) is a vari­ able of :F 2 (S2).
2. if cis a constant of :F 1 (St) then 9(c) is a con­ stant of :F2(S2).
3. if f(t 1 , .. . , tm) is a term of :F 1 (S1) then e (f(tt, ... , tm)) = 1'J (9(!), e(tt ), ... , e(tm)) "th .o( ) { a( at, ... , am) or Wl u a, a1, . . . , am = ( ) Ck 4 a, a1, ... , am

The constants a have to be chosen appropri­ ately out of s2, especially they have to be new, that is, there must be no element o/ E St so that a 4 = 9( a'). The case which is chosen can depend only on the a, not on the a1 , ·.· , am. (a stands for apply.)

1. For all formulae C{'t, cp2 and for all variables z:
2. 9(cpt A cp2) = 9(cpt) A 9(cp2)

1. e(Vzcp) = 'r/9(z)9(cp)
2. All terms that are not formulae of :F 1 (St) are mapped to terms that are not formulae of :F2(S2).

4 A Sufficient Criterion for Soundness

In this section we give a sufficient criterion for the sound­ ness of translations of formulae of r,n onto formulae of C!ort· which is strong enough to cover most require­ ments.

1. Theorem: If e is an injective quasi-homomorphism from cn(s) to C!ort(Sr.), then e is weakly sound.

Proof: Let M be a weak model of a formula set r, M = ({V.,. }.,., :T} is a weak model for any cp out of r, that is, Vt'cp = T for every assignment e. We are going to construct a model M = ( {v"-r" } .. .,. .. , J} of e(r,o), where "r"· denotes the sort upon which the type T is mapped. We define the sets i)''r" := Vr . j is defined as J(e(c)) := .J(c) for all constants c in S. (Here and in the sequel we make use of the injectivity of e. Additionally we use the fact that constants are mapped onto constants.) The assignments e are defined by e(e(x)) := e(x). Because of iJ"r" = Vr we get all assignments in this way. Recall that we have no function or predicate variables in .C!ort. We also use the fact that variables are mapped onto variables. For the functions a::r" with r = (r1 x · · · x Tm - u) we can define the in­ terpretation so that it takes the interpretation of the first argument, which is a function, and applies it to the other arguments. We can do this, because these functions are new. Formally this interpretation can be written: for all I E v"r", for all Zl E v"rl", . .. , Xm E v"r,.." vt<a;r")(!, Zl, .. . , Xm) := l(xl, ... , Xm)· Note that I E v"r" = Vr is a function and hence applicable. ~nalogo:!~~;r we define the interpretation for the pred­ Icates a:P .

· A formula is regarded as a formula set with one element. Especially we write 9( 'I') instead of 9( { <p }).

Now M is a model of e(r,o) , which is proved by showing inductively that for all terms and formulae vt 0 e = vr . The proof is straightforward and can be found in [Kerber, 1990]. ·

4.2 Theorem: If e is an injective quasi-homomorphism from .cn(S) to .C!ort(S~). then e is strongly sound.

Proof: If there is a strong model of a formula set r in .cn(S), then this model is also a weak model. By the previous theorem there is hence a weak model of e(r) in .C!ort(S~). By a sorted version of remark 2.8 there is also a strong model of e(r). ·

By the theorems above it follows directly that the translation used in example 1.1 is weakly and strongly sound.

4.3 Remark: Note that the formulae that are obtained by these translations are not essentially more difficult than the original ones and that the structure of the for­ mulae (number and position of quantifiers or junctors) is respected. In the image the terms are never more nested than in the original.· The only thing that can change, is that the number of arguments in a term is increased by one.

5 A Complete Translation

Now we want to define morphisms en from .en to .C!ort which are not only sound but also complete. We define the morphisms for odd n, for even n they are obtained as the restrictions of the next higher odd n, that is e2n := E>2n+1 I.e, ... The morphisms e are defined as e(r,o) = e'(r,o) U EXT, where e' is a quasi-homomorphism and EXT is the set of extensionality axioms which depends only on the signature. In the following we drop the index n. Again we abbreviate apply as a .

·By "T" we mean the string after expanding the abbre­ viation for r, for instance, if r = (t x t - o) then "T" is "(txt~o)".

5.1 Definition (Standard Translation e2n-l): Let S 2 n-l = Ur Sr be the signature of a logic in .C2n-l. We define a signature s~ of a logic in .C!ort by assigning to each predicate constant of order n, arity m, and type r = (r1 x · · · x Tm - o) a predicate constant of order 1, arity m (that is, of type (t x · · · X £ - o))· and sort ("Tl", . .. , "Tm "). All constants and variables of order less than n and of a type u are mapped onto constants and variables of type t and sort "U". Because we as­ sumed all members in S2n-l to be disjoint, we can use the same names for the images.

Additionally we have in s~ for each type T of order less than n with r = (r1 x ···X Tm- o) a new (m + 1)-ary d. "r" f ( ) pre 1cate constant a: o sort "r", "rl ", . .. , "r m" and for each type r of order less than n with r = (r1 x · · · x Tm - u), u #: o a new (m + 1)-ary func-. "r" f ( ) bon constant a: o sort "r", "r1 ", . . . , "Tm" : "U". Now we are going to define a quasi-homomorphism e'. For terms it is defined inductively by:

• T1 for all variables Xr, e'(xr) = x"r"
• T2 for all constants Cr of order equal n with T = (rl X ··· X Tm- o), e'(cr) = c("r,", .. . ,"r,..")
• T3 for all constants Cr of order less than n, e' ( Cr) = c"T"
• T4 For a term with an m-ary function term I of type T as top expression We define e'(/(tl, ... , tm)) = a:"r" (e'(f), e'(tt), . .. , e'(tm))

For formulae we define e' inductively by:

• F1 For an atomic formula with predicate constant p of order n as top expression we define e'(p(tl, .. . , tm)) = e'(p)(e'(tl), ... , e'(tm))
• F2 For a term with an m-ary predicate term p of type r and order less than n as top expression we define e'(p(tl, ... , tm)) = a:"r" (e'(p), e'(tl), .. . , e'(tm))
• F3 For all other formulae we define e' as the homomor­ phic extension.

EXT is the set of the following .C!ort-formulae:

Now we can define e(r,o) = e'(r,o) U EXT.

5.2 Remark: It should become obvious now, why we excluded types like (o - o): For instance let P be a predicate of this type, Q be a predicate of type ( t - o), and c be a constant of type L. Then the transla­ tion of P(Q(c)) A Q(c) can be only the apply-construct a"(o-o)"(P,a"C'-o)"(Q,c)) A a"(,-o)"(Q,c) or the direct translation P(a"(,-o)"(Q,c)) A a"<·-o)"(Q,c). But both formulae are not well formed, because a"<·-o)"(Q,c) has to be a formula and a term at once. Even worse in general a uniform (quasi-homomorphic) translation is not possible, because Q( c) must be trans­ lated in the first case to a term and in the second to a formula, what is not allowed in first order logic. I think that this example is also a counterexample for the correctness of the translation given by BENTHEM and DOETS [1983] for a language without function symbols. A possible translation of the unrestricted typed higher order logic has also to provide a translation of formulae of the kind P(Q(c)) A Q(c) . This is possible by having as functional symbols only the a"""; all other symbols are object variables or object constants. Especially the junctor "A" has also to be translated to a constant.

·Recall: In £ 2 ,..... 1 there is no function constant of order n.

5.3 Theorem: e is weakly and strongly sound. (For a proof see [Kerber, 1990].)

5.4 Theorem: e is weakly complete.

Proof: Let r be a formula set in .c 2 n- 1 (S). Let M be a weak model of e(r). Then M is a model of e(r,c) for every formula r,c in r. Let M be ({1J·}., :J} and e be an arbitrary assignment. Then we have Vt(e(r,c)) = T. We want to construct a model M of r,c, so that for all assignments i we have Vf(r,c) = T. Therefore we define i>, := 1J"'" and V0 := {T, F} . For all other types T with T = (T1 x · · · x Tm - IT) we have to define i>,. ~ :F(V,. 1 , · ·· , iJ,..,.; i>u ). We do it by inductively defining injectiye fu!lctions Q,. f~om p"(r1 x .. ·xr.,.:-:!" to :F(1J,.1l ... , 1J,..,.; 'Du) and settmg 1J,. := Q,.(1J ,. ). Hence Q,. is a bijective function from v"r" to i),. .· We define Q,. inductively:

Q, : 1J"'" - i>, is the identity mapping. (This function is obviously bijective.)

Let Q,., and Qu be defined for 1J"T1"' ... 'v"r ... " and v"u". We are going to define a function Q,. with T = ( ) .J. fi v"r" ll .. ,. .. T1 x · · · x Tm -IT , IT.,.. o, or . For a x E 1J Q,.(z) is defined as the function Q,.(z)(i1, . .. , im) := Qu(Vt (a"r")(x, Q;. 1 (il), . . . , Q;~(im))) for all i1 E iJ,. 1 , ... , im E iJ,.,.. .

The following diagram may help to see the involved map­ pings at a glance:

By the corresponding extensionality axiom in EXT it can be shown that Q,. is bijective (see [Kerber, 1990]). For IT = o and for order of T is equal to n we define Q,.(p)(il, ... , im) := p(Q;. 1 (it), . . . , ~;~(im)) , and for order of T less than n , q,.(z)(it, . . . , im) := Vt(a"r")(x, ~;/(it), ... , Q;~(im)) for all i1 E V,. 1 , ·· · , im E iJ,..,.. The bijectivity is shown analogously with help of the extensionality axioms.

*In order to get strong completeness it would be necessary to achieve bijectivity from v"r" to :F(t>,.u . .. , 1:>,.,.; t>u ). For n > 1 this is impossible because of GOdel's incompleteness theorem.

Q is the polymorphic mapping defined by all the indi­ vidual q,.. Now we are going to show that if M is a model of e(r,c), that is, for all assignments e we have vt(e(r,c)) = T, we have M is a model of r,c, that is, for all assignments i we have Vf ( r,c) = T with M = ( { iJ,. },. ' j}. j is defined as Q 0 :J 0 e'. The assign­ ments i are defined as Q o e o e'. Because Q and e' are bijective, we get all assignments this way.

By induction on the construction of terms it can be proved, that for all terms: vf = q o vt o e' and for all formulae: Vf = Vt o e'. The proof can be found in [Kerber, 1990]. Summarizing we have: ifVt(e(r,c)) = T then Vt(f>'(r,c)) = T then Vf(r,c) = T. ·

5.5 Remark: Because e' is an injective quasi­ homomorphism, e'- 1 provides a calculus for .C". If we add rules that enforce that function symbols and pred­ icate symbols are equal if they agree in all arguments, we can transform every sound and complete first order calculus of .C!orf by e to a sound and weakly complete calculus for .en. We can execute the proof in .C!ort and then lift it to a proof in .en.

1. Remark: One might wonder why we proposed a suf­ ficient criterion for the soundness of translations, when we have a translation that is sound and complete and hence could be used always. However in a concrete situ­ ation it can be better not to translate into the full sound and complete formulae, because the search space may become too big. It would not be a good idea to add the extensionality axioms if they are not really needed. In addition we can prevent instantiation if we translate certain constants not by an apply or if we use different apply functions or predicates although we could use the same. On the other hand the completeness result guar­ antees that we can find a translation at all . Which one we choose may be very important for the theorem prover to find a proof. Whereas the extensionality axioms are relatively harmless, for really higher order theorems it is necessary to add S<rcalled comprehension axioms (com­ pare [Andrews, 1986, p.156]) in order to approximate weak semantics to strong semantics. For many theorems these axioms are not necessary, for the others one must choose the axioms very carefully, otherwise the first or­ der theorem prover will get a search space that is too big. It is the advantage of higher order theorem prov­ ing compared to our approach, that there one does not need these axioms (for the prize of the undecidability of unification) . In the appendix we give an example of a theorem, where a comprehension axiom is necessary.

6 Summary and Open Problems

In the sections above we introduced the basic machinery for translating higher order formulae to first order logic.

We introduced a sufficient criterion for the soundness of such a translation, namely that it has to be an injective quasi-homomorphism. Then we gave a complete trans­ lation for the restricted higher order language.

In the full version of the paper [Kerber, 1990] we gen­ eralized the results to logics with equality. An interest­ ing and useful generalization would be to a higher order sorted logic. Then the first order logic should have a sort structure at least as powerful as that of the higher order source logic. The results should be transferable although the formal treatment can become strenuous.

Acknowledgement

I like to thank AXEL PRACKLEIN for many discussions and thorough reading of a draft and JORG SIEKMANN for his advice that resulted in numerous improvements.