Common Logic: Abstract Syntax and Semantics

Common Logic Working Group

Introduction

The purpose of this document is to provide an abstract syntax for the Common Logic standard and a corresponding semantics. The idea here is to provide a syntax at a sufficiently high level of abstraction that it can be satisfied by many "concrete" languages — e.g., KIF, Conceptual Graphs, or the familiar Principia-style syntax found in most mathematical logic texts. In the development of a standard language and semantics for use in Ontology and Knowledge Engineering generally, one can take two approaches to this diversity. One approach is simply to legislate that one particular syntax shall be the standard. This, of course, would be the simplest solution, but quite likely the least effective, as it would marginalize those who prefer other languages, many of whom would not be inclined to change. The other approach is to specify a standard at a higherxter level of abstraction, which, at that level, can encompass all of the distinct concrete languages. CL has chosen the latter path; it does not privilege any one in a large class of concrete languages over another. Nevertheless, it still offers the advantages of the single language approach: Because all compliant languages are, at CL's level of abstraction, the "same" language, translation between those languages — guided by specifications detailing how each language exemplifies the abstract CL syntax — will be straightforward.

Syntax

Lexicon

A CL language is based upon an initial stock of primitive syntactic entities. Specifically, a CL lexicon λ consists of the following mutually disjoint sets:

A countable set Con called the constants of λ.
A denumerable set OrdVar called the ordinary variables of λ;
A (possibly empty) set SeqVar called the sequence variables of λ. If nonempty, SeqVar is denumerable.¹

We stipulate that Con, OrdVar and SeqVar be pairwise disjoint. Var = OrdVar ∪ SeqVar is known as the set of variables of λ. Let PrimTrm = Con ∪ Var; PrimTrm is known as the set of primitive terms of λ.

Note that, unlike traditional logical languages, there is no distinction between individual constants and predicates in CL lexicon. This reflects the underlying perspective that everything is a "first-class" logical citizen.

CL Languages

Every CL lexicon determines a class of languages. Structurally speaking, these languages are all identical, insofar as they all satisfy the same abstract conditions. They differ only in the details of their outward form. We will illustrate this below.

Term Classes

For any set M, let M* be the set of finite sequences of elements of M, i.e., M* = ∪_0≤n<ωMⁿ, where Mⁿ is the set of all n-tuples of elements of M.

Say that T is a term class for λ if T is a smallest class that includes PrimTrm and is closed under an operation App — called a generator for T — such that

App is one-to-one;
App : (T – SeqVar) × T* → T.²

For any term class Trm for λ, let FuncTrm = Range(App),³ where App is a generator for Trm, and let SingTrm = Trm – SeqVar. FuncTrm is the set of function terms of λ (relative to Trm), and SingTrm is the class of singular terms of λ (relative to Trm).

Formula classes

Let λ be a CL lexicon, and let Trm be a term class for λ. Let FuncTrm be the class of function terms of λ relative to Trm and SingTrm the class of singular terms of λ relative to Trm. Let Atom be a one-to-one function on FuncTrm and let AtomicFla be the range of Atom. Say that F is a formula class for λ, relative to Trm, if it is a smallest class that includes AtomicWff and is closed under a set Op — known as a generator set for F — of operations Atom, Id, Neg, Conj, Disj, Cond, Bicond, ExQuant, UnivQuant that satisfy the following conditions:

Each operation is one-to-one;
The ranges of the operations are pairwise disjoint, and disjoint from Trm
Id : SingTrm × SingTrm → F
Neg : F → F
Conj : F* → F
Disj : F* → F
Cond : F × F → F
BiCond : F × F → F
ExQuant : (Var ∪ (Var × Con))* × F → F
UnivQuant : (Var ∪ (Var × Con))* × F → F

The clauses for "quantified" formulas here, i.e., those entities in the ranges of ExQuant and UnivQuant, allow for the use of restricted quantifiers. Thus, in a KIF-like implementation of CL, these clauses would allow such formulas as

(forall ((?x Boy))
        (exists ((?y Girl))
                (Kissed ?x ?y)))

