Abstract Syntax and Semantics for SCL

Common Logic Working Group

Version 1.1 (Changelog)

SCL Syntax

SCL provides an abstract syntax that can be realized in infinitely many distinct forms, infinitely many "concrete" syntaxes. Each syntax will consist in a stock of initial lexical elements and a grammar that specifies the classes of terms and formulas built upon those elements. Languages will be identified with the formulas generated by a given grammar from a given lexicon. SCL provides the structural constraints that must be met by any language so generated to be considered conformant.

Lexicons

An SCL language is based upon an initial stock of primitive syntactic entities. Specifically, an SCL lexicon λ will consist of the following sets:

If SeqVar is empty, then λ is known as a first-order lexicon.

Con = PredConIndCon is known as the set of constants of λ. Var = GenVarSeqVar is known as the set of variables of λ. GenVar and SeqVar shall be disjoint, and Var shall be disjoint from ConFnSym. Let PrimTrm = IndConGenVar. PrimTrm is known as the set of primitive terms of λ. λ is a lexicon with identity if it also contains a distinguished predicate Id.

Lexicons λ also come with a function arity that maps each predicate constant and function symbol into the set N ∪ {ω}, where N is the set of natural numbers and ω is any object not in N. For predicates π, arity will indicate the number of arguments π will take. (This will of course be expressed explicitly in the grammar below.) If arity(π) = nN, then π is said to be an n-place predicate; otherwise π is variably polyadic. Variably polyadic predicates will be able to take any number of arguments. We let PredConn be the set of n-place predicates, and PredConω the set of variably polyadic predicates. Because we will interpret function symbols as functional relations, we will let the arity of a function symbol correspond to the arity of the relation it denotes rather than to the number of arguments it takes. This will also enable the predicates of an SCL lexicon to do double duty as function symbols — note that there is no requirement that PredCon and FnSym be disjoint — without requiring a separate arity function for function symbols. Accordingly, for function symbols α, if arity(α) = n+1, we say that α is an n-place function symbol; otherwise α is variably polyadic. We stipulate that arity(α) ≠ 0, for any function symbol α. We let FnSymn be the set of n-place function symbols, and FnSymω the set of variably polyadic function symbols.

Over and above presence of sequence variables, SCL lexicons differ from traditional first-order lexicons in two particularly important ways. First, SCL generalizes the notion of arity by allowing variably polyadic predicate constants and function symbols, i.e., predicate constants and function symbols that can take arbitrarily many arguments. Variably polyadicity is especially useful and appropriate in SCL languages containing sequence variables.

Second, it is not required that PredCon, IndCon, and FnSym be pairwise disjoint. This reflects SCL's goal of generality. Many knowledge representation languages are "type-free" to one extent or another; that is, they treat properties, propositions, classes, functions, and other so-called "higher-order" entities as "first-class citizens" in their own right, capable of being referred to and quantified over along with individuals. Natural language itself reflects this "dual role" that properties and their ilk can play in the gerundive construction, whereby verb phrases expressing properties and relations — e.g., is a linguist — are transformed into noun phrases — being a linguist. By allowing predicate constants and function sybols simultaneously to serve as individual constants, and by allowing variables to serve as predicable terms, SCL provides a formal correlate to these constructions and thereby provides a rigorous framework in which this common knowledge representation construction is fully sanctioned.

It is useful explicitly to pick out several important limiting cases of SCL languages that are determined by minimally or maximally tweaking arity and the degree of overlap among constants and function symbols. Specifically, say that an SCL lexicon λ is fully typed if (PredConFnSym) ∩ IndCon = ∅; arity-fixed if, for all predicate constants and function symbols κ, arity(κ) = n, for some nN; and traditional first-order (TFO) if λ is both fully-typed and arity-fixed. By contrast, say that λ is arity-free if, for all predicate constants and function symbols κ, arity(κ) = ω; type-free if PredConFnSymIndCon; and unconstrained if λ is both arity-free and type-free. In between the extremes of TFO and unconstrained lexicons, of course, lie a number of interesting intermediate possibilities.

Grammars

Terms

Given an SCL lexicon λ, we define the notion of a term class based on λ. Intuitively, a term is either a primitive term (constant or variable) or the result of "applying" a function symbol to some nonempty sequence of terms. Because we are defining an abstract syntax, we do not want to specify the exact form that the application of a function symbol to its arguments should take. Hence, we simply specify the general constraints than any syntax of application must satisfy; we do this in terms of a certain type of syntactic function.

As groundwork for this definition, for any set M, let Mω be the set of finite sequences of elements of M, i.e., Mω = nNMn, where Mn is the set of all n-tuples of elements of M. Given this, say that T is a term class for λ if T contains all of the primitive terms of λ and is the smallest class1 closed under a one-to-one operation App — called a term generator for λ — such that

