Theory Interpretation in Simple Type Theory^{⋆}

William M. Farmer

The MITRE Corporation 202 Burlington Road Bedford, MA 01730-1420, USA

                       farmer@mitre.org

March 28, 1994

Abstract. Theory interpretation is a logical technique for relating one axiomatic theory to another with important applications in mathematics and computer science as well as in logic itself. This paper presents a method for theory interpretation in a version of simple type theory, called lutins, which admits partial functions and subtypes. The method is patterned on the standard approach to theory interpretation in firstorder logic. Although the method is based on a nonclassical version of simple type theory, it is intended as a guide for theory interpretation in classical simple type theories as well as in predicate logics with partial functions.

1 Introduction

Theory interpretation—in which one theory is interpreted in another via a syntactic mapping—is a fundamental logical technique which has important applications in mathematics and computer science as well as in logic itself. An interpretation^{1} of a theory^{2} T_{1} in a theory T_{2} is a mapping from the expressions of T_{1} to the expressions of T_{2} which preserves the validity of sentences. (T_{1} and T_{2} are called the source theory and the target theory of the interpretation, respectively.) In logic, interpretations are used to prove metamathematical properties about theories and to compare theories in terms of their “strength”. In mathematics, theorems and problems are transported from one context to another via interpretations. In computer science, interpretations are a rigorous tool for documenting and verifying that one system specification is a refinement of another.

⋆ Supported by the MITRE-Sponsored Research program. To appear in the proceedings of the International Workshop on Higher Order Algebra, Logic and Term Rewriting (HOA ’93, Amsterdam, The Netherlands, September 1993), Lecture Notes in Computer Science, Springer-Verlag, 1994.

1 Theory interpretations of this kind are also called translations, theory morphisms,

immersions, and realizations. 2 We take a theory to be a set of sentences in a formal language (that is not necessarily

closed under logical consequence). The sentences are called the axioms of the theory.

Until recently, interpretations have been almost exclusively employed by theoreticians. However, implementors are now discovering that interpretations are useful for organizing and supporting mathematical reasoning in automated reasoning systems such as mechanical theorem provers and computer system specification and verification environments. Interpretations are used extensively with success in the imps Interactive Mathematical Proof System [10, 11, 12]. They are also a fundamental component in the following programming and verification environments: ehdm [27], m-eves [5] and eves [6], iota [24], and obj3 [14].

Theory interpretation has primarily been studied and applied in the context of first-order predicate logic. Logic textbooks like Enderton [7], Monk [22], and Shoenfield [28] present a fairly standard approach to theory interpretation in first-order logic. The approach revolves around a special class of interpretations that are well behaved both syntactically and semantically. Suppose Φ is an interpretation of T_{1} in T_{2} which is in this class. Then Φ will be a kind of homomorphism which preserves the structure of terms and formulas and which is completely determined by how it associates the sorts (if there are any) and constants of T_{1} with objects of T_{2}. Moreover, Φ will define a way of extracting a model for T_{1} from any model for T_{2}.

Although there is a wealth of writing on theory interpretation in first-order logic, the subject is only beginning to be seriously explored in higher-order logic (and type theory) [9, 17, 36]. There are, however, at least two good reasons to study theory interpretation in higher-order logic. First, higher-order logic is becoming increasingly important in computer science and mechanized mathematics. Second, since higher-order logic is much more expressive than first-order logic, the space of interpretations is much richer in higher-order logic than in first-order logic. This means that some techniques based on theory interpretation are more powerful in a higher-order logic than in a first-order logic (e.g., the technique of verifying that a theory T′ is a model conservative extension of T by exhibiting an interpretation of T′ in T which fixes T).

The most well-known and widely used form of higher-order logic is simple type theory [4, 1]. Since it has built-in support for functions—a hierarchy of function types, full quantification over functions, and (usually) λ-notation for specifying functions—it is a convenient logic for formalizing mathematics. For this reason, it is the logical basis for several automated reasoning systems, including ehdm, hol [15], imps, Isabelle [25], pvs [26], and tps [2]. In spite of its popularity and utility, there is not a well-developed approach to theory interpretation in simple type theory.

The goal of this paper is to develop a method for theory interpretation in simple type theory patterned on the standard first-order approach. We want the method to handle interpretations in which a base type (i.e., a type of individuals) of the source theory can be associated with either a (possibly higher-order) type or subtype of the target theory.

In first-order logic, an interpretation which associates base types with types is merely an interpretation which associates the universe (i.e., the implicit type of individuals) of the source theory with the universe of the target theory. An interpretation of this kind does not alter the quantifiers in expressions of the source theory. An interpretation which associates base types with subtypes is one which associates the universe of the source theory with a unary predicate of the target theory. An interpretation of this kind “relativizes” the quantifiers in expressions of the source theory. For example, if Φ is an interpretation which associates the universe of the source theory with the predicate φ, then

Φ((∀x)ψ) = (∀x)(φ(x) → Φ(ψ)).

Many natural theory interpretations associate a base type with a subtype (i.e., part of a type). For example, suppose G is a theory of an abstract group in which α is a base type denoting the set of group elements; F is a theory of an abstract field in which β is a base type denoting the set of field elements; and Φ is the interpretation of G in F in which the group structure of G is “interpreted” as the structure of the multiplicative group of F. Then Φ would associate α with the subtype of β consisting of the nonzero field elements. Moreover, the most natural translation of the group operation of G via Φ would be an expression denoting the multiplication operation of F restricted to the nonzero field elements. Thus we see that associating base types with subtypes leads to functions with restricted domains. (This example is worked out in detail in Section 7.)

If only interpretations which associate base types with full types are considered, it is easy to lift the first-order notion of a theory interpretation to simple type theory. On the other hand, associating base types with subtypes is messy in simple type theory since one must deal with functions with restricted domains, as we have seen above. Restricting the domain of a function is unproblematic in informal mathematics, but there is no completely satisfactory way that it can be done in classical predicate logic since expressions cannot directly denote partial functions. (See [8] for a discussion on the various ways of dealing with partial functions in predicate logic.) In first-order logic, partial functions are avoided by relativizing quantifiers. This approach would be more complicated in simple type theory because more than just quantifiers would have to be relativized; in particular, all predicates on functions (such as those corresponding to universal and existential quantification) would have to be relativized.

Our method for theory interpretation is formulated in a version of simple type theory, called lutins^{3} [8, 9, 16], which supports both partial functions and subtypes. We have chosen lutins over a classical simple type for three pragmatic reasons. First, as we have pointed out, partial functions naturally arise from interpretations that associate base types with subtypes. Consequently, interpretations of this kind can be formalized more directly in a logic which admits partial functions like lutins. Second, since lutins contains subtypes, an interpretation in lutins does not have to relativize quantifiers and other variable binders, provided appropriate subtypes are defined. Finally, as the logic of the imps interactive theorem proving system, lutins has been implemented and rigorously and extensively tested [12]. It is clearly an effective logic for formalizing a wide range of mathematics. Although the method is based on a nonclassical

3 Pronounced as the word in French.

form of simple type theory, we expect it to be useful as a guide for theory interpretation in classical simple type theories as well as in predicate logics which admit partial functions.

The paper is organized as follows. An overview and discussion via examples of the standard approach to theory interpretation in first-order logic is given in Sections 2 and 3. Section 4 gives a quick introduction to PF^{∗}, an austere version of simple type theory with partial functions and subtypes on which lutins is based. The syntax and semantics of lutins are then presented in Section 5. The notion of a theory interpretation in lutins is defined in Section 6. Section 7 contains some examples in lutins of interpretations of groups in fields. The interpretation and relative satisfiability theorems for lutins are proved in Section 8. And a brief conclusion is found in Section 9.

Comparisons between our method of theory interpretation and the standard approach in first-order logic are made at several places in the paper.

2 Theory Interpretation in First-Order Logic

This section presents an outline of the standard approach to theory interpretation in first-order logic [7, 22, 28]. For the most part, we shall adopt in this section the definitions and notation of first-order logic (with equality) presented in [3]. An expression of a first-order language L or theory T is a term or a formula of L or T. An n-ary expression function is a λ-expression of the form λ{x_{1}, …, x_{n} . E} where E is an expression. Let θ = λ{x_{1}, …, x_{n} . E} be an expression function. θ is a term [respectively, formula] function if E is a term [respectively, formula]. Given terms t_{1}, …, t_{n}, θ(t_{1}, …, t_{n}) denotes the result of simultaneously substituting t_{i} for all free occurrences of x_{i} in E, for all i with 1 ≤ i ≤ n.

Let T_{i} be a first-order theory for i = 1, 2. A standard translation from T_{1} to T_{2} is a pair (U, ν) where U is a closed formula function of the form λ{x . φ} which represents a unary predicate and ν is a function from the nonlogical constants of T_{1} to the nonlogical constants, expressions, and expression functions of T_{2} such that:

1. If c is an individual constant symbol of T_{1}, then ν(c) is either an individual constant symbol or a closed term.

2. If F is an n-ary function symbol of T_{1}, then ν(F) is either an n-ary function symbol or a closed n-ary term function.

3. If P is an n-ary relation symbol of T_{1}, then ν(P) is either an n-ary relation symbol or a closed n-ary formula function.

4. ν(≡) = ≡.^{4}

Let Φ = (U, ν) be a standard translation from T_{1} to T_{2} throughout the rest of this section. For an expression E of T_{1}, the translation of E via Φ, written Φ(E), is the expression of T_{2} defined inductively by:

4 In [3], the binary relation symbol ≡ denotes the equality relation.

1. Φ(x) = x, if x is a variable.

2. Φ(c) = ν(c), if c is an individual constant symbol.

3. Φ(S(t_{1}, …, t_{n})) = ν(S)(Φ(t_{1}), …, Φ(t_{n})), if S is an n-ary function or relation symbol.

4. Φ(¬φ) = ¬Φ(φ).

5. Φ(φ □ ψ) = Φ(φ) □ Φ(ψ), if □ ∈ {∧, ∨, →, ↔}.

6. Φ((□x)φ) = (□x)Φ(φ), if □ ∈ {∀, ∃} and U = λ{x . x ≡ x}.