to represent "Every boy kissed a girl."

Note that, because the operations in a generator set for a formula class Fla for λ are all one-to-one and disjoint in their ranges, every element of Fla will have exactly one "decomposition" under the inverses of those operations, and that all such decompositions are finite. ⁴

Let φ ∈ Fla. An object ε in the decomposition of φ is an atom of φ just in case ε is element of the lexicon λ. φ is atomic if φ ∈ AtomicWff. ψ is a subformula of φ if ψ ∈ Fla and ψ is in the decomposition of φ.

We define a CL language to be a formula class Fla for a CL lexicon λ. If L = Fla is a CL language, where Fla is formula class for λ relative to Trm, then we say that L is a language for λ (alternatively, that λ underlies L), and we say that Trm is the set of terms of L. L is said to be first-order if SeqVar = ∅. If λ and λ′ are CL lexicons with the same sets of constants and L and L′ are CL languages for λ and λ′, respectively, then L and L′ are said to be equivalent.

Semantics

Interpretations

Let L be a CL language for λ, and let Trm be the terms of L. A CL interpretation I for L is a 4-tuple ⟨D,ext,skol,V⟩ satisfying the following conditions. First, D = A ∪ R is a nonempty set such that A ∩ R = ∅. Intuitively, A represents the set of individuals of I and R the set of relations-in-intension (though, as will be seen, it is possible to think of them extensionally as sets). ext is a function from D into D*, though we stipulate that, for all a ∈ A, ext(a) = ∅. Intuitively, ext represents the extension of every relation. However, to smooth the semantics for the highly unrestricted syntax of CL languages, in which there is no syntactic distinction between individual constants and predicates, the individuals of D are assigned extensions as well, albeit always empty ones — thus, the result of predicating one individual of another, while semantically meaningful, will always yield falsehood.

The purpose of skol is to enable the definition of reasonable denotations for function terms when the term occurring in function position in such a term does not denote a total function (i.e., denotes either a partial function, a non-functional relation, or an individual). Toward that end, for ⟨e₁, …, e_n⟩ ∈ D*, say that an object e ∈ D is defined on ⟨e₁, …, e_n⟩ in I just in case there is at least one object e₀ ∈ D such that ⟨e₀, e₁, …, e_n⟩ ∈ ext(e). Define an I-skolemization of e to be any (total) function f : D* → D such that, for all ⟨e₁, …, e_n⟩ on which e is defined we have ⟨f(e₁, …, e_n), e₁, …, e_n⟩ ∈ ext(e).⁵

Note that (given standard ZFC set theory) every element of D has a skolemization. The object skol in our interpretation I = ⟨D, ext, skol, V⟩, then, is stipulated to be a function that maps every element e in the domain D of I to an I-skolemization of e. This mechanism enables one to use a term denoting a functional relation as both a predicate and a function symbol with the intuitively correct result. Thus, for example, in a Principia-style CL language, one could correctly assert both 'FatherOf(Adam,Cain)' and 'Gardener(FatherOf(Cain))'. This approach, of course, does have as a consequence that certain expressions that are intuitively nonsensical — e.g., 'Gardener(FatherOf(17))' — turn out to be meaningful, and even possibly true. However, this has little practical upshot, as such "unintended" truths are easily rendered innocuous by a proper formulation of one's axioms.⁶

Finally, V is a "denotation" function that assigns appropriate values to the primitive terms of L. Specifically, if τ ∈ Con ∪ OrdVar, then V(τ) ∈ D, and if τ ∈ SeqVar, then, V(τ) ∈ D*.

Denotations and Truth

Given the notion of an interpretation, we can now define what it is for a formula of a CL language to be true in an interpretation. First, we need some notation. For n-tuples s₁,..,s_n, let cnct(s₁,..,s_n) be the concatenation of s with s′.⁷ This definition is useful for defining semantic values for function terms.