App : nN(FnSymn × Tn) ∪ (FnSymω × (Tω ∪ (Tω × SeqVar))) → T.

That is, for τ1,…,τnT, if α is an n-place function symbol, then App(α,τ1,…,τn) ∈ T, and if α is a variably polyadic functional, then in addition for any sequence variable σ, App(α,τ1,…,τn,σ) ∈ T;

We say that App generates the corresponding term class T. For any term generator App for λ, let FnTrm = Range(App),2 . FnTrm is the set of function terms of λ (relative to App).

So, for example, if a and b were among the constants of a lexicon λ and f and g among its function symbols, then any of the following might among the function terms produced by different generators: f(a,g(b),s), (f a (g b) s), s[bg]af (somewhat perversely), and even

<term>
  <fnsym>f</fnsym>
  <indcon>a</indcon>
  <term>
    <fnsym>g</fnsym>
    <indcon>b</indcon>
  </term>
  <seqvar>s</seqvar>
</term>
      

This example illustrates the use of a sequence variable — note that such variables can only occur in a single distinguished position (typically, "tail" position) in a function term.

Type-Freedom and Predicability

As hinted at above, and as will be spelled out in more detail in the model theory below, one of the important features of SCL is that it allows for a "type-free" semantics in which properties and relations are treated as first-class individuals. Languages with such a semantics will there be allowed to refer to and quantify over such "reified" entities directly. In particular, it is important to allow such languages to quantify over them in their predicative roles. Syntactically speaking, this means that we must allow variables to occur in predicate position in atomic formulas.

However, because it is important that SCL encompass more traditional first-order languages as well, type-freedom should be optional. Accordingly, whether or not variables (and other expressions, more generally) can occur in predicative position along with predicate constants will be specified in the grammar for a language, rather than being predetermined by the chosen lexicon. Consequently, we define the set Predn of n-place predicables to be either simply the set PredConnPredω (since variably polyadic predicates be predicated of any finite number of arguments — hence, in particular of n) or the set PredConnPredωGenVar. A similar generalization that allows variables to occur in function position in complex terms adds a certain elegance and convenience at the cost of a great deal of semantic complexity, but the gains are minimal for the purposes envisioned for SCL.0.

Formulas

In light of the above, we now do for formulas what we did for terms. Let λ be an SCL lexicon, and let Trm be the term class for λ generated by some term generator App. First, we need a class of basic formulas. Let Holds be a one-to-one function on

nN(Predn × Tn) ∪ (Predω × (Tω ∪ (Tω × SeqVar))).

That is, given an n-place predicable and n terms, or a variably polyadic predicable, n terms and a sequence variable, Holds returns a unique formula. Any such function Holds is said to be a predication operation for λ based on App. As with term generators, the outputs of different predication functions might take very different forms. The only constraint is that distinct inputs always yield distinct outputs.3 Given a term generator, the range of a predication operation Holds for λ is said to be the class of atomic formulas for λ generated by Holds.

Let AtFla be the class of atomic formulas for λ based on a predication operator Holds. Say that F is a formula class for λ, relative to Holds, if it is the smallest class that includes At and is closed under a set Op — known as a formula generator for λ based on Holds — of operations Id, Neg, Conj, Disj, Cond, Bicond, ExQuant, UnivQuant that satisfy the following conditions:

If λ is a lexicon with identity, then in addition Op contains an operation

Let Fla be range of the operations in Op. We say that Fla is the formula class generated by Op.

As with terms, depending on one's choice of term generator, predication operation, and generator set, SCL languages can come in many different concrete forms. So, for example, the standard, first-order "logical form" of 'Every boy kissed a girl' in terms of our abstract syntax is

UnivQuant1,Cond(Holds11),ExQuant2,Conj(Holds22),Holds312))))),

where π1, π2, and π3, are "slots" for the predicates constants of the appropriate arity chosen from any particular lexicon to represent boyhood, girlhood, and kissing, and ν1 and ν2 represent some choice of variables. In one SCL language, this form might be realized by its familiar introductory text-book form:

(∀x)(Boy(x) → (∃y)(Girl(y) & Kissed(x,y)))

A conceptual graph interchange form (CGIF) implementation has a rather different appearance:

[@every*x] [If: (Boy ?x) [Then: [*y] (Girl ?y) (Kissed ?x ?y) ]]

As does a KIF-like implementation:

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

And an XML-ish implementation might take another very different form still:

