A "Pure" First-order Abstract Syntax and Semantics for SCL

Common Logic Working Group

Syntax

Lexicon

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

A countable set PredCon called the predicate constants of λ. (We will also sometimes refer to the members of PredCon simply as predicates.) PredCon shall contain at least one distinguished element Id.
A countable set FnSym called the function symbols of λ.
A countable set IndCon called the individual constants of λ.
A denumerable set IndVar called the individual variables of λ;

PredCon, FnSym, IndCon and IndVar shall be pairwise disjoint. Let PrimTrm = IndCon ∪ IndVar; PrimTrm is known as the set of primitive terms of λ.

Note that, unlike traditional logical languages, predicate constants and function symbols are not assigned a unique arity; as will be seen explicitly in the following subsection, the predicates and function symbols of an SCL language can legitimately can take any number of terms as argument.

SCL Languages

Every SCL 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.

Terms

Given an SCL lexicon λ, we define the notion of a term class based on λ. Intuitively, a term is either a primitive term (indiviudal 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* = ∪_0≤n<ωMⁿ, where Mⁿ 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 class ¹ closed under an operation App — called a term generator for λ — such that

App is one-to-one;
App : FnSym × T* → T.

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

So, for example, if a and b were among the individual 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: fagb, f(a,g(b)), (f a (g b)), and even

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

Formula classes

We now do for formulas what we just 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. For this we simply require that there be a one-to-one function Pred on PredCon × Trm*; given a predicate constant and n terms, that is, Pred generates a unique formula. Any such function Pred 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.³ Given a term generator, the range of a predication operation for λ is said to be a class of atomic formulas for λ.

Let At be a class of atomic formulas for λ. Say that F is a formula class for λ, relative to Pred, if it is the smallest class that includes At and is closed under a set Op — known as a formula generator for λ based on Pred — of operations 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 : Trm × Trm → F
Neg : F → F
Conj : F* → F
Disj : F* → F
Cond : F × F → F
BiCond : F × F → F
ExQuant : (Var ∪ (Var × PredCon))* × F → F
UnivQuant : (Var ∪ (Var × PredCon))* × F → F

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

UnivQuant(ν₁,Cond(Pred(π₁,ν₁),ExQuant(ν₂,Conj(Pred(π₂,ν₂),Pred(π₃,ν₁,ν₂)))))

where π₁, π₂, and π₃, are "slots" for the predicates chosen from any particular lexicon to represent boyhood, girlhood, and kissing, and ν₁ and ν₂ represent some choice 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>
            <pred>Boy</pred>
            <var>x</var>
          </atom>
        </formula>
        <formula>
          <exists>
            <var>y</var>
            <formula>
              <and>
                <formula>
                  <atom>
                    <pred>Girl</pred>
                    <var>x</var>
                  </atom>
                </formula>
                <formula>
                  <atom>
                    <pred>Kissed</pred>
                    <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. ⁴ 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 φ.

Let App be a term generator for λ, where Trm is the set generated by App, and let Pred be based upon App. Let Op be a formula generator for λ based on Pred, 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 λ. Alternatively, 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 L and L′ are SCL languages for λ and λ′, respectively, then L and L′ are said to be equivalent.

Semantics

Interpretations

Let L be an SCL language for λ, and let Trm be the terms of L. A SCL interpretation I for L is a 4-tuple ⟨D,R,ext,V⟩ satisfying the following conditions. First, D and R are nonempty sets such that D ∩ R = ∅. Intuitively, D 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 relations-in-intension (though, as will be seen, it is possible to think of them extensionally as sets). Its members will serve as the semantic values of predicates. ext is a function from R into D*. Intuitively, ext(r) represents the extension of r. For elements r of R, if ext(r) is a total function on D*, then we say that r is a functional relation. If FnSym is not empty, we require that at least one element of R be functional. Finally, V is a "denotation" function that assigns appropriate values to the primitive terms of L. Specifically,

If τ is a primitive term (individual constant or variable), then V(τ) ∈ D,
If α is a function symbol, then V(α) is a functional relation.
If π is a predicate constant, then V(π) is a member of R.

Denotations and Truth

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

Further notation will be useful in defining truth for quantified formulas (i.e., formulas in the range of ExQuant and UnivQuant). What we are after is the notion of an interpretation I′ that is exactly like a given interpretation I except that it might not agree with I on one small (but crucial) point, namely, what to a assign to one particular variable. The presence of restricted quantifiers forces us to proceed with some care. First, the, where χ is either a variable or a variable/predicate pair that can, therefore, be used to form a restricted quantifier, |χ| simply be χ itself if χ is a variable, and if χ is a variable/predicate pair ⟨ν,κ⟩, let |χ| be the variable ν of the pair. Now let I = ⟨D, R, ext, V⟩ be an interpretation for L. In our syntax, a quantifier can bind an entire sequence consisting of variables and variable/predicate pairs. So we let χ₁,…,χ_n be such a sequence, and we say that V′ is a [χ₁,…,χ_n]-variant of V iff

V′(ν) is in the extension of the relation V(κ) that V assigns to κ, if χ_i is a variable/predicate pair ⟨ν,κ⟩;
V′(τ) = V(τ), if τ ≠ |χ_i| for any i, 1 ≤ i ≤ n, i.e., if τ distinct from all the variables in the sequence χ₁,…,χ_n and all of the variables occurring in variable/predicate pairs in the sequence.

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

Thus, to spell out somewhat more precisely what we noted above, 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 variable (i.e., each |χ_i|) in the sequence χ₁,…,χ_n; in particular, in the case where χ_i is a pair variable/predicate pair ⟨ν,κ⟩, V′ assigns a member of the extension of V(κ) to ν. This somewhat complicated definition --- necessitated by the ability of quantifiers to bind a sequence that can be a mix of both variables and variable/predicate pairs --- enables the formulation of the very simple definition of truth for quantified formulas below.

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

If τ is a primitive term, then V^#(τ) = V(τ).
If τ = App(α,τ₁,…,τ_n) ∈ FuncTrm, then V^#(τ) = V^#(α)(V(τ₁,…,V(τ)_m),

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

If φ = Pred(π,τ₁,…,τ_n), then φ is true in I iff ⟨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.

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

Notes

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, Pred should be computable and reversible; that is, given any inputs, we should be able to compute Pred'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.