Further notation will be useful in defining truth for quantified formulas (i.e., formulas in the range of ExQuant and UnivQuant). First, for χ ∈ (Var ∪ (Var × Con)), let |χ| = χ if χ ∈ Var, and if χ = ⟨ν,κ⟩ ∈ (Var × Con)), let |χ| = ν. Now let I = ⟨D, ext, skol, V⟩ be an interpretation for L. For χ₁,…,χ_n ∈ (Var ∪ (Var × Con)), say that V′ is a [χ₁,…,χ_n]-variant of V iff

V′(ν) ∈ ext(V(κ)), if χ_i = ⟨ν,κ⟩;
V′(τ) = V(τ), if τ ≠ |χ_i| for any i, 1 ≤ i ≤ n.

We then say that an interpretation I′ = ⟨D, ext, skol, V′ ⟩ for L is a [χ₁,…,χ_n]-variant of I iff V′ is a [χ₁,…,χ_n]-variant of V.

In plain but somewhat less precise English, a [χ₁,…,χ_n]-variant I′ of I is an interpretation that is just like I except that its denotation function V′ possibly assigns something else to each |χ_i|; in particular, in the case where χ_i is a pair ⟨ν,κ⟩ ∈ (Var × Con), V′ assigns a member of the extension of V(κ) to ν. This somewhat complicated definition enables the formulation of the very simple definition of truth for quantified formulas below.

So let L be a CL language for a lexicon λ, Trm the set of terms of L, and App a generator for Trm, and let I = ⟨D,ext,skol,V⟩ be an interpretation for L. Given I, the denotations of the non-primitive terms of L in I are completely determined by skol and V. This can be expressed in terms of a unique extension V^# of V such that, for any term τ ∈ Trm:

If τ ∈ Con ∪ Var, then V^#(τ) = V(τ).
If τ ∈ SeqVar, then V^##(τ) = V^#(τ), otherwise V^##(τ) = ⟨V^#(τ)⟩.
If τ = App(ε,τ₁,…,τ_n) ∈ FuncTrm, then V^#(τ) = skol(V^#(ε))(e₁,…,e_m), where ⟨e₁,…,e_m⟩ = cnct(V^##(τ₁),…,V^##(τ_n)).

The purpose of V^## is simply to enable us to form proper sequences out of the semantic values of sequences of terms, some of which denote objects in D and others of which (viz., the sequence variables) denote sequences of such objects. For example (in a Principia-style CL language again), suppose 'Moved' denotes a 3-place relation that holds between an object o and locations p₁and p₂ just in case o has moved from p₁ to p₂. Thus, in an interpretation where V('a') is o and V('@r') is the pair ⟨p₁,p₂⟩ ('@r' here being a sequence variable), we want 'Moved(a,@r)' to be true just in case the triple ⟨o,p₁,p₂⟩ ∈ ext('Moved'). We accomplish this simply by formulating the semantic clause in terms of the concatenation of sequences. But for this we need, not the object o itself, but its singleton sequence ⟨o⟩. And thus 'Moved(a,@r)' is true in our interpretation just in case cnct(V^##('a'),V^##('@r')) = cnct(⟨o⟩,⟨p₁,p₂⟩) = ⟨o,p₁,p₂⟩) ∈ ext('Moved').

Given V, we define truth for the formulas of L in our interpretation I as follows. Let φ ∈ L.