<formula>
  <forall>
    <var>x</var>
    <formula>
      <implies>
        <formula>
          <atom>
            <con>Boy</con>
            <var>x</var>
          </atom>
        </formula>
        <formula>
          <exists>
            <var>y</var>
            <formula>
              <and>
                <formula>
                  <atom>
                    <con>Girl</con>
                    <var>x</var>
                  </atom>
                </formula>
                <formula>
                  <atom>
                    <con>Kissed</con>
                    <var>x</var>
                    <var>y</var>
                  </atom>
                </formula>
              </and>
            </formula>
          </exists>
        </formula>
      </implies>
   </forall>
</formula>
    

Note also that the clauses for quantified formulas above, i.e., those entities in the ranges of ExQuant and UnivQuant, allow for the use of restricted quantifiers. Thus, the logical form of "Every boy kissed a girl" using such quantifiers, implementated in our standard textbook form might be:

(∀x:Boy)(∃y:Girl)Kissed(x,y)

An in CGIF and KIF-like implementations:

[Boy: @every*x] [Girl: *y] (Kissed ?x ?y)
(forall ((?x Boy))
        (exists ((?y Girl))
                (Kissed ?x ?y)))
    

The advantages of restricted quantifiers for readability are apparent.

It is important to observe 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. 4 Let φ ∈ Fla. An object ε in the decomposition of φ is an atom of φ just in case ε is element of the lexicon λ. ψ is a subformula of φ if ψ ∈ Fla and ψ is in the decomposition of φ.

Hand in glove with the capacity to treat predicates as individual constants, as noted, is the ability of suitably defined SCL languages to have quantified variables occur in predicate position. The motivation is clear: since properties and relations can be treated as individuals, it should be possible to talk about them in general. This, of course, we can do in a basic way simply in virtue of their occurring as individuals in the domain of quantification. However, what we want to say about them might concern their predicative roles. Hence, we want to allow the variables that range over them to be able to occur in predicate position in atomic formulas as well. Similar remarks apply to functions.

As a simple example, one can axiomatize the property of symmetry for 2-place relations generally in the obvious way:

(forall (?x ?y ?F)
        (implies (Symmetric ?F)
                 (implies (?F ?x ?y)
                          (?F ?y ?x))))
      

Languages

Let App be a term generator for λ, where Trm is the set generated by App, and let Holds be based upon App. Let Op be a formula generator for λ based on Holds, and let L be the formula class generated by Op. We define any such set L to be an SCL language for the SCL lexicon λ, and we say that λ underlies L. Trm is said to be the set of terms of L. If λ and λ′ are SCL lexicons with the same sets of constants and function symbols, and L and L′ are SCL languages for λ and λ′, respectively, then L and L′ are said to be equivalent. If λ is a first-order lexicon, then a language for λ is said to be a first-order SCL language, or an SCL

KIF: A Paradigmatic SCL Language

The CL project, of which SCL is a part, is an outgrowth of the KIF project. CL for the most part 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 an SCL language. SCL abstracts from a somewhat simpler version of KIF known as SKIF (Hayes and Menzel, 2001). We will demonstrate that SKIF is an instance of an SCL language in this section.

For purposes here, we will take SKIF 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 SKIF language. Although the syntax for SKIF is now based more generally upon unicode, for purposes here we can take the sets PredCon, IndCon, and FnSym of a SKIF lexicon to be a set of (finite) strings over A, minus the usual SKIF keywords (i.e., "forall", "exists", "not", etc.). GenVar consists of the result of prefixing "?" to all strings over A, and SeqVar the result of prefixing "@" to those same strings. Clearly, these sets meet the disjointness requirements on SCL lexicons. Relative to this lexicon, then, Var is the set GenVarSeqVar, PrimTrm is the set ConGenVar, and PredTrm is the set PredConGenVar. arity for SKIF is the constant function ω (i.e., all predicate constants and function symbols are variably polyadic).