7. Φ((□x)φ) = \{ \begin{matrix}(∀x)(U(x) → Φ(φ)) & if □ = ∀ \\ (∃x)(U(x) ∧ Φ(φ)) & if □ = ∃ \end{matrix}

if U ≠ λ{x . x ≡ x}.

A standard translation thus associates the universe of its source theory with a closed unary predicate of its target theory; the nonlogical constants of its source theory with closed expressions (of appropriate “type”) of its target theory; and the variables and logical connectives with themselves. The quantifiers are relativized to the unary predicate if it is not λ{x . x ≡ x}. Except for the relativization of quantifiers, a standard translation preserves the structure of first-order syntax. Hence, a standard translation can be viewed as a homomorphism from the expressions of its source theory to the expressions of its target theory.

Φ is a standard interpretation of T_{1} in T_{2} if Φ(φ) is valid in T_{2} for each sentence φ which is valid in T_{1}. That is, Φ is an interpretation if it maps valid sentences to valid sentences. The theorem below gives a sufficient condition for a standard translation to be a standard interpretation.

An obligation of Φ is any one of the following sentences of T_{2}:

1. Φ(φ) for each axiom φ of T_{1}.

2. (∃x)U(x).

3. Φ((∃y)c ≡ y) for each individual constant symbol c of T_{1}.

4. Φ((∀x_{1} ⋯ x_{n})(∃y)F (x_{1}, …, x_{n}) ≡ y) for each function symbol F of T_{1}.

The four kinds of obligations are called, in order, axiom, universe nonemptiness, individual constant symbol, and function symbol obligations. The meaning of an individual constant symbol obligation is that the interpretation of the universe contains the interpretation of the individual constant symbol, and the meaning of a function symbol obligation is that the interpretation of the universe is closed under the interpretation of the function symbol. Note: The last three kinds of obligations are trivially valid in T_{2} if U = λ{x . x ≡ x}.

Theorem 2.1 (Standard Interpretation Theorem) A standard translation from T_{1} to T_{2} is a standard interpretation if each of its obligations is valid in T_{2}.

T_{1} is interpretable in T_{2} (in the standard sense) if there is a standard interpretation of T_{1} in T_{2}. The next theorem is the most important consequence of interpretability.

Theorem 2.2 (Standard Relative Satisfiability) If T_{1} is interpretable in T_{2} and T_{2} is satisfiable, then T_{1} is satisfiable.

The key idea in the proof of this theorem is to use the standard interpretation of T_{1} in T_{2} to extract a model of T_{1} from a model of T_{2}. The Standard Interpretation Theorem and the Standard Relative Satisfiability theorem are the chief theorems of the standard approach to theory interpretation in first-order logic.

By virtue of being a validity preserving homomorphism, a standard interpretation syntactically and semantically embeds its source theory in its target theory. Standard interpretations are used to compare the strength of theories: T_{2} is at least as strong as T_{1}, if T_{1} is interpretable in T_{2}. Also, standard interpretations have long been used in logic to prove metamathematical properties about first-order theories, mainly relative consistency, decidability, and undecidability. For example, the classic work of Tarski, Mostowski, and Robinson [32] illustrates how the undecidability of T_{1} can be reduced to the undecidability of T_{2} by constructing an appropriate standard interpretation of T_{2} in T_{1}. For other references on the theory and use of standard interpretations, see [13, 23, 30, 31, 34].

3 Some Simple Examples

This section contains three examples of standard first-order interpretations. Although the examples are very simple, they illustrate some of the power and versatility of theory interpretation.

The first example is an interpretation of a theory of an abstract nonstrict partial order in a theory of an abstract strict total order.

Example 3.1 Let PO be the theory consisting of the following three sentences in the first-order language of a binary relation symbol ≤:

1. Reflexivity. (∀x)(x ≤ x).

2. Transitivity. (∀xyz)((x ≤ y ∧ y ≤ z) → x ≤ z).

3. Antisymmetry. (∀xy)((x ≤ y ∧ y ≤ x) → x ≡ y).

PO clearly specifies ≤ to be a nonstrict partial order.

Similarly, let TO be the theory consisting of the following three sentences in the first-order language of a binary relation symbol <:

1. Irreflexivity. (∀x)¬(x < x).

2. Transitivity. (∀xyz)((x < y ∧ y < z) → x < z).

3. Trichotomy. (∀xy)(x < y ∨ y < x ∨ x ≡ y).

TO clearly specifies < to be a strict total order.

Let Φ_{1} be the standard translation (U_{1}, ν_{1}) from PO to TO where U_{1} = λ{x . x ≡ x} and ν_{1}(≤) = λ{x, y . (x < y ∨ x ≡ y)}. Φ_{1} is clearly an interpretation of PO in TO by the Standard Interpretation Theorem.□

Φ_{1} links two different axiomatizations—different axioms in different formal languages—of the same mathematical domain (i.e., the notion of an order relation). Via Φ_{1}, theorems proved in PO about the nonstrict partial order ≤ can be transformed into corresponding theorems in TO about the strict total order <. In other words, Φ_{1} serves as a conduit through which theorems can be freely “transported” from one mathematical formalization to another. Interpretations are used in this manner, at least informally, in many areas of mathematics to transport theorems from abstract to more concrete contexts or to move a problem to a more convenient setting (for examples, see [18]). Moreover, interpretations of this sort are fundamental to the “little theories” version of the axiom method in which mathematical reasoning is performed over a network of theories linked by interpretations—instead of entirely within one single “big theory” such as Zermelo-Fraenkel set theory. (In [11], we describe the little theories approach and argue in favor of its implementation in mechanical theorem provers.)

Φ_{1} also establishes that TO is a “refinement” of PO. Actually, TO refines PO in two ways: (1) the models of TO are a special kind of partial order, namely a total order, and (2) the atomic relation ≤ is decomposed into a compound relation built from < and ≡ via Φ_{1}. (This latter sort of refinement is much like a definition done in reverse.) Refinement is a basic technique in computer science for specifying and building computer systems. Theory interpretation is an excellent tool for rigorizing computer system development based on refinement (for examples, see [20, 21, 29, 33, 35]).

The interpretation in the next example formalizes the symmetry between left and right multiplication in a monoid.

Example 3.2 Let M be the theory consisting of the following three sentences in the first-order language of a binary function constant ∗ and an individual constant e:

1. Associativity. (∀xyz)((x ∗ y) ∗ z ≡ x ∗ (y ∗ z)).

2. Left Identity. (∀x)(e ∗ x ≡ x).

3. Right Identity. (∀x)(x ∗ e ≡ x).

M is a very standard formulation of a theory of an abstract monoid.

Now let Φ_{2} be the standard translation (U_{2}, ν_{2}) from M to itself where U_{2} = λ{x . x ≡ x}, ν_{2}(∗) = λ{x, y . y ∗ x}, and ν_{2}(e) = e. Φ_{2} is a homomorphism from the expressions (terms and formulas) of M to the expressions of M, but (unlike Φ_{1}) Φ_{2} alters terms. Each expression A of M is mapped by Φ_{2} to an expression Φ_{2}(A) which is symmetric to A with respect to reversing the argument order of ∗. For instance, Φ_{2} maps the Left Identity axiom to the Right Identity axiom and vice versa. Consequently, Φ_{1} is an interpretation of M in itself by the Standard Interpretation Theorem.□

Interpretations like Φ_{2} allow one to reason “by symmetry” in mechanized mathematics systems. For an illustration, suppose A and B are two sentences we want to prove which are symmetric to each other in some way. In informal mathematics, we would first construct a proof of A, and then we would prove B by simply noting that there is a proof of B that is symmetric to the proof of A. We would not have bothered to construct this proof of B, for nothing new would be learned. In a mechanized mathematics system with interpretations, after proving A, we would find an interpretation which formalizes the symmetry between A and B and which maps A to B. Just as in informal mathematics, we would not bother to produce a proof of B, but we would know that B is valid because it is the image of a theorem by an interpretation. Moreover, the verification that the mapping is really an interpretation would effectively be a verification that this particular kind of reasoning by symmetry is valid.

The interpretation in the last example associates the universe of an abstract monoid with the singleton set of the identity element.

Example 3.3 Let Φ_{3} be the standard translation (U_{3}, ν_{3}) from M to itself where U_{3} = λ{x . x ≡ e}, ν(∗) = ∗, and ν_{3}(e) = e. Since ({e}, ∗, e) has the structure of a monoid, it is easy to see that Φ_{3} is an interpretation of M in itself.□

Since U_{3} denotes a proper subset of the universe of M, Φ_{3} relativizes quantifiers. For example,

Φ_{3}((∀x)(e ∗ x ≡ x)) = (∀x)(x ≡ e → e ∗ x ≡ x).

Also, notice that Φ_{3} fixes the primitive constants of M (i.e., ∗ and e). The act of verifying that Φ_{3} is an interpretation is equivalent to proving that {e} is a submonoid of M. A standard interpretation that fixes the primitive constants of the source theory but restricts the universe of the source theory is called a relativization. Relativizations are commonly used in set theory to establish relative consistency [19].

4 PF^{∗}

PF^{∗} is a version of simple type theory with partial functions and subtypes. This section gives a quick introduction to the syntax and semantics of PF^{∗}. The next section introduces a “user-friendly” version of PF^{∗} called lutins. See [9] for the full, definitive presentation of PF^{∗}.

Preliminary Definitions

We begin by defining the machinery we will use to specify the various symbols of a PF^{∗} language. In particular, the set of type or subtype symbols built from a set S of base type or subtype symbols will be the set Ω(S) defined below.

Let S be a set of symbols containing the symbol ∗. Ω(S) is the set defined inductively by:

1. S ⊆ Ω(S).

2. If α_{1}, …, α_{n}, α_{n+1} ∈ Ω(S) (n ≥ 1), then [α_{1}, …, α_{n}, α_{n+1}] ∈ Ω(S).

Ω^{∗}(S) is the subset of Ω(S) defined inductively by:

1. ∗ ∈ Ω^{∗}(S).

2. If α_{1}, …, α_{n} ∈ Ω(S) and α_{n+1} ∈ Ω^{∗}(S) (n ≥ 1), then [α_{1}, …, α_{n}, α_{n+1}] ∈ Ω^{∗}(S).

Given a total function f : S → Ω(S), ⪯_{f} is the smallest binary relation on Ω(S) such that:

1. If α ∈ S, then α ⪯_{f} f(α).

2. ⪯_{f} is reflexive, i.e., for all α ∈ Ω(S), α ⪯_{f} α.

3. ⪯_{f} is transitive, i.e., for all α, β, γ ∈ Ω(S), if α ⪯_{f} β and β ⪯_{f} γ, then α ⪯_{f} γ.

4. If α_{1} ⪯_{f} β_{1}, …, α_{n} ⪯_{f} β_{n}, α_{n+1} ⪯_{f} β_{n+1}, then [α_{1}, …, α_{n}, α_{n+1}] ⪯_{f} [β_{1}, …, β_{n}, β_{n+1}].

⪯_{f} is noetherian if every ascending sequence of members of Ω(S),

α_{1} ⪯_{f} α_{2} ⪯_{f} α_{3} ⪯_{f} ⋯,

is eventually stationary, i.e., there is some m such that α_{i} = α_{m} for all i ≥ m. If ⪯_{f} is noetherian, then ⪯_{f} is obviously antisymmetric (i.e., for all α, β ∈ Ω(S), if α ⪯_{f} β and β ⪯_{f} α, then α = β). Hence, ⪯_{f} is a partial order if it is noetherian.

An S-tagged symbol is a symbol tagged with a member of Ω(S). A tagged symbol whose symbol is a and whose tag is α is written as a_{α}. A tagged symbol a_{α}, where a = b_{i}, will be written as b_{α}^{i} (instead of as (b_{i})_{α}). Two tagged symbols a_{α} and b_{β} are distinct if a ≠ b.

Sort Systems

The types and subtypes of a PF^{∗} language are called “sorts”. Syntactically, they form a partial order. The semantics of the partial order of sorts is a mapping that takes each sort to a nonempty set and takes the order relation to set inclusion.

A sort system of PF^{∗} is a pair (A, ξ) where A is a finite set of symbols such that, for some m ≥ 1, B_{m} = {∗, ι_{1}, …, ι_{m}} ⊆ A and ξ is a total function from A to Ω(A) such that:

1. For all α ∈ A, α ∈ B_{m} iff ξ(α) = α.

2. For all α ∈ A, ξ(α) ∈ Ω^{∗}(A) iff α = ∗.

3. ⪯_{ξ} is noetherian.

A sort of the system is any member of Ω(A), and a type of the system is any member of Ω(B_{m}). The sorts in A, Ω(A) \ A, B_{m}, and Ω(B_{m}) \ B_{m} are called the atomic sorts, compound sorts, base types, and function types of the system, respectively. (∗ is the type of propositions, and each ι_{k} is a type of individuals.) The enclosing sort of α ∈ A is the sort ξ(α).

Let S be a sort system (A, ξ). By α ∈ S we shall mean α ∈ Ω(A). Also, let T be the set of types of S. The definition of a sort system implies that, for each α ∈ S, there is a unique β ∈ T , called the type of α, such that α ⪯_{ξ} β. The type of α is denoted by τ(α). A sort α is of kind ∗ [respectively, ι] if α ∈ Ω^{∗}(A)

[respectively, α ∈ Ω(A) \ Ω^{∗}(A)]. Let S^{∗} [S^{ι}] denote the set of all α ∈ S of kind ∗ [ι]. The least upper bound of α and β, written α ⊔_{ξ} β, is the least upper bound of α and β in the partial order ⪯_{ξ}. Since each atomic sort has just a single enclosing sort, the least upper bound of two sorts with the same type is always defined.

A standard sort frame for S is a set {D_{α} : α ∈ S} of nonempty domains (sets) such that:

1. D_{∗} = {t, f}. (t ≠ f.)

2. If α ⪯_{ξ} β, then D_{α} ⊆ D_{β}.

3. If α = [α_{1}, …, α_{n}, α_{n+1}] is of kind ι, then D_{α} is the set of all partial functions f : D_{α_{1}} × ⋯ × D_{α_{n}} → D_{α_{n+1}}.

4. If α = [α_{1}, …, α_{n}, α_{n+1}] is of kind ∗, then D_{α} is the set of all total functions f : D_{τ(α_{1})} × ⋯ × D_{τ(α_{n})} → D_{α_{n+1}} such that, for all ⟨b_{1}, …, b_{n}⟩ ∈ D_{τ(α_{1})} × ⋯ × D_{τ(α_{n})}, f(b_{1}, …, b_{n}) = f_{τ(α_{n+1})} (see definition below) whenever b_{i} ∉ D_{α_{i}} for at least one i with 1 ≤ i ≤ n.

For a type α ∈ S^{∗}, f_{α} is defined inductively by:

1. f_{∗} = f.

2. If α = [α_{1}, …, α_{n}, α_{n+1}], then f_{α} is the function which maps every n-tuple ⟨a_{1}, …, a_{n}⟩ ∈ D_{α_{1}} × ⋯ × D_{α_{n}} to f_{α_{n+1}}.

It follows from the definition of a standard sort frame that f_{τ(α)} ∈ D_{α} for all α ∈ S^{∗}.

Languages

A language of PF^{∗} is a tuple (A, ξ, V, C) such that:

1. (A, ξ) is a sort system of PF^{∗}.

2. V and C are disjoint countable sets of pairwise distinct A-tagged symbols, whose members are called variables and constants, respectively.

3. For each α ∈ Ω(A), there is an infinite subset V_{α} of V such that x_{β} ∈ V_{α} iff β = α.

4. For each α ∈ Ω(A), =_{[α,α,∗]} and ι_{[[α,∗],α]} are members of C called logical constants.

Variables are denoted by f_{α}, g_{α}, h_{α}, x_{α}, y_{α}, z_{α}, etc. For the rest of this section, let L = (A, ξ, V, C) be a language of PF^{∗}, S be the sort system (A, ξ), and T be the set of types of S.

An expression of L of sort α is a finite sequence of members of V ∪ C ∪ {@, λ, “{”, “}”, “, ”, “.”} defined inductively by:

1. Each x_{α} ∈ V and c_{α} ∈ C is an expression of sort α.

2. If F is an expression of sort [α_{1}, …, α_{n}, β]; A_{1}, …, A_{n} are expressions of sort α′_{1}, …, α′_{n}; and τ(α_{1}) = τ(α′_{1}), …, τ(α_{n}) = τ(α′_{n}), then @{F, A_{1}, …, A_{n}} is an expression of sort β.

3. If x_{α_{1}}^{1}, …, x_{α_{n}}^{n} are distinct variables and B is an expression of sort β, then λ{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . B} is an expression of sort [α_{1}, …, α_{n}, β].

Expressions are denoted by A, B, C, etc., and expressions of sort α are denoted by A_{α}, B_{α}, C_{α}, etc. “Free variable”, “closed expression”, and similar notions are defined in the obvious way. A formula is an expression of sort ∗. A sentence is a closed formula.

Intuitively, when an expression @{F, A_{1}, …, A_{n}} has a denotation, it denotes the value of the function denoted by F applied to the arguments denoted by A_{1}, …, A_{n}. Also, an expression λ{x_{1}, …, x_{n} . B} denotes the function whose value, when given arguments x_{1}, …, x_{n}, is the denotation of B (which generally depends on x_{1}, …, x_{n}) if B has a denotation and is undefined otherwise.

The following abbreviations provide notation for the major logical operations of PF^{∗}:

F (A_{1}, …, A_{n}) for @{F, A_{1}, …, A_{n}} (A_{α} =_{γ} B_{β}) for =_{[γ,γ,∗]} (A_{α}, B_{β}) (A_{∗} ≡ B_{∗}) for (A_{∗} =_{∗} B_{∗}) T_{∗} for (=_{[∗,∗,∗]} =_{[∗,∗,∗]} =_{[∗,∗,∗]}) F_{∗} for (λ{x_{∗} . T_{∗}} =_{[∗,∗]} λ{x_{∗} . x_{∗}}) ¬_{[∗,∗]} for λ{x_{∗} . (x_{∗} ≡ F_{∗})} (¬A_{∗}) for ¬_{[∗,∗]}(A_{∗}) ∧_{[∗,∗,∗]} for λ{x_{∗}, y_{∗} . (λ{g_{[∗,∗,∗]} . g_{[∗,∗,∗]}(T_{∗}, T_{∗})} =_{[[∗,∗,∗],∗]}

λ{g_{[∗,∗,∗]} . g_{[∗,∗,∗]}(x_{∗}, y_{∗})})}

(A_{∗} ∧ B_{∗}) for ∧_{[∗,∗,∗]}(A_{∗}, B_{∗}) ∨_{[∗,∗,∗]} for λ{x_{∗}, y_{∗} . (¬((¬x_{∗}) ∧ (¬y_{∗})))} (A_{∗} ∨ B_{∗}) for ∨_{[∗,∗,∗]}(A_{∗}, B_{∗}) ⊃_{[∗,∗,∗]} for λ{x_{∗}, y_{∗} . (x_{∗} ≡ (x_{∗} ∧ y_{∗}))} (A_{∗} ⊃ B_{∗}) for ⊃_{[∗,∗,∗]} (A_{∗}, B_{∗}) Π_{[[α_{1},...,α_{n},∗],∗]} for λ{p_{[α_{1},...,α_{n},∗]} . (p_{[α_{1},...,α_{n},∗]} =_{[α_{1},...,α_{n},∗]}

λ{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . T_{∗}})}

∀{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . A_{∗}} for Π_{[[α_{1},...,α_{n},∗],∗]}(λ{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . A_{∗}}) ∃{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . A_{∗}} for (¬∀{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . (¬A_{∗})}) I{x_{α} . A_{∗}} for ι_{[[α,∗],α]}(λ{x_{α} . A_{∗}}) (A_{α} ↓ β) for λ{x_{β} . T_{∗}}(A_{α}) (A_{α} ↑ β) for (¬(A_{α} ↓ β)) (A_{α}↓) for (A_{α} ↓ α) (A_{α}↑) for (¬(A_{α}↓)) (A_{α} ≃_{γ} B_{β}) for ((A_{α}↓) ∨ (B_{β}↓)) ⊃ (A_{α} =_{γ} B_{β}) (A_{α} ≠_{γ} B_{β}) for (¬(A_{α} =_{γ} B_{β})) (A_{α} ≄_{γ} B_{β}) for (¬(A_{α} ≃_{γ} B_{β})) ⊥_{α} for I{x_{α} . F_{∗}} where α ∈ S^{ι} F_{[α_{1},...,α_{n},β]} for λ{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . F_{β}} where β ∈ S^{∗} α ⊆ β for ∀{x_{α} . (x_{α} ↓ β)} if{A_{∗}, B_{β}, C_{γ}} for I{x_{α} . ((A_{∗} ⊃ (x_{α} =_{α} B_{β})) ∧ ((¬A_{∗}) ⊃

(x_{α} =_{α} C_{γ})))} where α = β ⊔_{ξ} γ and

x_{α} does not occur in A_{∗}, B_{β}, or C_{γ}.

Parentheses in expressions may be suppressed when meaning is not lost.

Standard Models

In [9] we define two semantics for PF^{∗}, one based on “general models” and the other based on “standard models”. In this paper we are interested only in the standard models semantics. We begin by describing the objects that the logical constants are intended to denote.

Let {D_{α} : α ∈ S} be a standard sort frame for S. Fix β ∈ S with γ = τ(β). The identity relation for D_{β} is the total function p : D_{γ} × D_{γ} → D_{∗} such that, for all a, b ∈ D_{γ}, p(a, b) = t iff a, b ∈ D_{β} and a = b. Given b ∈ D_{γ}, the bdescriptor for D_{γ} is the total function p : D_{γ} → D_{∗} such that, for all a ∈ D_{γ}, p(a) = t iff a = b. When β ∈ S^{ι}, the definite description function for D_{β} is the partial function f : D_{[γ,∗]} → D_{γ} such that f(p) = b if p is the b-descriptor for D_{γ} for some b ∈ D_{β}, and f(p) is undefined otherwise. When β ∈ S^{∗}, the definite description function for D_{β} is the total function f : D_{[γ,∗]} → D_{γ} such that f(p) = b if p is the b-descriptor for D_{γ} for some b ∈ D_{β}, and f(p) = f_{γ} otherwise.

A standard model for L is a pair M = ({D_{α} : α ∈ S}, I) where {D_{α} : α ∈ S} is a standard sort frame for S such that ⊥ ∉ D_{α} for all α ∈ S and I is a function which maps each c_{α} ∈ C to an element of D_{α} such that, for each α ∈ S, (1) I(=_{[α,α,∗]}) is the identity relation for D_{α} and (2) I(ι_{[[α,∗],α]}) is the definite description function for D_{α}. A V-assignment into M is a function which maps each x_{α} ∈ V to an element of D_{α}. Given a V-assignment φ into M; distinct variables x_{α_{1}}^{1}, …, x_{α_{n}}^{n} ∈ V (n ≥ 1); and a_{1} ∈ D_{α_{1}}, … a_{n} ∈ D_{α_{n}}, let φ[x_{α_{1}}^{1} ↦ a_{1}, …, x_{α_{n}}^{n} ↦ a_{n}] be the V-assignment ψ such that ψ(x_{α_{i}}^{i}) = a_{i} for all i with 1 ≤ i ≤ n and ψ(y_{β}) = φ(y_{β}) for all y_{β} ∉ {x_{α_{1}}^{1}, …, x_{α_{n}}^{n}}.

Let M = ({D_{α} : α ∈ S}, I) be a standard model for L. Then there exists a binary function V = V^{M} such that: (1) for each V-assignment φ into M and each expression A_{α}, V_{φ}(A_{α}) ∈ D_{α} ∪ {⊥} if α ∈ S^{ι} and V_{φ}(A_{α}) ∈ D_{α} if α ∈ S^{∗}, and (2) the following conditions are satisfied for all V-assignments φ into M and all expressions:

1. V_{φ}(x_{α}) = φ(x_{α}) if x_{α} ∈ V.

2. V_{φ}(c_{α}) = I(c_{α}) if c_{α} ∈ C.

3. Let A_{α} = @{F, A_{1}, …, A_{n}} with α ∈ S^{ι}. If each of V_{φ}(F), V_{φ}(A_{1}), …, V_{φ}(A_{n}) does not equal ⊥ and V_{φ}(F) is defined at ⟨V_{φ}(A_{1}), …, V_{φ}(A_{n})⟩, then

V_{φ}(A_{α}) = (V_{φ}(F))(V_{φ}(A_{1}), …, V_{φ}(A_{n}));

otherwise V_{φ}(A_{α}) = ⊥.

4. Let A_{α} = @{F, A_{1}, …, A_{n}} with α = [α_{1}, …, α_{n}, β] ∈ S^{∗}. If each of V_{φ}(A_{1}),…,V_{φ}(A_{n}) does not equal ⊥, then

V_{φ}(A_{α}) = (V_{φ}(F))(V_{φ}(A_{1}), …, V_{φ}(A_{n}));

otherwise V_{φ}(A_{α}) = f_{τ(β)}.

5. Let A_{α} = λ{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . B_{β}} with β ∈ S^{ι}. V_{φ}(A_{α}) is the partial function f : D_{α_{1}} × ⋯ × D_{α_{n}} → D_{β} such that

f(a_{1}, …, a_{n}) = V_{φ[x_{α_{1}}^{1} ↦a_{1},...,x_{αn}^{n} ↦a_{n}]}(B_{β})

if V_{φ[x_{α_{1}}^{1} ↦a_{1},...,x_{αn}^{n} ↦a_{n}]}(B_{β}) is defined; otherwise f(a_{1}, …, a_{n}) is undefined.

6. Let A_{α} = λ{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . B_{β}} with β ∈ S^{∗}. V_{φ}(A_{α}) is the total function f : D_{τ(α_{1})} × ⋯ × D_{τ(α_{n})} → D_{β} such that

f(a_{1}, …, a_{n}) = V_{φ[x_{α_{1}}^{1} ↦a_{1},...,x_{αn}^{n} ↦a_{n}]}(B_{β})

if ⟨a_{1}, …, a_{n}⟩ ∈ D_{α_{1}} × ⋯ × D_{α_{n}}; otherwise f(a_{1}, …, a_{n}) = f_{τ(β)}.

When V_{φ}(A_{α}) ≠ ⊥, V_{φ}(A_{α}) is called the value of A_{α} in M with respect to φ. Intuitively, V_{φ}(A_{α}) = ⊥ means that A_{α} has no denotation or value in M with respect to φ. That is, V is intuitively a partial valuation function. For a closed expression A_{α}, it is clear that V_{φ}(A_{α}) does not depend on φ and thus V (A_{α}) is meaningful.

A formula A_{∗} of L is valid in M if V_{φ}(A_{∗}) = t for every V-assignment φ into M.

Theories

A theory of PF^{∗} is a pair T = (L, Γ) where L is a language of PF^{∗} and Γ is a set of sentences of L. The members of Γ are called the axioms of T. T, T′, etc. denote theories.

Let T = (L, Γ). A standard model for T is a standard model for L in which each member of Γ is valid. T is satisfiable (in the standard sense) if there is some standard model for T. A sentence A_{∗} is a (semantic) theorem of T (in the standard sense), written T ⊧ A_{∗}, if A_{∗} is valid in every standard model for T.

5 LUTINS

lutins (Logic of Undefined Terms for Inference in a Natural Style) is the logic of imps. It is essentially the same as PF^{∗} plus several additional expression constructors, which are defined in terms of the primitive notions of PF^{∗}: function application, λ-abstraction, equality, and definite description. This section gives a brief presentation of the syntax and semantics of lutins. A more detailed presentation of a slightly different version of lutins is found in [16].^{5} We assume that each concept and notation defined in the previous section for PF^{∗} is defined for lutins in the obvious way if it is not explicitly defined in this section.

5 The reader should be aware that in [16] lutins is called PF.

Syntax

A language of lutins is a tuple (A, ξ, V, C) such that (A, ξ, V, C̃) is a language of PF^{∗}, where

C̃ = C ∪ {=_{[α,α,∗]}, ι_{[[α,∗],α]} : α ∈ Ω(A)}.

For any language L = (A, ξ, V, C) of lutins, let L̃ be the language (A, ξ, V, C̃) of PF^{∗}.

For the remainder of this section, let L = (A, ξ, V, C) be a language of lutins, S be the sort system (A, ξ), and T be the set of types of S. When there is no possibility of confusion, the components of a language L_{i} will be denoted by A_{i}, ξ_{i}, V_{i}, C_{i}, and the sort system and set of types of L_{i} will be denoted by S_{i} and T_{i}, respectively.

Our version of lutins has 21 expression constructors: apply, lambda,

equals, quasi-equals, iota, iota-p, the-true, the-false, not, and, or,
implies, iff, if-form, forall, forsome, defined-in, is-defined, if,

undefined, and falselike. An expression of L of sort α ∈ S is a finite sequence of variables, constants, expression constructors, sorts, and punctuation symbols defined inductively by:

1. Each x_{α} ∈ V and c_{α} ∈ C is an expression of sort α.

2. If F is an expression of sort [α_{1}, …, α_{n}, β]; A_{1}, …, A_{n} are expressions of sort α′_{1}, …, α′_{n}; and τ(α_{1}) = τ(α′_{1}), …, τ(α_{n}) = τ(α′_{n}), then apply{F, A_{1}, …, A_{n}} is an expression of sort β.

3. If x_{α_{1}}^{1}, …, x_{α_{n}}^{n} are distinct variables and B is an expression of sort β, then lambda{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . B} is an expression of sort [α_{1}, …, α_{n}, β].

4. If A and B are expressions of sort α and β, respectively, with τ(α) = τ(β), then equals{A, B} and quasi-equals{A, B} are expressions of sort ∗.

5. If x_{α}, y_{β} are variables; α, β are of kind ι, ∗, respectively; and C is an expression of sort ∗, then iota{x_{α} . C} and iota-p{y_{β} . C} are expressions of sort α and β, respectively.

6. If A, B, C, A_{1}, …, A_{n} are expressions of sort ∗ with n ≥ 0, then the-true{}, the-false{}, not{A} and{A_{1}, …, A_{n}}, or{A_{1}, …, A_{n}}, implies{A, B}, iff{A, B}, and if-form{A, B, C} are expressions of sort ∗.

7. If x_{α_{1}}^{1}, …, x_{α_{n}}^{n} are distinct variables and B is an expression of sort ∗, then forall{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . B} and forsome{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . B} are expressions of sort ∗.

8. If A is an expression of sort α and τ(α) = τ(β), then defined-in{A, β} and is-defined{A} are expressions of sort ∗.

9. If A, B, C are expressions of sort ∗, β, γ, respectively, with τ(β) = τ(γ), then if{A, B, C} is an expression of sort β ⊔_{ξ} γ.

10. If α is of kind ι, then undefined{α} is an expression of sort α.

11. If α is of kind ∗, then falselike{α} is an expression of sort α.

Expressions that are not variables or constants are called compound expressions. The length of an expression A, written |A|, is the number of occurrences of expression constructors in A. The set of expressions of L [respectively, L_{i}] is denoted by E [respectively, E_{i}], and the set of expressions of L̃ [L̃_{i}] is denoted by Ẽ [Ẽ_{i}].

Semantics

The semantics of lutins is defined in terms of the standard models semantics of PF^{∗}.

Let ζ : E → Ẽ be the mapping defined by the following statements:

1. ζ(a_{α}) = a_{α} where a_{α} ∈ V ∪ C.

2. ζ(apply{F, A_{1}, …, A_{n}}) = @{ζ(F), ζ(A_{1}), …, ζ(A_{n})}.

3. ζ(lambda{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . B}) = λ{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . ζ(B)}.

4. ζ(equals{A_{α}, B_{β}}) = (ζ(A_{α}) =_{γ} ζ(B_{β})) where γ = τ(α) = τ(β).

5. ζ(quasi-equals{A_{α}, B_{β}}) = (ζ(A_{α}) ≃_{γ} ζ(B_{β})) where γ = τ(α) = τ(β).

6. ζ(□{x_{α} . A_{∗}}) = I{x_{α} . ζ(A_{∗})} where □ is iota or iota-p.

7. ζ(□{}) = T_{∗} where □ is the-true or and.

8. ζ(□{}) = F_{∗} where □ is the-false or or.

9. ζ(not{A}) = ¬ζ(A).

10. ζ(and{A_{1}, …, A_{n}}) = (ζ(A_{1}) ∧ (ζ(A_{2}) ∧ ⋯)) where n ≥ 1.

11. ζ(or{A_{1}, …, A_{n}}) = (ζ(A_{1}) ∨ (ζ(A_{2}) ∨ ⋯)) where n ≥ 1.

12. ζ(implies{A, B}) = (ζ(A) ⊃ ζ(B)).

13. ζ(iff{A, B}) = (ζ(A) ≡ ζ(B)).

14. ζ(□{A, B, C}) = if{ζ(A), ζ(B), ζ(C)} where □ is if-form or if.

15. ζ(forall{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . B}) = ∀{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . ζ(B)}.

16. ζ(forsome{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . B}) = ∃{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . ζ(B)}.

17. ζ(defined-in{A, β}) = (ζ(A) ↓ β).

18. ζ(is-defined{A}) = ζ(A)↓.

19. ζ(undefined{α}) = ⊥_{α}.

20. ζ(falselike{α}) = F_{α}.

Notice that A_{α} and ζ(A_{α}) have the same sort for every expression A_{α} of L.

A model for L is a standard model for L̃. Let M = ({D_{α} : α ∈ S}, I) be a model for L, and let V = V^{M} be the valuation function for L̃ with respect to M. U = U^{M} is the binary function, on V-assignments φ into M and expressions A_{α} of L, defined by

U_{φ}(A_{α}) = V_{φ}(ζ(A_{α})).

Clearly, for each V-assignment φ into M and each expression A_{α} of L, U_{φ}(A_{α}) ∈ D_{α} ∪ {⊥} if α ∈ S^{ι} and U_{φ}(A_{α}) ∈ D_{α} if α ∈ S^{∗}. Thus U is a (partial) valuation function for L with respect to M.

A formula A_{∗} of L is valid in M if U_{φ}(A_{∗}) = t for every V-assignment φ into M.

Let M_{i} = ({D_{α}^{i} : α ∈ S_{i}}, I_{i}) be a model for T_{i} = (L_{i}, Γ_{i}) for i = 1, 2. L_{2} is an expansion of L_{1}, written L_{1} ≤ L_{2}, if A_{1} ⊆ A_{2}, ξ_{1} is a subfunction of ξ_{2}, V_{1} ⊆ V_{2}, and C_{1} ⊆ C_{2}. T_{2} is an extension of T_{1}, written T_{1} ≤ T_{2}, if L_{1} ≤ L_{2} and Γ_{1} ⊆ Γ_{2}. M_{2} is an expansion of M_{1} to L_{2} (and M_{2} is the reduct of M_{1} to L_{1}) if D_{α}^{1} = D_{α}^{2} for all α ∈ S_{1} and I_{1} is a subfunction of I_{2}.

6 Theory Interpretation in LUTINS

We have seen that, in first-order predicate logic, an interpretation of one theory in another is a certain kind of homomorphism on expressions that preserves the validity of sentences. In this section we define an interpretation of one lutins theory in another which is very similar to the notion of a standard first-order interpretation. We will first define a notion of a translation from a source theory to a target theory. A translation is determined by how the primitive symbols of the source theory (i.e., the atomic sorts, variables, and constants of the source theory) are associated with objects of the target theory. In the definition given here, atomic sorts are associated with sorts and closed unary predicates; variables are associated with variables; and constants are associated with closed expressions (of appropriate sort). Then an interpretation is defined to be a translation which maps every theorem of the source theory to a theorem of the target theory.

Our notion of a translation in lutins extends the notion of a translation in PF^{∗} defined in [9] in two ways:

– A lutins translation directly handles all 21 expression constructors of lutins, while a PF^{∗} translation handles just the constructors corresponding

   to apply and lambda.

– A lutins translation can associate an atomic sort with either a sort or a closed unary predicate, but a PF^{∗} translation can associate an atomic sort with only a sort.

This section is the heart of the paper. Most of the complexity in the definitions is a result of allowing sorts to be associated with unary predicates.

Quasi-Sorts

Let us define a quasi-sort to be any closed unary predicate, i.e., any expression whose sort is of the form [α, ∗]. Then let Q [Q_{i}] denote the set of quasi-sorts of the language L [L_{i}].

For q ∈ S ∪ Q and A_{α} ∈ E, the domain of q, written δ(q), is defined by

δ(q) = \{ \begin{matrix}q & if q ∈ S \\ α & if q ∈ Q and [α, ∗] is the sort of q \end{matrix}

and, provided δ(q) = α, the condition of q on A_{α}, written κ(q, A_{α}), is defined by

κ(q, A_{α}) = \{ \begin{matrix}the-true\{\} & if q ∈ S \\ apply\{q, A_{α}\} & if q ∈ Q \end{matrix}

We will need a quasi-sort constructor (denoted by [[⋯]]) for building “compound” quasi-sorts that is analogous to the [⋯] sort constructor for building compound sorts. Let q_{1}, …, q_{n+1} ∈ S ∪ Q with n ≥ 1. When δ(q_{n+1}) ∈ S^{ι}, [[q_{1}, …, q_{n+1}]] will be a quasi-sort whose extension (in a model) is the set of partial functions f : D_{1} × ⋯ × D_{n} → D_{n+1}, where D_{i} is the extension of q_{i} for i with 1 ≤ i ≤ n + 1.

[[q_{1}, …, q_{n+1}]] is defined as follows. Let γ = [δ(q_{1}), …, δ(q_{n+1})]. Choose distinct variables f_{γ}, x_{δ(q_{1})}^{1}, …, x_{δ(q_{n})}^{n} which do not occur in q_{1}, …, q_{n+1}. Make the following definitions:

A = and{κ(q_{1}, x_{δ(q_{1})}^{1}), …, κ(q_{n}, x_{δ(q_{n})}^{n})}.
B = apply{f_{γ}, x_{δ(q_{1})}^{1}, …, x_{δ(q_{n})}^{n}}.

C = \{ \begin{matrix}if-form\{A, & if γ is of kind ι \\ implies\{is-defined\{B\}, κ(q_{n+1}, B)\}, \\ not\{is-defined\{B\}\}\} \\ if-form\{A, & if γ is of kind ∗ \\ κ(q_{n+1}, B), \\ equals\{B, falselike\{δ(q_{n+1})\}\}\} \end{matrix}

Then define [[q_{1}, …, q_{n+1}]] to be

lambda{f_{γ} . forall{x_{δ(q_{1})}^{1}, …, x_{δ(q_{n})}^{n} . C}}.

Clearly, for all q_{1}, …, q_{n+1} ∈ S ∪Q, [[q_{1}, …, q_{n+1}]] is a well-formed member of E.

Proposition 6.1

1. If α_{1}, …, α_{n+1} ∈ S, then δ([α_{1}, …, α_{n+1}]) = [δ(α_{1}), …, δ(α_{n+1})].

2. If q_{1}, …, q_{n+1} ∈ S ∪ Q, then δ([[q_{1}, …, q_{n+1}]]) = [δ(q_{1}), …, δ(q_{n+1})].

Translations

Let T_{i} = (L_{i}, Γ_{i}) be a theory of lutins for i = 1, 2. Given a function μ : A_{1} → S_{2} ∪ Q_{2}, μ̄ : S_{1} → S_{2} ∪ Q_{2} is the canonical extension of μ defined inductively by:

1. If α ∈ A_{1}, then μ̄(α) = μ(α).

2. If α = [α_{1}, …, α_{n+1}] ∈ S_{1} and {μ̄(α_{1}), …, μ̄(α_{n+1})} ⊆ S_{2}, then μ̄(α) = [μ̄(α_{1}), …, μ̄(α_{n+1})].

3. If α = [α_{1}, …, α_{n+1}] ∈ S_{1} and {μ̄(α_{1}), …, μ̄(α_{n+1})} ⊈ S_{2}, then μ̄(α) = [[μ̄(α_{1}), …, μ̄(α_{n+1})]].

Given α ∈ A_{1}, let μ[α] = δ(μ(α)), and given α ∈ S_{1}, let μ̄[α] = δ(μ̄(α)).

A translation from T_{1} to T_{2} is a pair (μ, ν), where μ : A_{1} → S_{2} ∪ Q_{2} and ν : V_{1} ∪ C_{1} → E_{2}, such that:

1. μ(∗) = ∗.

2. For all α ∈ A_{1} with α ≠ ∗, μ[α] is a sort of type τ(μ̄[τ(α)]) of kind ι.

3. For all x_{α} ∈ V_{1}, ν(x_{α}) is a variable of sort μ̄[α].

4. ν is injective on V_{1}.

5. For all c_{α} ∈ C_{1}, ν(c_{α}) is a closed expression of type τ(μ̄[α]).

(μ, ν) is normal if μ(α) ∈ S_{2} for all α ∈ A_{1}. Obviously, μ̄[α] = μ̄(α) for all α ∈ S_{1} if (μ, ν) is normal.

Let Φ = (μ, ν) be a translation from T_{1} to T_{2} throughout the rest of this section. For A ∈ E_{1}, the translation of A via Φ, written Φ(A), is the member of E_{2} defined inductively by:

1. Φ(a) = ν(a) if a ∈ V_{1} ∪ C_{1}.

2. Φ(□{A_{1}, …, A_{n}}) = □{Φ(A_{1}), …, Φ(A_{n})} if □ is apply, equals,

quasi-equals, the-true, the-false, not, and, or, implies, iff, if-form,
is-defined, or if.

3. Φ(□{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . B}) = □{Φ(x_{α_{1}}^{1}), …, Φ(x_{α_{n}}^{n}) . Φ(B)} if □ is lambda, iota, iota-p, forall, or forsome and {μ̄(α_{1}), …, μ̄(α_{n})} ⊆ S_{2}.

4. Φ(□{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . B}) =

□{Φ(x_{α_{1}}^{1}), …, Φ(x_{α_{n}}^{n}) . if{C, Φ(B), □′{γ}}} if □ is lambda
□{Φ(x_{α_{1}}^{1}), …, Φ(x_{α_{n}}^{n}) . implies{C, Φ(B)}} if □ is forall
□{Φ(x_{α_{1}}^{1}), …, Φ(x_{α_{n}}^{n}) . and{C, Φ(B)}}  if □ is forsome,

                                            iota, or iota-p

if {μ̄(α_{1}), …, μ̄(α_{n})} ⊈ S_{2}, where

C = and{κ(μ̄(α_{1}), Φ(x_{α_{1}}^{1})), …, κ(μ̄(α_{n}), Φ(x_{α_{n}}^{n}))},

γ is the sort of Φ(B), and □′ is undefined [falselike] if γ is of kind ι [∗].

5. Φ(□{α}) = □{μ̄[α]} if □ is undefined or falselike.

6. Φ(defined-in\{A, β\}) = \{ \begin{matrix}defined-in\{Φ(A), μ̄(β)\} & if μ̄(β) ∈ S_{2} \\ apply\{μ̄(β), Φ(A)\} & if μ̄(β) ∈ Q_{2} \end{matrix}

Proposition 6.2 Let α, β ∈ S_{1}.

1. α and μ̄[α] are of the same kind.

2. τ(μ̄[α]) = τ(μ̄[τ(α)]).

3. τ(α) = τ(β) implies τ(μ̄[α]) = τ(μ̄[β]).

Proof The same as the proof of Proposition 11.1 in [9].□

Proposition 6.3 Let A_{α} ∈ E_{1}.

1. Φ(A_{α}) is a (well-formed) member of E_{2} of type τ(μ̄[α]).

2. If the sort of ν(c_{γ}) is μ̄[γ] for each constant c_{γ} occurring in A_{α}, then the sort of Φ(A_{α}) is μ̄[α].

Proof By induction on |A_{α}|.□

Before proceeding to the notion of an interpretation, we shall make a few comments about this definition of a translation:

– The mapping μ plays the role of U in a standard translation.

– The variables of the source theory are injectively mapped to the variables of the target theory by both a standard and lutins translation. In (singlesorted) first-order logic, variables all have effectively the same sort. Consequently, they can be uniformly mapped to themselves and need not be in the domain of ν in a standard translation. Although variables have different sorts in a sorted logic such as lutins, one might think that a variable of the form x_{α} could be uniformly mapped to x_{μ̄[α]}. However, this mapping would clearly not be injective if there exists variables x_{α}, x_{β} ∈ V_{1} such that α ≠ β and μ̄[α] = μ̄[β]. Therefore, in our definition of Φ, the mapping of variables is specified explicitly by ν.

– Since simple type theory has a more uniform syntax than first-order logic, the definition of ν on constants is less complicated in a lutins translation than in a standard translation.

– A normal lutins translation preserves the structure of lutins syntax, as can be seen clearly by the definition given above.

– In some cases, a nonnormal lutins translation relativizes the constructor defined-in and the variable-binding constructors: lambda, iota, iota-p, forall, forsome. For each of these expression constructors, the relativization is defined in the obvious way. In particular, the relativization of lambda in an expression A = lambda{x_{α_{1}}^{1}, …, x_{α_{n}}^{n} . B} produces an expression beginning with lambda which is the appropriate restriction of the unrelativized translation of A.

Interpretations

Φ is an interpretation of T_{1} in T_{2} if Φ(A_{∗}) is a theorem of T_{2} for each theorem A_{∗} of T_{1}. T_{1} is interpretable in T_{2} if there is an interpretation of T_{1} in T_{2}.

A pre-obligation of Φ is any one of the following theorems of T_{1}:

1. An axiom of T_{1}.

2. forsome{x_{α} . the-true{}} where α ∈ A_{1}.

3. defined-in{c_{α}, α} where c_{α} ∈ C_{1}.

4. forall{x_{α} . defined-in{x_{α}, ξ_{1}(α)}} where α ∈ A_{1}.

An obligation of Φ is any sentence Φ(A_{∗}) where A_{∗} is a pre-obligation of Φ. The four kinds of pre-obligations [obligations] are called, in order, axiom, sort nonemptiness, constant sort, and sort inclusion pre-obligations [obligations]. Note: The sort nonemptiness obligations of Φ are trivially theorems of T_{2} if Φ is normal.

The first three kinds of obligations correspond very closely to the four kinds of obligations for a standard first-order translation (constant sort obligations correspond to both individual constant symbol and function symbol obligations). There are no standard translation obligations corresponding to sort inclusion obligations because there are no subtypes in first-order logic. Obligations serve the same purpose for lutins translations as they do for standard translations: if all of the obligations of a translation are theorems of the target theory, then the translation is an interpretation. This result is proved for lutins in Section 8.

7 Some Examples Involving Groups and Fields

In this section we construct some interpretations of a theory G of an abstract group in a theory F of an abstract field. We will employ the following abbreviations:

– F (A_{1}, …, A_{n}) for apply{F, A_{1}, …, A_{n}}.

– A = B for equals{A, B}.

– A ≠ B for ¬{equals{A, B}}.

Define G = ((A_{G}, ξ_{G}, V_{G}, C_{G}), Γ_{G}) to be a theory of an abstract group where:

1. A_{G} = {∗, α}.

2. ξ_{G} is the identity function.

3. C_{G} = {e_{α}, mul_{[α,α,α]}, inv_{[α,α]}}.

4. Γ_{G} is the usual set of axioms for a group.

Define F = ((A_{F} , ξ_{F} , V_{F} , C_{F}), Γ_{F}) to be a theory of an abstract field where:

1. A_{F} = {∗, β}.

2. ξ_{F} is the identity function.

3. C_{F} = {0_{β}, 1_{β}, +_{[β,β,β]}, ×_{[β,β,β]}}.

4. Γ_{F} is the usual set of axioms for a field.

Except for V_{G} and V_{F}, the languages of G and F are determined by the conditions given above.

Example 7.1 Let Φ_{1} = (μ_{1}, ν_{1}) be an interpretation of G in F such that:

1. μ_{1}(α) = β.

2. ν_{1}(e_{α}) = 0_{β}.

3. ν_{1}(mul_{[α,α,α]}) = +_{[β,β,β]}.

4. ν_{1}(inv_{[α,α]}) = lambda{x_{β} . iota{y_{β} . +_{[β,β,β]}(x_{β}, y_{β}) = 0_{β}}}.

Φ_{1} shows that the elements of a field form a group under addition.□

Example 7.2 Let Φ_{2} = (μ_{2}, ν_{2}) be an interpretation of G in F such that:

1. μ_{2}(α) = lambda{x_{β} . x_{β} ≠ 0_{β}}.

2. ν_{2}(e_{α}) = 1_{β}.

3. ν_{2}(mul_{[α,α,α]}) = lambda{x_{β}, y_{β} . if{and{x_{β} ≠ 0_{β}, y_{β} ≠ 0_{β}}, ×_{[β,β,β]}(x_{β}, y_{β}),

                                 undefined{β}}}.

4. ν_{2}(inv_{[α,α]}) = lambda{x_{β} . iota{y_{β} . ×_{[β,β,β]}(x_{β}, y_{β}) = 1_{β}}}.

Φ_{2} shows that the nonzero elements of a field form a group under multiplication. Since α is associated with a quasi-sort, Φ_{2} is nonnormal and thus relativizes the quantifiers in expressions of G. Notice that mul_{[α,α,α]} is associated with the restriction of ×_{[β,β,β]} to the nonzero elements of β, and ν_{2}(inv_{[α,α]}) is undefined at 0_{β}.□

Now define F′ = ((A_{F} ∪ {γ}, ξ_{F′}, V_{F′}, C_{F}), Γ_{F} ∪ {A_{∗}}) to be an extension of F such that:

1. ξ_{F′}(γ) = β.

2. A_{∗} = forall{x_{β} . iff{defined-in{x_{β}, γ}, x_{β} ≠ 0_{β}}}.

Thus F′ is obtained by defining in F an atomic sort γ with the same extension as the quasi-sort lambda{x_{β} . x_{β} ≠ 0_{β}}.

Example 7.3 Let Φ_{3} = (μ_{3}, ν_{3}) be an interpretation of G in F′ such that:

1. μ_{3}(α) = γ.

2. ν_{3}(e_{α}) = 1_{β}.

3. ν_{3}(mul_{[α,α,α]}) = lambda{x_{γ}, y_{γ} . ×_{[β,β,β]}(x_{γ}, y_{γ})}.

4. ν_{3}(inv_{[α,α]}) = lambda{x_{γ} . iota{y_{γ} . ×_{[β,β,β]}(x_{γ}, y_{γ}) = 1_{β}}}.

Like Φ_{2}, Φ_{3} shows that the nonzero elements of a field form a group under multiplication. In a certain sense, Φ_{2} and Φ_{3} are two renditions of the same interpretation. However, since Φ_{3} associates α with a sort, Φ_{3} is syntactically more economical than Φ_{2}. In particular, Φ_{3} is normal while Φ_{2} is nonnormal.□

Examples 7.2 and 7.3 together illustrate how a nonnormal translation can be transformed into a normal translation. Since lutins admits subtypes, any nonnormal translation can be “normalized” in this way as long as one is willing to define new atomic sorts. The general idea is as follows. Suppose the translation Φ is nonnormal. For each α ∈ A_{1} such that μ(α) ∉ S_{2}, (1) add to T_{2} a new atomic sort α′ and a new axiom which says that μ(α) and α′ are coextensional and (2) redefine μ so that μ(α) = α′. The resulting translation is obviously normal. (This construction is described in detail in the next section.) Hence, nonnormal translations are unnecessary in lutins if there is no restriction on defining atomic sorts. However, in practice the strict avoidance of nonnormal translations can easily lead to theories with a large number of atomic sorts which are almost never used.

8 Interpretation and Satisfiability Theorems

We prove in this section the interpretation and relative satisfiability theorems for lutins. The former establishes a sufficient condition for a translation to be an interpretation, and the latter says that a theory which is interpretable in a satisfiable theory is itself satisfiable. They correspond, respectively, to the Standard Interpretation Theorem (Theorem 2.1) and Standard Relative Satisfiability (Theorem 2.2) for first-order logic. The proofs are based on the interpretation and relative satisfiability theorems for PF^{∗} proved in [9].

Let T_{i} = (L_{i}, Γ_{i}) be a lutins theory for i = 1, 2.

PF^{∗} Theories and Translations

Given a lutins theory T = (L, Γ), let T̃ = (L̃, {ζ(A_{∗}) : A_{∗} ∈ Γ }), which is a PF^{∗} theory.

Proposition 8.1 Let T = (L, Γ) be a lutins theory and M be a model for L. Then:

1. M is a model for T iff M is a standard model for T̃.

2. T ⊧ A_{∗} iff T̃ ⊧ ζ(A_{∗}), for all sentences A_{∗} ∈ E.

Proof Let φ be a V-assignment into M and A_{∗} be a formula of L. Then, by definition, U_{φ}^{M}(A_{∗}) = V_{φ}^{M}(ζ(A_{∗})). This identity implies (1), and (1) and the identity imply (2).□

Suppose Φ_{n} = (μ, ν) is a normal lutins translation from T_{1} to T_{2}. Let Φ̃_{n} = (μ, ν̃) where ν̃ : V_{1} ∪ C̃_{1} → Ẽ_{2} is defined by:

1. For all x_{α} ∈ V_{1}, ν̃(x_{α}) = ν(x_{α}).

2. For all c_{α} ∈ C_{1}, ν̃(c_{α}) = ζ(ν(c_{α})).

3. For all α ∈ S_{1}, ν̃(=_{[α,α,∗]}) = =_{[μ̄(α),μ̄(α),∗]} and ν̃(ι_{[[α,∗],α]}) = ι_{[[μ̄(α),∗],μ̄(α)]}.

Φ̃_{n} is easily verified to be a PF^{∗} translation from T̃_{1} to T̃_{2}. For E ∈ Ẽ_{1}, let Φ̃_{n}(E) = ν̃(E), the translation of E via Φ̃_{n}.

The key lemma of this section is

Lemma 8.2 Let Φ be a normal lutins translation from T_{1} to T_{2} such that each of its constant sort and sort inclusion obligations is a theorem of T_{2}. Also, let M_{2} be a model for T_{2} and φ be a V_{2}-assignment into M_{2}. Then:

1. V_{φ}^{M_{2}}(ζ(Φ(E))) = V_{φ}^{M_{2}}(Φ̃(ζ(E))), for all expressions E ∈ E_{1}.

2. T̃_{2} ⊧ ζ(Φ(A_{∗})) iff T̃_{2} ⊧ Φ̃(ζ(A_{∗})), for all sentences A_{∗} ∈ E_{1}.

The proof of this lemma requires the following technical lemma:

Lemma 8.3 Let Φ = (μ, ν) be a normal lutins translation from T_{1} to T_{2} such that each of its constant sort and sort inclusion obligations is a theorem of T_{2}. Also, let M_{2} be a model for T_{2}, φ be a V_{2}-assignment into M_{2}, and A_{α}, B_{β}, C_{γ}, X_{∗} ∈ E_{1}. Then:

1. If □ ∈ {=, ≃}, δ is the type of Φ(A_{α}), and ϵ = μ̄(τ(α)), then V_{φ}^{M_{2}}(E^{δ}) =

V_{φ}^{M_{2}}(E^{ϵ}) where

E^{θ} = ζ(Φ(A_{α})) □_{θ} ζ(Φ(B_{β})).

2. If δ is the least upper bound in ⪯_{ξ_{2}} of the sorts of Φ(B_{β}) and Φ(C_{γ}), and ϵ = μ̄(β ⊔_{ξ_{2}} γ), then V_{φ}^{M_{2}}(E^{δ}) = V_{φ}^{M_{2}}(E^{ϵ}) where

E^{θ} = I{x_{θ} . (ζ(Φ(X_{∗})) ⊃ (x_{θ} =_{θ} ζ(Φ(B_{β})))) ∧
(¬ζ(Φ(X_{∗})) ⊃ (x_{θ} =_{θ} ζ(Φ(C_{γ}))))}.

3. If δ is the sort of Φ(A_{α}) and ϵ = μ̄(α), then V_{φ}^{M_{2}}(E^{δ}) = V_{φ}^{M_{2}}(E^{ϵ}) where

E^{θ} = (ζ(Φ(A_{α})) ↓ θ).

Proof Follows from the lemmas in Section 11 of [9].□

Proof of Lemma 8.2 Part (2) follows from part (1) by Proposition 8.1. Let Φ = (μ, ν) and E ∈ E_{1}. The proof of (1) is by induction on |E|. Basis. Assume |E| = 0; then E ∈ V_{1} ∪ C_{1}. Let E ∈ V_{1}. Then

V_{φ}^{M_{2}}(ζ(Φ(E))) = V_{φ}^{M_{2}}(Φ(E))  (1)
= V_{φ}^{M_{2}}(Φ̃(E))  (2)
= V_{φ}^{M_{2}}(Φ̃(ζ(E)))  (3)

(1) and (3) hold since ζ is the identity on V_{1}, and (2) holds since Φ = Φ̃ on V_{1}. Let E ∈ C_{1}. Then

V_{φ}^{M_{2}}(ζ(Φ(E))) = V_{φ}^{M_{2}}(Φ̃(E))  (4)
= V_{φ}^{M_{2}}(Φ̃(ζ(E)))  (5)

(4) holds since ζ ∘ Φ = Φ̃ on C_{1}, and (5) holds since ζ is the identity on C_{1}. Induction step. Assume |E| > 0; then E is a compound expression beginning

with the expression constructor □.

Let E = defined-in{A_{α}, β}. Then

V_{φ}^{M_{2}}(ζ(Φ(defined-in{A_{α}, β})))
= V_{φ}^{M_{2}}(ζ(defined-in{Φ(A_{α}), μ̄(β)}))  (6)
= V_{φ}^{M_{2}}(ζ(Φ(A_{α})) ↓ μ̄(β))  (7)
= V_{φ}^{M_{2}}(Φ̃(ζ(A_{α})) ↓ μ̄(β))  (8)
= V_{φ}^{M_{2}}(Φ̃(ζ(A_{α}) ↓ β))  (9)
= V_{φ}^{M_{2}}(Φ̃(ζ(defined-in{A_{α}, β})))  (10)

(6) is by the definition of the application of a normal lutins translation to an expression; (7) and (10) are by the definition of ζ; (8) is by the induction hypothesis; and (9) is by Lemma 11.5 in [9].

The derivation is very similar when □ is any one of the other expression constructors except for equals, quasi-equals, if, or is-defined. The derivations for these last four expression constructors require Lemma 8.3.

This completes the proof.□

A Special Case of the Interpretation Theorem

Lemma 8.2 and the Semantic Interpretation Theorem for PF^{∗} imply the Interpretation Theorem for lutins restricted to normal translations:

Theorem 8.4 A normal lutins translation from T_{1} to T_{2} is an interpretation if each of its obligations is a theorem of T_{2}.

Proof Let Φ be a normal lutins translation from T_{1} to T_{2} such that each of its obligations is a theorem of T_{2}.

We begin by showing that Φ̃ is an interpretation. Let O be an obligation of Φ̃. Then O has the form Φ̃(ζ(A_{∗})) where A_{∗} is an axiom, constant sort, or sort inclusion pre-obligation of Φ. By hypothesis, T_{2} ⊧ Φ(A_{∗}). Then

T_{2} ⊧ Φ(A_{∗}) iff T̃_{2} ⊧ ζ(Φ(A_{∗}))  (11)
iff T̃_{2} ⊧ Φ̃(ζ(A_{∗}))  (12)

(11) holds by Proposition 8.1, and (12) holds by Lemma 8.2. Hence, each obligation of Φ̃ is a theorem of T̃_{2}, and so Φ̃ is a PF^{∗} interpretation by the Semantic Interpretation Theorem for PF^{∗} [9, Theorem 12.4].

Let A_{∗} be a theorem of T_{1}. Then

T_{1} ⊧ A_{∗} iff T̃_{1} ⊧ ζ(A_{∗})  (13)
implies T̃_{2} ⊧ Φ̃(ζ(A_{∗}))  (14)
iff T̃_{2} ⊧ ζ(Φ(A_{∗}))  (15)
iff T_{2} ⊧ Φ(A_{∗})  (16)

(13) and (16) hold by Proposition 8.1; (14) holds because Φ̃ is a PF^{∗} interpretation; and (15) holds by Lemma 8.2. Therefore, the sequence of implications shows that Φ maps each theorem of T_{1} to a theorem of T_{2}, that is, that Φ is an interpretation.□

The Translation Φ′ and Its Properties

Before we can strengthen Theorem 8.4 to the full interpretation theorem for lutins, we must show how an arbitrary lutins translation can be transformed into a normal translation.

Let Φ = (μ, ν) be a lutins translation from T_{1} to T_{2}. The key idea is to add new atomic sorts to T_{2}. Let T′_{2} = (L′_{2}, Γ′_{2}) be the theory

((A ∪ A_{2}, ξ ∪ ξ_{2}, V ∪ V_{2}, C_{2}), Γ ∪ Γ_{2})

such that:

1. A = {γ^{μ(α)} : α ∈ A_{1} and μ(α) ∈ Q_{2}}.

2. ξ : A → A_{2} and ξ(γ^{Q_{[α,∗]}}) = α.

3. V is an appropriate set of new variables.

4. Γ = {A^{Q_{[α,∗]}} : γ^{Q_{[α,∗]}} ∈ A} where A^{Q_{[α,∗]}} is

forall{x_{τ(α)} . iff{defined-in{x_{τ(α)}, γ^{Q_{[α,∗]}}}, apply{Q_{[α,∗]}, x_{τ(α)}}}}.

T′_{2} is a “definitional” extension of T_{2}; its new atomic sorts are axiomatically defined to be coextensional with the quasi-sorts in the range of μ. Consequently, the following proposition is easy to prove.

Proposition 8.5 Suppose each sort nonemptiness obligation of Φ is a theorem of T_{2}. Then:

1. Each model for T_{2} expands to a model for T′_{2}.

2. Each model for T′_{2} reduces to a model for T_{2}.

Let Φ′ = (μ′, ν′) be a translation from T_{1} to T′_{2} such that:

1. If μ(α) ∈ S_{2}, then μ′(α) = μ(α).

2. If μ(α) ∈ Q_{2}, then μ′(α) = γ^{μ(α)}.

3. If c_{α} ∈ C_{1}, then ν′(c_{α}) = ν(c_{α}).

Φ′ is clearly normal. Notice that Φ ≠ Φ′ on V_{1} unless Φ is normal.

Lemma 8.6 Let M_{2} and M′_{2} be models for T_{2} and T′_{2}, respectively, such that M′_{2} is an expansion of M_{2}. Then

U_{φ}^{M_{2}}(Φ(E)) = U_{φ′}^{M′_{2}}(Φ′(E))

for all E ∈ E_{1}, V_{2}-assignments φ into M_{2}, and V′_{2}-assignments φ′ into M′_{2} such that φ(Φ(x_{α})) = φ′(Φ′(x_{α})) for all x_{α} ∈ V_{1}.

Proof By induction on |E|.□

Lemma 8.7 Suppose each sort nonemptiness obligation of Φ is a theorem of T_{2}. Then

T_{2} ⊧ Φ(A_{∗}) iff T′_{2} ⊧ Φ′(A_{∗})

for all sentences A_{∗} ∈ E_{1}.

Proof By Proposition 8.5 and Lemma 8.6.□

The Theorems

Theorem 8.8 (Interpretation Theorem) A translation from T_{1} to T_{2} is an interpretation if each of its obligations is a theorem of T_{2}.

Proof Let Φ be a lutins translation from T_{1} to T_{2} such that each of its obligations is a theorem of T_{2}. As above, construct the theory T′_{2} from T_{2} and the normal translation Φ′ from Φ. Since Φ and Φ′ have the same source theory, they also have the same pre-obligations. Hence, each obligation of Φ′ is a theorem of T′_{2} by Lemma 8.7. Φ′ is normal, so Φ′ is an interpretation by Theorem 8.4. This implies that Φ is an interpretation by Lemma 8.7.□

Theorem 8.9 (Relative Satisfiability) If T_{1} is interpretable in T_{2} and T_{2} is satisfiable, then T_{1} is satisfiable.

Proof Let Φ be a lutins interpretation of T_{1} in T_{2} and M_{2} be a model for T_{2}. As above, construct the theory T′_{2} from T_{2} and the normal translation Φ′ from Φ. By Proposition 8.5, there is a model M′_{2} for T′_{2} which is an expansion of M_{2} since Φ is an interpretation. M′_{2} is also a standard model for T̃′_{2} by Proposition 8.1. By Lemma 8.7, Φ′ is an interpretation, and so by the proof of Theorem 8.4, Φ̃′ is a also an interpretation. Therefore, there is a standard model M_{1} for T̃_{1} by Relative Satisfiability for PF^{∗} [9, Theorem 12.3]. M_{1} is also a model for T_{1} by Proposition 8.1, so T_{1} is satisfiable.□

9 Conclusion

In this paper we have developed a method for theory interpretation in lutins, a version of simple type theory which supports partial functions and subtypes. The method embodies the principal characteristics of the standard approach to theory interpretation in first-order logic:

– A translation is a kind of homomorphism that is determined by how the primitive symbols of the source theory are associated with objects of the target theory.

– When sort symbols are associated with unary predicates, the translation of an expression may involve the relativization of variable-binding constructors such as the universal and existential quantifiers.

– A translation is an interpretation if the “obligations” of the translation are theorems of the target theory (interpretation theorem).

– A theory which is interpretable in a satisfiable theory is itself satisfiable (relative satisfiability).

Since the method is based on a logic with partial functions and subtypes, it has two advantages over the standard first-order approach:

– The functions with restricted domains that naturally arise from interpretations which associate base types with subtypes are handled directly as partial functions.

– Relativization of variable-binding constructors can be avoided completely, provided that appropriate sort symbols are defined.

The method is intended as a guide for theory interpretation in classical simple type theories as well as in predicate logics which admit partial functions.

Acknowledgments

I am grateful for the suggestions received from the referees. Many of the ideas in this paper grew out of conversations I have had with Dr. Joshua Guttman and Dr. Javier Thayer in the course of developing imps.

References

1. P. B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth through Proof. Academic Press, 1986.

2. P. B. Andrews, S. Issar, D. Nesmith, and F. Pfenning. The tps theorem proving system (system abstract). In M. E. Stickel, editor, 10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Computer Science, pages 641–642. Springer-Verlag, 1990.

3. C. C. Chang and H. J. Keisler. Model Theory. North-Holland, 1990.

4. A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.

5. D. Craigen, S. Kromodimoeljo, I. Meisels, A. Neilson, B. Pase, and M. Saaltink. m-eves: A tool for verifying software. In 11th International Conference on Software Engineering (ICSE’11), Singapore, 1988.

6. D. Craigen, S. Kromodimoeljo, I. Meisels, B. Pase, and M. Saaltink. eves: An overview. Technical Report CP-91-5402-43, ORA Corporation, 1991.

7. H. B. Enderton. A Mathematical Introduction to Logic. Academic Press, 1972.

8. W. M. Farmer. A partial functions version of Church’s simple theory of types. Journal of Symbolic Logic, 55:1269–1291, 1990.

9. W. M. Farmer. A simple type theory with partial functions and subtypes. Annals of Pure and Applied Logic, 64:211–240, 1993.

10. W. M. Farmer, J. D. Guttman, and F. J. Thayer. imps: System description. In D. Kapur, editor, Automated Deduction—CADE-11, volume 607 of Lecture Notes in Computer Science, pages 701–705. Springer-Verlag, 1992.

11. W. M. Farmer, J. D. Guttman, and F. J. Thayer. Little theories. In D. Kapur, editor, Automated Deduction—CADE-11, volume 607 of Lecture Notes in Computer Science, pages 567–581. Springer-Verlag, 1992.

12. W. M. Farmer, J. D. Guttman, and F. J. Thayer. imps: an Interactive Mathematical Proof System. Journal of Automated Reasoning, 11:213–248, 1993.

13. F. Giunchiglia and T. Walsh. A theory of abstraction. Artificial Intelligence, 57:323–389, 1992.

14. J. A. Goguen and T. Winkler. Introducing obj3. Technical Report sri-csl-99-9, sri International, August 1988.

15. M. J. C. Gordon. hol: A proof generating system for higher-order logic. In G. Birtwistle and P. A. Surahmanyam, editors, VLSI Specification, Verification, and Synthesis, pages 73–128. Kluwer, 1987.

16. J. D. Guttman. A proposed interface logic for verification environments. Technical Report M91-19, The mitre Corporation, 1991.

17. R. W. Harper and F. Pfenning. A module system for a programming language based on the LF logical framework. Journal of Functional Programming. Forthcoming.

18. D. Hilbert. The Foundations of Geometry. Open Court, Chicago, 1902.

19. K. Kunen. Set Theory: An Introduction to Independence Proofs. North-Holland, 1980.

20. B. H. Levy. An Approach to Compiler Correctness Using Interpretation Between Theories. PhD thesis, University of California, Los Angeles, 1986. Also Technical Report ATR-86(8454)-4, The Aerospace Corporation, El Segundo, California.

21. T. S. E. Maibaum, P. A. S. Veloso, and M. R. Sadler. A theory of abstract data types for program development: Bridging the gap? In H. Ehrig, C. Floyd, M. Nivat, and J. Thatcher, editors, Formal Methods and Software Development, Volume 2, volume 186 of Lecture Notes in Computer Science, pages 214–230. Springer-Verlag, 1985.

22. J. D. Monk. Mathematical Logic. Springer-Verlag, 1976.

23. J. Mycielski. A lattice of interpretability types of theories. Journal of Symbolic Logic, 42:297–305, 1977.

24. R. Nakajima and T. Yuasa, editors. The iota Programming System, volume 160 of Lecture Notes in Computer Science. Springer-Verlag, 1982.

25. T. Nipkow and L. C. Paulson. Isabelle-91. In D. Kapur, editor, Automated Deduction—CADE-11, volume 607 of Lecture Notes in Computer Science, pages 673–676. Springer-Verlag, 1992.

26. S. Owre, J. M. Rushby, and N. Shankar. pvs: A prototype verification system. In D. Kapur, editor, Automated Deduction—CADE-11, volume 607 of Lecture Notes in Computer Science, pages 748–752. Springer-Verlag, 1992.

27. J. Rushby, F. von Henke, and S. Owre. An introduction to formal specification and verification using ehdm. Technical Report sri-csl-91-02, sri International, 1991.

28. J. R. Shoenfield. Mathematical Logic. Addison-Wesley, 1967.

29. D. R. Smith and M. R. Lowry. Algorithmic theories and design tactics. Science of Computer Programming, 14:305–321, 1990.

30. L. W. Szczerba. Interpretability of elementary theories. In R. E. Butts and J. Hintikka, editors, Logic, Foundations of Mathematics, and Computability Theory, pages 129–145. Reidel, 1977.

31. L. W. Szczerba. Interpretability and axiomatizability. Bulletin de L’Académie Polonaise des Sciences, 27:425–429, 1979.

32. A. Tarski, A. Mostowski, and R. M. Robinson. Undecidable theories. North-Holland, 1953.

33. W. M. Turski and T. S. E. Maibaum. The Specification of Computer Programs. Addison-Wesley, 1987.

34. J. van Bentham and D. Pearce. A mathematical characterization of interpretation between theories. Logica Studia, 43:295–303, 1984.

35. P. J. Windley. Formal modeling and verification of microprocessors. IEEE Transactions on Computers. Forthcoming.

36. P. J. Windley. Abstract theories in hol. In L. Claesen and M. J. C. Gordon, editors, Proceedings of the 1992 International Workshop on the hol Theorem Prover and its Applications. North-Holland, November 1992.

This article was processed using the LaTEX macro package with LLNCS style