If τ = App(ε,τ₁,…,τ_n) ∈ FuncTrm and φ = Atom(τ), then φ is true in I iff cnct(V^##(τ₁),…,V^##(τ_n)) ∈ ext(V^#(ε)).
If φ = Id(τ,τ′), then φ is true in I iff V(τ) = V(τ′).
If φ = Neg(ψ), then φ is true in I iff ψ is not true in I.
If φ = Disj(ψ₁,…ψ_n), then φ is true in I iff ψ_i is true in I for some i, 1 ≤ i ≤ n.
If φ = Conj(ψ₁,…ψ_n), then φ is true in I iff ψ_i is true in I for each i, 1 ≤ i ≤ n.
If φ = Cond(ψ,ψ′), then φ is true in I iff ψ is not true in I or ψ′ is true in I.
If φ = BiCond(ψ,ψ′), then φ is true in I iff ψ and ψ′ are either both true in I or both false in I.
If φ = ExQuant(χ₁,…,χ_n,ψ), then φ is true in I iff ψ is true in some [χ₁,…,χ_n]-variant of I.
If φ = UnivQuant(χ₁,…,χ_n,ψ), then φ is true in I iff ψ is true in all [χ₁,…,χ_n]-variants of I.

Note that this semantics requires no "pruning" to serve as an appropriate semantics for first-order CL languages, as interpretations themselves involve no non-first-order entities; given an interpretation I = ⟨D,ext,skol,V⟩ the range D* of the sequence variables itself lies outside of I proper. If L is first-order, the clauses for formulas containing sequence variables simply never kick in.

The True and the False

It is convenient for many applications to introduce truth functional constants denoting truth and falsity. Given the syntax and semantics for CL above, these notions can be introduced simply as definitions. Specifically, the syntax generates both the empty conjunction Conj(∅) and the empty disjunction Disj(∅) for any given generator set. (In KIF, for example, these would correspond to the formulas '(and)' and '(or)', respectively.) On the semantics for these operators, Conj(∅) is true in all interpretations and Disj(∅) is false in all interpretations. Hence, in any given CL language, constants for truth and falsity can be introduced and defined axiomatically to be equivalent to these formulas. Thus, for example, in KIF, one might add the constants 'true' and 'false' and the axioms '(iff true (and))' and '(iff false (or))'.

KIF: A Paradigmatic CL Language

CL is in fact an outgrowth of the KIF project. CL simply abstracts away from the particularities of KIF — its choice of basic syntactic elements, its use of parenthesis, its choice of keywords, etc. A full CL language will therefore be structurally identical to a KIF language, but might differ in its surface form. Not surprisingly, then, it is rather straightforward to demonstrate that any KIF language is also a CL language. For purposes here, we will take KIF expressions to be strings.⁸. Let A be the usual set of alphanumeric characters together with the characters "-" and "_". Our first task is to specify a lexicon for a KIF language. Although the syntax for KIF is now based more generally upon unicode, for purposes here we can take the set Con of constants of a lexicon to be a set of (finite) strings over A, minus the usual KIF keywords (i.e., "forall", "exists", "not", etc.). OrdVar consists of the result of prefixing "?" to all strings over A, and SeqVar the result of prefixing "@" to those same strings. Clearly, Con, OrdVar, and SeqVar are all mutually disjoint, and the sets OrdVar and SeqVar are denumerable. Hence, Con, OrdVar, and SeqVar jointly constitute a CL lexicon. Relative to this lexicon, then, Var is the set OrdVar ∪ SeqVar and PrimTrm is the set Con ∪ Var.

Consider now the set S of strings over the set A ∪ {"?", "@", " ", "(", ")"} (" " being the space character). Define an operation App* on (S – SeqVar) × S* such that App*(t, s₁, …, s_n) = ⌈(ts₁ …s_n)⌉. ("⌈" and "⌉" here are quasi-quotes, or "Quine corners".) Let Trm be the smallest set containing PrimTrm that is closed under App*, and let App be App* restricted to Trm. App is easily seen to be a generator for Trm, and that Trm is the set of KIF function terms that is determined by the given lexicon. Let the function Atom be the identity function; thus, AtomicWff = FuncTrm in KIF.

Consider now the following operations:

Id^*(s₁,s₂) = ⌈(= s₁ s₂)⌉, for s₁,s₂ ∈ S;
Neg^*(s) = ⌈(not s)⌉, for s ∈ S;
Conj^* = ⌈(and s₁ … s_n)⌉, for s₁, …, s_n ∈ S;
Disj^* = ⌈(or s₁ … s_n)⌉, for s₁, …, s_n ∈ S;
Cond^*(s₁,s₂) = ⌈(if s₁ s₂)⌉, for s₁,s₂ ∈ S;
BiCond^*(s₁,s₂) = ⌈(iff s₁ s₂)⌉, for s₁,s₂ ∈ S;
ExQuant^*(v₁,…,v_n,s) = ⌈(exists (v*₁… v*_n)s)⌉, for v₁,…,v_n ∈ (Var ∪ (Var × Con)), s ∈ S, where v*_i is v_i if v_i ∈ Var, and v*_i is ⌈(x c)⌉, if v*_i = ⟨x,c⟩ ∈ Var × Con;
UnivQuant^*(v₁,…,v_n,s) = ⌈(forall (v*₁… v*_n)s)⌉, for v₁,…,v_n ∈ (Var ∪ (Var × Con)), s ∈ S, where v*_i is as above.

Let F be the smallest set containing AtomicWff that is closed under these operations. F is exactly the set of formulas of the KIF language determined by the given lexicon, i.e., the above operations, restricted to F, jointly constitute a generator set for F.

XML: A DTD for CL

XML provides another important framework for defining CL languages. The following simple Document Type Definition (DTD) provides a convenient XML expression of a CL language (relative to some an unspecified lexicon). The DTD's URI is http://cl.tamu.edu/docs/cl.dtd.


<!ELEMENT formula (and | or | implies | iff | not | forall | exists | atom)>

<!ELEMENT and (formula*)>

<!ELEMENT or (formula*)>

<!ELEMENT implies (formula, formula)>

<!ELEMENT iff (formula, formula)>

<!ELEMENT not (formula)>

<!ELEMENT forall (varlist, formula)>

<!ELEMENT exists (varlist, formula)>

<!ELEMENT atom ((con | var | fnterm), (con | var | fnterm | seqvar)*)>

<!ELEMENT fnterm ((con | var | fnterm), (con | var | fnterm | seqvar)+)>

<!ELEMENT varlist (var | seqvar | sortvar)*>

<!ELEMENT sortvar (var, con)>

<!ELEMENT con (#PCDATA)>

<!ELEMENT var (#PCDATA)>

<!ELEMENT seqvar (#PCDATA)>

Thus, for example, in a language satisfying this DTD, "Every boy kissed a girl" would be rendered as follows:

<formula>
  <forall>
    <varlist>
      <sortvar>
        <var>x</var>
        <con>Boy</con>
      </sortvar>
    </varlist>
    <exists>
      <varlist>
        <sortvar>
          <var>y</var>
  	  <con>Girl</con>
        </sortvar>
      </varlist>
      <atom>
        <con>Kissed</con>
        <var>x</var>
        <var>y</var>
      </atom>
    </exists>
  </forall>
</formula>

It is straightforward to show that any language defined by the above DTD is CL-conformant in the sense to be defined in the following section.

Conformance

CL languages are both syntactically anarchic (hence rather non-traditional) and quite powerful expressively. In many contexts, one might desire to use a language that is more structured, less expressive, or both — as is the case with most familiar first-order languages. If conformance with CL required one to adopt both the anarchic syntax of CL languages and its full expressive power, it is unlikely that CL would receive wide acceptance. Hence, conformance comes in two varieties: direct, for languages that fully embrace both CL's anarchic syntax and its semantic expressiveness, and indirect, for more languages that are more constrained syntactically, semantically, or both.

Direct Conformance

A given language is directly conformant with the CL standard just in case it is an instance of a CL language. Hence, as just illustrated, to demonstrate that a language L* is directly conformant, one must simply:

Specify the sets constituting the lexicon λ that underlies L* — specifically, the sets of constants, ordinary variables, and sequence variables of λ — and demonstrate that they are pairwise disjoint;
Specify the operation that serves as the generator for the set of terms of L*;
Specify the operations in the generator class for the relevant formula class for λ that we identify with L*.

Indirect Conformance

As indicated, more constrained languages can still be thought of as CL conformant in a robust, well-defined sense. Specifically, where L is a CL language, we define a subset L′ ⊆ L to be indirectly conformant relative to L just in case L′ is recursive. Hence, in general, to show that a given language L′ (simply a set of formulas, recall) is indirectly conformant, one must simply provide a recursive specification of L′ relative to some CL language L. Typically, of course, a specification of an indirectly conformant language will be provided independent of any specific CL language.

The class of interpretations for an indirectly conformant language L′ can simply be thought of as identical to the class of interpretations for its CL superlanguage L where the true-in relation is restricted to L′. However, typically, once again, it is assumed that the notion of interpretation can be defined for L′ independently of any directly conformant language.

A language will be said to be CL conformant (conformant, for short) just in case it is either a CL language or indirectly conformant relative to some CL language.

Example: The Language of Traditional FOL

The traditional language of first-order logic, relative to some choice of constants, is a prime example of an indirectly conformant language. Specifically, let L be a CL language for some lexicon λ such that SeqVar = ∅. Let p-arity and f-arity be total recursive functions from disjoint subsets Pred, Func of Con into the set of positive integers. Let τ ∈ Con. We say that τ is an n-place predicate if p-arity(τ) = n, and that τ is an n-place function symbol if f-arity(τ) = n. Otherwise we say that τ is an individual constant. Let IndCon = Con - (Pred ∪ Func) . Let Trm* be the smallest set containing IndCon and OrdVar and containing App(α,τ₁,…,τ_n) whenever α is an n-place function symbol and τ₁,…,τ_n ∈ Trm*. Let arity be p-arity ∪ f-arity. We then define the traditional first-order (TFO) sublanguage L₁ of L determined by arity to be those formulas φ of L that satisfy the following two conditions:

All of of the atomic subformulas of φ are of the form App(π,τ₁,…,τ_n), where π is an n-place predicate and each τ_i ∈ Trm*; and
If φ = ExQuant(χ₁,…,χ_n,ψ) or φ = UnivQuant(χ₁,…,χ_n,ψ) and χ_i = ⟨ν,κ⟩, then κ is a 1-place predicate of L₁.

L₁ is clearly indirectly conformant.

First-order CL and Traditional First-order Languages

In this section we clarify the relation between first-order CL (henceforth, "CL₁") languages and more traditional first-order languages. We will show that CL₁ languages and their FO counterparts are equally expressive in a well-defined sense.

Traditional First-order Languages and Their Model Theory

We will exploit the notion of a TFO sublanguage of a CL language to clarify the connection between traditional first-order logic and first-order CL. Specifically, we will clarify the connection between a CL₁ language and its TFO counterparts. There is no loss of generality here, since any first-order language can be thought of as a TFO sublanguage of some CL language.

We begin by altering our general CL semantics slightly to define a variant of traditional first-order model theory for TFO sublanguages. To motivate this alteration, note that, because we include relations in the basic logical ontology of CL, the validities of a TFO language with respect to the model theory of CL are not coextensive with the validities of that language relative to traditional model theory. For instance, the following is valid relative to CL's model theory:^8a

(=> (and (P a)
         (not (Q a)))
    (not (forall (?x ?y) 
                 (= ?x ?y))))

The reason for this is that, in CL, there is no intrinsic distinction between predicates and individual constants, and, as befits a classical model theory, all constants denote. This does not change with the introduction of the arity functions that generate a TFO language. Hence, in such languages, predicates denote objects in the domain of quantification no less than individual constants. Thus, in any CL interpretation of the sentence above, 'P' and 'Q' both denote. And since the denotation of only one has the denotation of 'a' in its extension, it follows that 'P' and 'Q' cannot denote the same thing, and hence that there cannot be only one thing in the domain. In traditional first-order model theory, however, predicates do not denote objects in the domain of an interpretation, they only have extensions over that domain. Hence, the above sentence will be false in interpretations containing a single object that is in the extension of 'P' but not 'Q'.

It is straightforward to circumscribe a subclass of CL interpretation, and a corresponding notion of truth, relative to which validity is coextensive with more traditional first-order model theory. Thus, let L be a CL language and L₁ be a traditional first-order sublanguage of L determined by arity. An interpretation I = ⟨D,ext,skol,V⟩ for L is L₁-agreeable just in case the following conditions hold (where, as usual, D = A ∪ R):

For all n-place predicates and (n-1)-place function symbols β of L₁, V(β) ∈ R and ext(V(β)) is a set of n-tuples over A. (Intuitively, this condition ensures that n-place predicates and (n-1)-place function symbols are all mapped to n-place relations that hold among individuals.)
For all n-place function symbols α of L₁, ext(V(α)) = skol(V(α))|Aⁿ, i.e., the restriction of skol(V(α)) to Aⁿ. (This condition ensures that the relation to which α is mapped is a total n-place function on individuals.)
For all κ ∈ IndCon ∪ OrdVar, V(κ) ∈ A.

It is nearly trivial to transform an L₁-agreeable CL interpretation into a more traditional first-order interpretation. The definition of what it is for a formula φ of L₁ to be true₁ in an L₁-agreeable interpretation I = ⟨D,ext,skol,V⟩ of L is identical with the definition of truth in I except for the quantificational clauses, which differ slightly. Specifically, say that a [χ₁,…,χ_n]-variant V′ of V is L₁-agreeable iff V′(χ_i) ∈ A whenever χ_i is a variable.⁹ Then:

If φ = ExQuant(χ₁,…,χ_n,ψ), then φ is true₁ in I iff ψ is true in some L₁-agreeable [χ₁,…,χ_n]-variant of I.
If φ = UnivQuant(χ₁,…,χ_n,ψ), then φ is true₁ in I iff ψ is true in all L₁-agreeable [χ₁,…,χ_n]-variants of I.

φ is valid₁ iff it is true₁ in all L₁-agreeable interpretations. It is easy to see that the valid₁ formulas of L₁ are exactly the traditional first-order validities. Notably, our CL-valid formula above is obviously not true in an L₁-agreeable interpretation I in which V('a') is the only object in the set A of individuals of the domain D of I.

Intepreting TFO Sublanguages in CL₁

In this section we show that TFO languages are interpretable in CL in two very natural senses, one interpretation-relative and the other interpretation-independent.

Interpretability I: Interpretability Relative to an Interepretation

The first notion of interpretability plays off the fact that, relative to an L₁-agreeable interpretation, the definition of truth₁ differs from the definition of truth only in the range of the quantifiers. This suggests the following set of definitions.

Let L be a CL₁ language – for definiteness, let us assume KIF syntax – and let L₁ be the TFO sublanguage of L generated by an arity function arity. Let L⁺ be the result of adding a single predicate 'Ind' to L. For any L₁-agreeable interpretation I = ⟨D,ext,skol,V⟩ for L (where, as usual, D = A ∪ R), let I⁺ = ⟨D⁺,ext⁺,skol⁺,V⁺⟩ be any interepretation such that

D⁺ = A ∪ R⁺, where R⁺ is the result of adding a single element Ind to R;
ext ⊆ ext⁺ and ext⁺(ind) = A;
skol ⊆ skol⁺;
V⁺(Ind) = Ind.

Now define a simple mapping + from the sentences of L₁ into those of L⁺ as follows:

φ⁺ = φ, for atomic formulas φ;
(not φ)⁺ = (not φ⁺);
(and φ ψ)⁺ = (and φ⁺ ψ⁺); similarly for the remaining boolean operators;
(exists (v₁…v_n) φ)⁺ = (exists (v₁*…v_n*) φ⁺)), where v_i* is ⌈(v_i Ind)⌉ if v_i is a variable, and v_i* is v_i otherwise (i.e., if v_i is a variable/constant pair ⌈(xc)⌉);
(forall (v₁…v_n) φ)⁺ = (forall (v₁*…v_n*) φ⁺)), where v_i* is as above.

So, for example, let φ be the sentence

(forall (?x (?d Direction) (?t1 Time) (?t3 Time))
        (if (and (moving-in ?x ?d ?t1)
                 (not (exists (?y (?t2 Time))
	                      (and (between ?t2 ?t1 ?t3)
                                   (acts-on ?y ?x ?t2)))))
            (moving-in ?x ?d ?t3)))

expressing the proposition that if an object is moving in a certain direction at a given time t₁ then it is still moving in that direction at a later time t₃ if nothing acts upon it at any intervening time. Then φ⁺ is

(forall ((?x Ind) (?d Direction) (?t1 Time) (?t3 Time))
        (if (and (moving-in ?x ?d ?t1)
                 (not (exists ((?y Ind) (?t2 Time))
	                      (and (between ?t2 ?t1 ?t3)
                                   (acts-on ?y ?x ?t2)))))
            (moving-in ?x ?d ?t3)))

Given our two + functions we have the following simple theorem: Let I be any L₁-agreeable interpretation for L. Then for any L₁ sentence φ, φ is true₁ in I iff φ⁺ is true in I⁺. The proof is a simple induction on the formulas of L₁.

Interpretability II: TFO Languages as CL₁ Theories

The function arity that generates a TFO sublanguage L₁ of a CL₁ language L separates the syntactically undifferentiated constants of L into n-place predicates, n-place function symbols, and individual constants. This partitioning of the constants explicitly reflects the intuitive, but typed, ontology of traditional first-order logic that is expressed in its semantics – relations (including functions) and individuals. CL₁ basically shares the same ontology, albeit untyped: relations are first-class logical citizens. We can therefore make the implict ontology of TFO languages in L despite its undifferentiated constants simply by extending L to a new language L⁺⁺ by introducing appropriate new constants and interpreting them in a way that parallels the semantics of traditional first-order logic. And we can capture its typed character by suitably restricting the quantifiers, as in the first notion of interpretability. Moreover, we can axiomatize this ontology explicitly as a theory of L⁺⁺. Specifically, we show that, for any TFO sublanguage L₁ of a CL₁ language L, there is a theory in a "natural" extension L⁺⁺ of L whose models are exactly (slightly modified versions of) the class of L₁-agreeable interpretations.

[Details forthcoming…]

Intepreting CL₁ Languages as TFO Theories

In logic, as in life generally, turnabout is fair play. Just as we can "translate" any given TFO language into a CL₁ theory, so we can translate any CL₁ language into a theory in a TFO language.

[Details forthcoming…]

Notes

1. If SeqVar is empty, then languages built on λ will be first-order. We allow SeqVar to be empty to allow to allow first-order languages to be fully conformant without embracing sequence variables.

2. T is a smallest such class just in case it satisfies the conditions in question but is not a proper superclass of any other class satisfying those conditions.

3. Where Range(App) = { τ ∈ Trm : for some x, App(x) = τ}.

4. Suppose φ ∈ Fla has an infinite decomposition. Then Fla – {φ} still satisfies the conditions above, as closure under the operations in the generator set only requires finite compositions of those operations applied to the base sets. But then Fla is not a smallest class of the relevant sort, contrary to its definition. This will be important for the semantics of CL languages below.

5. We identify the first rather than the last element of an n-tuple in the extension of a function with the value of the function, as this increases the usability of an important sublanguage of any CL langage. This will be discussed below.

6. Note that, on this semantics, '(∃x)F(x,y)' entails, but is not entailed by, '(∃x)x = F(y)' (indeed, as in classical first-order logic, the latter is a logical truth of our semantics). Hence, perhaps somewhat paradoxically at first sight, from the fact that something is identical to the FatherOf 17, it doesn't follow that 17 has a father. Note, however, that this is going to be an issue for any language that

Includes a classical quantification theory;
Includes in its intended domain objects of vastly different ontological categories; and
Contains terms that intuitively express functions which only sensibly apply to the objects of some ontological categories but not others.

7. More exactly, where s = ⟨e₁,…,e_n⟩ and s′ = ⟨e_n+1,…,e_n+m⟩, cnct(s,s′) = ⟨s₁,…,s_n+m⟩.

8. It is perhaps most natural to take the expressions of KIF to be strings, but other construals (e.g., sequences) are of course possible.

8a. This fine example is due to Ian Horrocks.

9. We only need to consider this case because when χ_i = ⟨ν,κ⟩ we are already guaranteed by the definitions of a [χ₁,…,χ_n]-variant and an L₁-agreeable interpretation that V′(ν) ∈ A.