Consider now the set S of strings over the set A ∪ {"?", " ", "(", ")"} (" " being the space character). Define an operation App* on FnSym × (S* ∪ (S* × SeqVar)) such that App*(t, s1, …, sn) = ⌈(t s1 sn)⌉. ("⌈" 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 FnSym × (Trm* ∪ (Trm* × SeqVar)). It is easy to see that App is a generator for Trm and that Trm is the set of SKIF function terms that is determined by the given lexicon. Given Trm, we define the operation Holds on PredTrm × (Trm* ∪ (Trm* × SeqVar)) such that Holds*(π, τ1, …, τn) = ⌈(π τ1 τn)⌉. Let AtFla be the atomic formulas for our given lexicon, i.e., the range of Holds.

Consider now the following operations:

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

A XML DTD for SCL

XML provides another important framework for defining SCL languages. The following simple Document Type Definition (DTD) provides a convenient XML expression of an SCL language relative to some an unspecified lexicon that includes sequence variables. For simplicity's sake, we also assume that the lexicon is fully-typed and arity-free. The DTD's URI is http://cl.tamu.edu/docs/scl/scl-latest.dtd. This DTD validates the XML rendering of "Every boy kissed a girl" above.


<!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 varlist (genvar | sortvar)+>

<!ELEMENT sortvar (genvar, predcon)>

<!ELEMENT atom (pred, (indcon | genvar | fnterm)*, seqvar{0,1})>

<!ELEMENT fnterm (fnsym, (indcon | genvar | fnterm)*, seqvar{0,1})>

<!ELEMENT pred (predcon | genvar) (#PCDATA)>

<!ELEMENT indcon (#PCDATA)>

<!ELEMENT predcon (#PCDATA)>

<!ELEMENT fnsym (#PCDATA)>

<!ELEMENT genvar (#PCDATA)>

<!ELEMENT seqvar (#PCDATA)>
    

SCL Semantics

Interpretations

Let λ be an SCL lexicon. An SCL interpretation I for λ is a 4-tuple ⟨I,R,ext,V⟩ satisfying the following conditions. First, I and R are nonempty sets. Intuitively, I represents the set of individuals of I, and will serve as the range of the quantifiers and its members will serve as the denotations of terms. R is the set of relations5 whose members are the denotations of predicate constants. To allow for type-freedom, there is no requirement that I and R be disjoint; indeed any degree of overlap, from partial to complete, is allowed. Those relations that are also members of I are said to be reified. Intuitively, reified relations are relations that can also be thought of as individuals. Accordingly, they can also be the values of individual constants and individual variables.

R is itself the union of countable sets Rω, R1, R2, R3, …. All are possibly empty with the exception of R2, which contains a distinguished element Id, intended to serve as the identity relation. Intuitively, Rω is the set of variably polyadic relations, and each Rn the set of n-place relations. Accordingly, ext is a corresponding extension function from R into ℘(Iω) subject to the constraint that, for any natural number n > 0, if rRn, then ext(r) ⊆ In; in particular, ext(Id) = {⟨a,a⟩ : aI}.

Intuitively, of course ext(r) represents the extension of r. For elements r of Rω , if ext(r) is a total (extensional) function on Iω,6 then we say that r is a function on Iω. For n+1-place relations, r, if ext(r) is a total (extensional) function on In,6 then we also say that r is a function on In, or an n-place function.

Finally, V is a "denotation" function that assigns appropriate values to the constants and function symbols of L. Specifically,

Note, importantly, that it is not required that I and R be disjoint. This is the semantic correlate of the type-freedom permitted (though not required) in SCL languages. Specifically, an SCL language L can allow a primitive term κ to do double duty as both a predicate constant and an individual constant. Consequently, the denotation function V in any interpretation I of L must by definition map κ, qua predicate constant, to an element of R; it must also map κ, qua individual constant, qua individual constant, to an element of I. Consequently, to satisfy these constraints, I, V(κ) will have to be in both I and R, i.e., it will have to be both a relation and an individual. And this is just what the semantics allows. In a similar fashion, predicate constants can do double duty as function symbols.

Denotations and Truth

Given the notion of an interpretation for a lexicon λ, we can now define what it is for a formula of an SCL language L based on λ to be true in an interpretation.

Some additional apparatus will be useful in defining truth for quantified formulas (i.e., formulas in the range of ExQuant and UnivQuant). First, given an interpretation I, define a variable assignment for I to be a function that maps individual variables into I and sequence variables into Iω. To define the semantics of quantification, what we need is the notion of a variable assignment v′ that is exactly like a given assignment v except that it might not agree with v on what to assign to some finite set of individual variables. The idea is straightforward, but the presence of restricted quantifiers forces us to proceed with some care. Let I = ⟨I, R, ext, V⟩ be an interpretation for L, and let v be a variable assignment for I. In our syntax, a quantifier can bind an entire sequence consisting of (individual) variables and variable/predicate pairs. So let χ1, …, χn be such a sequence, and say that a variable assignment v′ for I is a [χ1,…,χn]-variant of v iff

So let L be an SCL language for a lexicon λ, where App generates the set Trm of terms of L, and let I = ⟨I,R,ext,V⟩ be an interpretation for L. Given I and a variable assignment v, let Vv be the union of V and v. Given I and a variable assignment v, the denotations of the function terms of L in I are completely determined by Vv. This can be expressed in terms of a unique extension Vv# of V such that, for any term τ ∈ Trm:

Given V, we define satisfaction for the formulas of L by a variable assignment v for our interpretation I as follows. Let φ ∈ L:

If λ is a lexicon with identity, then:

Finally, then, a formula φ is true in I iff every variable assignment for I satisfies φ.

Note that, on this semantics, free individual variables are implicitly universally quantified; that is, if φ is a formula containing a free individual variable ν, then φ is true in I iff UnivQuant(ν,φ) is true in I. We do not have a similar metatheorem for formulas with free sequence variables because sequence variables are not explicitly quantified. It should be clear, however, that the above definition of truth treats free sequence variables as if they were universally quantified as well: a formula φ containing a free sequence variable σ will be true in an interpretation I iff every variable assignment v satisfies φ, and hence iff every [σ]-variant of every variable assignment satisfies φ.

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 SCL 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 SCL 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))'.

Conformance

SCL is rather less constrained than traditional logical logical languages and it is expressively quite powerful. In many contexts, especially the constructions of ontologies, a language is used that is more structured, less expressive, or both — as is the case with most familiar first-order languages. If conformance with SCL required adoption of all of its features, it is unlikely that it would see wide adoption. Hence, conformance comes in two varieties: direct, for languages that fully embrace both SCL's unconstrained 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 SCL standard just in case it is an instance of an SCL language. Hence, as just illustrated, to demonstrate that a language L* is directly conformant, one must simply:

  1. 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;
  2. Specify the operation that serves as the generator for the set of terms of L*;
  3. 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.

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

SCL and First-order Logic

It is easy to demonstrate that the presence of sequence variables pushes SCL beyond the power of first-order logic. For example, let 's' be a sequence variable and 'P' a variably polyadic predicate constant; then every finite subset of the the following set is satisfiable, but the set itself is not:

{(∃s)~Ps, P, (∀x1)Px1, (∀x1x2)Px1x2, …}

Hence, the compactness property fails for full SCL. However, despite its nontraditional extended features --- notably, the ability to quantify over so-called "higher-order" objects like properties and relations, SCL without sequence variables — call this "SCL1" — is fully first-order. Notably, it is easy to prove that SCL1 has both the compactness property and the downward Löwenheim-Skolem property, the two defining properties of first-order logic, by Lindstrom's famous theorem [REF]. Nonetheless, other features permitted in SCL1 languages — variables occurring in predicate position in atomic formulas and in function position in complex terms, predicates and function symbols serving simultaneous as arguments to other predicates and function symbols — lead to logical forms that are unfamiliar in traditional first-order (TFO) languages. It is important, therefore, to explore the connections between SCL1 and TFO languages.

Traditional First-order Languages

We first note that TFO languages can be defined in a way that shows them to be indirectly SCL conformant. Specifically, let L be an SCL language for some lexicon λ such that

L1 is clearly indirectly conformant.

It is straightforward to circumscribe a subclass of SCL interpretations for the lexicon λ, and a corresponding notion of truth — viz., "truth1" — for TFO languages based on λ, relative to which validity is coextensive with more traditional first-order model theory. Let L be an SCL1 language based on λ and L1 be the traditional first-order sublanguage of L determined by an arity function arity for λ. An interpretation I = ⟨I,R, ext, V⟩ for λ is TFO-agreeable relative to arity just in case the following conditions hold (henceforth reference to arity will be suppressed when it can be determined from the context):

Let L1 be a TFO sublanguage of L determined by arity, and let I = ⟨I,R,ext,V⟩ be a TFO-agreeable interpretation of λ. The definition of what it is for a formula φ of L1 to be true1 in I is identical to the definition of truth in I except for the quantificational clauses, which have to be restricted to TFO-agreeable interpretations; specifically:

φ is valid1 iff it is true1 in all TFO-agreeable interpretations of λ.

It is utterly trivial to transform a TFO-agreeable interpretation I into a structurally similar, more traditional "Tarskian" first-order interpretation I* of L1 (call this the Tarski correlate of I). We simply replace V and ext with their composition Vext, thereby mapping individual constants to elements of I and predicate constants and function symbols directly to extensions. More exactly, where I = ⟨I,R, ext, V⟩ is an L1-agreeable interpretation, let I* = ⟨I,V*⟩, where V*(κ) = V(κ) for individual constants κ and V*(β) = ext(V)(β), for predicate constants and function symbols β. It is easy to see that a formula is true1 in a TFO-agreeable interpretation I iff it is true in its Tarski correlate.

It is nearly as trivial to transform a Tarskian interpretation I* = ⟨I,V*⟩ of L1 into a structurally similar L1-agreeable interpretation I = ⟨I,R, ext, V⟩, where:

Once again, it is obvious that a sentence of L1 is true in a Tarskian interpretation I* iff it is true in its L1-agreeable counterpart. Hence, the valid1 formulas of L1 are exactly the traditional first-order validities of L1. That is to say, the logical properties of a TFO language are identical regardless of whether one interprets the language according to SCL's model theory for TFO languages or traditional Tarskian model theory.

Translating from an SCL1 Language into a TFO Language

As noted, SCL1 languages — SCL languages without sequence variables — are fully first-order. The easiest way to demonstrate this is to define a simple translation scheme from an arbitrary SCL1 language and a TFO language. Because of SCL's flexibility, the general translation scheme is rather involved. After defining the general scheme we will look at an important special case.

So L be an arbitrary SCL1 language based on a given lexicon λ whose corresponding arity function is arity. We let PredCon, IndCon, FnSym, and GenVar be the stock of primitive lexical items of λ. We begin by defining the notion of a fully typed correlate λ* of λ. The idea here, first, is to purge λ of its type-free elements, viz., those predicate constants and function symbols that double as individual constants. To accomplish this, we first separate off the "pure" predicates of λ, those that are not also individual constants. So let PurePred = PredConIndCon. (Recall that pure predicates, unlike predicates that double as individual constants, do not denote anything in the domain of the quantifiers. Hence, their status as predicates in λ needs to be maintained under any translation scheme if the translation is to be meaning-preserving.) Let PurePredn be the set of n-place pure predicates and PurePredω be the set of variably polyadic pure predicates. Let ImpPredn (the set of "impure" n-place predicates) be PredConn - PurePredn, and let ImpPredω be PredConω - PurePredω.

For variably polyadic predicates π ∈ PurePredω, for every natural number n, let πn be a unique new predicate. The idea here is that, since there are no variably polyadic predicates in a TFO language, we must translate occurrences of such a predicate π in L in terms of fixed-arity predicates πn that capture the meaning of π in contexts in which it is predicated of n arguments. Let PurePredω* be {πn : π ∈ PurePredω, n > 0}. (Note that, in practice, this is no genuine complication, as, in a concrete language, one can use the same character for all the predicates predicates πn.)

Next we need a mechanism for translating impure, or "dual-role", predicates that indicate relations that are also individuals. Let Holds be a set of countably many new predicates 'Holds1', 'Holds2', … . The idea is this. Let π be an impure n-place predicate of λ. π itself will take on the role of an individual constant in λ. But beecause that can be its only role in the TFO lexicon λ*, ⌈Holdsn⌉ will be evoked to capture the predicative qualities it can display qua predicate in λ. Thus, intuitively, ⌈Holdsn⌉ will be true of π, τ1, …, τn in any language based on λ* if and only if π is true of τ1, …, τn in L. (We will make this more precise model theoretically below.)

In general, we only want as many ⌈Holdsn⌉ predicates to be in λ* are are needed to translate the formulas of any languages based on λ. How many we need is determined by the impure predicates of λ, as pure n-place predicates can be imported directly into λ*, and pure variably polyadic predicates will be replaced by fixed-arity surrogates, one for each natural number n. Specifically, if there any impure variably polyadic predicates in λ, then we will need all of Holds, as such predicates can take any finite number of arguments languages based on λ. If there are no such predicates in λ, then we put ⌈Holdsn⌉ in λ* if and only if there is at least one impure n-place predicate in λ. More exactly: we let Holds* be Holds if ImpPredω ≠ ∅; otherwise let Holds* be {⌈Holdsn⌉ : ImpPredn ≠ ∅}. Letting arity* be the arity function for λ*, we stipulate that arity*(⌈Holdsn⌉) = n+1, for all n, as we wish the index of ⌈Holdsn⌉ to indicate the arity of the "objectified" constants ⌈πn⌉ that can occur as its first argument.

We need a similar treatment for functions symbols. We first purge the type-free elements. So let PureFn = FnSymIndCon, and let PureFnn be the set of n-place pure function symbols and PureFnω be the set of variably polyadic pure predicates. Let ImpFnn (the set of "impure" n-place function symbols) be FnSymn - PureFnn, and let ImpFnω be FnSymω - PureFnω.

For variably polyadic function symbols α ∈ PureFnω, for every natural number n, let αn be a unique new function symbol. As with predicates, since there are no variably polyadic function symbols in a TFO language, we must translate occurrences of such a function symbol α in L in terms of fixed-arity function symbols αn that capture the meaning of α in contexts in which it is predicated of n arguments. Let PureFnω* be {αn : α ∈ PureFnω, n > 0}.

Next, to deal with impure function symbols, let App be a set of countably many new function symbols 'App1', 'App2', …. The idea here is again analogous to predicates. Let α be an impure n-place function symbol of λ. α itself will take on the role of an individual constant in λ. Since that can be its only role in the TFO lexicon λ*, ⌈Appn⌉ will be evoked to capture applicative qualities it can display qua function symbol in λ . Thus, intuitively, ⌈Appn⌉ applied to α, τ1, …, τn in any language based on λ* will denote exactly what is denoted by α applied to τ1, …, τn in L.

As with predicates, if there any impure variably polyadic function symbols in λ, then we will need all of App. If there are no such function symbols in λ, then we put ⌈Appn⌉ in λ* if and only if there is at least one impure n-place function symbol in λ. More exactly: we let App* be App if ImpFnω ≠ ∅; otherwise let App* be {⌈Appn⌉ : ImpFnn ≠ ∅}. We stipulate that arity*(⌈Appn⌉) = n+1, for all n. (Recall that, to allow predicates denoting functional relations also to occur as function symbols, the arity of a function symbol is 1 + the number of arguments it takes it. We want the index of ⌈Appn⌉ to reflect the arity of the "objectified" function symbols ⌈αn⌉ that can occur as its first argument.)

To summarize, then, our fully-typed correlate λ* consists of the following sets:

Since PredCon*, IndCon*, and FnSym* are pairwise disjoint, λ* determines a class of equivalent SCL1 languages. Let L* be one of these languages. Let App, Holds, Id, … be L's term generator, predication operator, and formula generator, and let App*, Holds*, Id*, … be those of L*.

Our translation scheme from L into L*1 runs as follows. First, for terms τ of L:

Now let φ ∈ L:

Recall that the general form of quantified formulas allows for restricted quantifiers; in the existentially quantified case, ExQuant1,…,χn,ψ), where the χi are either single individual variables or pairs of the form ⟨ν,κ⟩, where ν is an individual variable and κ is a predicate. In the latter case we need to distinguish between the cases where κ is a 1-place or variably polyadic predicate only and those where κ is also an individual constant. Thus, for a sequence χ1,…,χn of the relevant sort, let ξ1,…,ξi be those members of the sequence, in order, that are either single individual variables νi or pairs ⟨ν,π⟩ where π ∈ PurePred. In the latter case, let ξi* be ⟨ν,π*⟩, where π* is just π if π is a 1-place predicate and is its 1-place λ*-correlate π1 if π is variably polyadic. The remaining elements of χ1,…,χn are all variable / predicate constant pairs ⟨μ11⟩, …, ⟨μjj⟩ where κi is an impure predicate of λ, and hence an individual constant in λ*. Our translation then continues as follows:

To illustrate, consider a KIF-like language L containing an individual constants 'a' and 'b', function symbols 'f' and 'g', , and predicates 'foo', 'bar', and 'baz'. Suppose also 'f' and 'foo' have also been designated individual constants. We suppose 'f1', 'f2', … are the n-place function symbols corresponding to 'f' in λ*; similarly for 'foo'. We suppose the grammar of L* be similar in form to L to simplify the example. Then the following would be example translations according to the above scheme:


(g a (f a b))* = (g2 a (App2 f a b))

(foo (g a) b (g f (f a)))* = (Holds3 foo (g1 a) b (g2 f (App1 f a)))

(forall (?x (?y foo) (?u foo))
        (exists (?z (?w bar))
                (and (baz ?x (f (g ?y)))
                     (not (foo ?x ?z (g (f ?x ?w)))))))* =
  (forall (?x)
          (implies (and (Holds1 foo ?y)
                        (Holds1 foo ?u))
                   (exists (?z (?w bar1))
                           (and (baz2 ?x (App1 f (g1 ?y)))
                                (not (Holds3 foo ?x ?z (g1 (App2 f ?x ?w))))))))
    

Two Important Special Cases

The translation scheme above is admittedly rather complicated to express in general. This is largely a consequence of the possibility of "partially type-free" languages, i.e., languages in which some, but not all, of the predicates double as individual constants. Additional formal complexity is introduced by the presence of variably polyadic predicates. As noted in the first section above, there are two important special cases of SCL languages at opposites ends of the type-freedom/variable-polyadicity spectrum — TFO languages, which contain no "dual role" predicates and no variably polyadic predicates, and "unconstrained" languages, in which all predicates are dual-role and variably polyadic. In the latter case, the translation function * is trivial, as there are no impure or variably polyadic predicates or function symbols, and hence no need for any of the ⌈Holdsn⌉ predicates or ⌈Appn⌉ function symbols, Thus, for TFO languages, λ* = λ. In the former case, the translation scheme is far more streamlined.

Specifically, where λ is unconstrained, λ* consists of the following:

That is, in this case, all of λ's predicates and function symbols are converted into individual constants, and all predicates and function symbols are of the forms ⌈Holdsn⌉ and ⌈Appn⌉. In this case, thought not as trivial as with TFO languages, the translation scheme is rather less daunting than the general case. Specifically, where once again, L is a language based on λ and App, Holds, Neg, … are its term generator, predication operator, and formula generator, and let App*, Holds*, Neg*, … be those of a language L* based on λ*.

So, for example, if 'father-of(cain)' is a function term of L, — assuming L* has a similar look and feel, and that 'App1' is the App1 of λ* — its translation into a L* would be 'App1(father-of,cain)'.

Now let φ ∈ L:

So, for example, if 'killed(cain,abel)' is an atomic formula of L, its translation into L* — where 'Pred2' is the Pred2 of λ* — would be 'Pred2(killed,cain,abel)'.

Continuing:

Recall again that the general form of quantified formulas involves sequences of the form χ1,…,χn,ψ, where the χi are either single individual variables or pairs of the form ⟨ν,π⟩, where ν is an individual variable and π is a predicate. Since all predicates of our unconstrained λ become individual constants in λ*, given the syntax for restricted quantifiers, all quantifier restrictions are pushed into the body of the translation of ψ. Thus, once again, for a sequence χ1,…,χn of variable/predicate pairs or single variables, let ν1, …, νi the single variables, in order, in the sequence, and let ⟨μ11⟩, …, ⟨μjj⟩ be the variable/predicate pairs of the sequence, in order. Our translation continues as follows:

To illustrate, with sentences similar to the above, suppose L's lexicon contains individual constants 'a' and 'b', function symbols 'f' and 'g', and predicates 'foo', 'bar', and 'baz'. We continue to suppose the grammar of L* to be similar in form to L to simplify the example. Then the following would be example translations according to the above scheme:


(g a (f a b))* = (App2 g a (App2 f a b))

(foo (g a) b (g f (f a)))* = (Holds3 foo (App1 g a) b (App2 g f (App1 f a)))

(forall (?x (?y foo) (?u foo))
        (exists (?z (?w bar))
                (and (baz ?x (f (g ?y)))
                     (not (foo ?x ?z (g (f ?x ?w)))))))* =
  (forall (?x ?y ?u)
          (implies (and (Holds1 foo ?y)
                        (Holds1 foo ?u))
                   (exists (?z ?w)
                           (and (Holds1 bar ?w)
                                (Holds2 baz ?x (App1 f (App1 g ?y)))
                                (not (Holds3 foo ?x ?z (App1 g (App2 f ?x ?w))))))))
    

Transforming SCL1 Interpretations into TFO-agreeable Interpretations

The translations scheme defined in the preceding section is intuitively meaning preserving. This intuition can be expressed precisely in our model theory. This is primarily a matter of defining a method for transforming any interpretation of the lexicon λ on which our SCL1 language L is based into an "equivalent" TFO-agreeable interpretation of λ's fully typed correlate λ*.

The method is quite obvious. Let I = ⟨I,R, ext, V⟩ be an interpretation for λ. Define an interpretation I* = ⟨I*,R*,ext*, V*⟩ for λ* as follows.

It is straightforward to show that I* is a TFO-agreeable interpretation of λ*. Call any such I* a TFO-agreeable correlate of I. The following is an easy induction on the complexity of formulas:

Theorem: Let L be an SCL1 language based on a lexicon λ, let L* be a language based on a fully typed correlate λ* of λ. Then a sentence φ of L is true in an interpretation I iff its translation φ* into L*1 is true1 in any TFO-agreeable correlate I* of I.

Identity

COMING SHORTLY.

References

P. Hayes and C. Menzel. A semantics for the knowledge interchange format. Available at http:reliant.teknowledge.com/IJCAI01/HayesMenzel-SKIF-IJCAI2001.pdf.

Notes

0. The complexity arises from the fact that, to keep the semantics classical, one must introduce a mechanism that guarantees that every term, no matter what it's semantic value, can be applied to arguments in such a way as to "return" a unique value. Such a semantics is worked out in the full Common Logic specification.

1. T is the 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.

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

3. Practically, speaking, of course, Holds should be computable and reversible; that is, given any inputs, we should be able to compute Holds's output, and given any of its outputs, we should be able to compute the arguments that yielded that output.

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 SCL languages below.

5.It is possible to model of the members of R extensionally as sets, though this will in general require non-well-founded set theory, since a relation, qua individual, can be in its own extension.

6. An extensional relation A on a set M is simply a subset of Mω. A is variably polyadic if there are tuples of different lengths in A. A is an n-place extensional relation if every element of A is of length n. An extensional, variably polyadic relation A on a set M is a total (extensional) function on Mω iff for any tuple ⟨a1,…,an⟩ ∈ Mω, there is a unique bM such that ⟨a1,…,an,b⟩ ∈ A. An (n+1)-place extensional relation A on a set M is a total (extensional) function on Mn iff for any n-tuple ⟨a1,…,an⟩ ∈ Mn, there is a unique bM such that ⟨a1,…,an,b⟩ ∈ A.

7. These lexical items of L1 are thus being tapped to play a semantic role in our L1-agreeable interpretation. Any objects would do as the elements of R, of course, but using the lexical elements themselves simplifies the construction.

Valid HTML 4.01!

Last modified: Thu Nov 13 22:26:48 CST 2003