Common Logic: Abstract Syntax and SemanticsCommon Logic Working GroupIntroductionThe 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 higher 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. SyntaxLexiconA CL language is based upon an initial stock of primitive syntactic entities. Specifically, a CL lexicon λ consists of the following mutually disjoint sets:
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 LanguagesEvery 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 in Section ??? below. Term ClassesFor any set M, let M* be the set of finite sequences of elements of M, i.e., M* = ∪1≤n<ωMn, where Mn 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 the primitive terms of λ and is closed under an operation App — called a generator for T — such that
For any term class Trm for λ, let FuncTrm = Range(App),3 where App is a generator for Trm, and let SingTrm FuncTrm is the set of function terms of λ (relative to Trm), and SingTrm is the class of singular terms of λ (relative to Trm). Formula classesLet λ 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. Say that F is a formula class for λ, relative to Trm, if it is a smallest class that includes FuncTrm and is closed under a set Op — known as a generator set for F — of operations Id, Neg, Conj, Disj, Cond, Bicond, ExQuant, UnivQuant that satisfy the following conditions:
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.4 Let φ ∈ Fla. An object ε in the decomposition of φ is an atom of φ just in case ε is element of the lexicon λ. φ is atomic if φ ∈ FuncTrm. ψ 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. 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. SemanticsInterpretationsLet 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 〈e1, …, en〉 ∈ D*, say that an object e ∈ D is defined on 〈e1, …, en〉 in I just in case there is at least one object e0 ∈ D such that 〈e0, e1, …, en〉 ∈ ext(e). Define an I-skolemization of e to be any (total) function f : D* → D such that, for all 〈e1, …, en〉 on which e is defined we have 〈f(e1, …, en), e1, …, en〉 ∈ ext(e).5 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 typically rendered innocuous by a proper formulation of one's axioms.6 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 TruthGiven 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 s1,..,sn, let cnct(s1,..,sn) be the concatenation of s with s′.7 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 χ1,…,χn ∈ (Var ∪ (Var × Con)), say that V′ is a [χ1,…,χn]-variant of V iff,
We then say that an interpretation I′ = 〈D, ext, skol, V′ 〉 for L is a [χ1,…,χn]-variant of I iff V′ is a [χ1,…,χn]-variant of V. In plain but somewhat less precise English, a [χ1,…,χ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:
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 p1 and p2 just in case o has moved from p1 to p2. Thus, in an interpretation where V('a') is o and V('@r') is the pair 〈p1,p2〉 ('@r' here being a sequence variable), we want 'Moved(a,@r)' to be true just in case the triple 〈o,p1,p2〉 ∈ 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〉,〈p1,p2〉) = 〈o,p1,p2〉) ∈ ext('Moved'). Given V, we define truth for the formulas of L in our interpretation I as follows. Let φ ∈ L.
Paradigmatic CL LanguagesKIFCGIFComplianceIn the simplest case, then, to demonstrate that a given language L* is compliant with the CL standard means simply that one can demonstrate that it is an instance of a CL language. More exactly, it means:
Indirect ComplianceCertain familiar classes of languages cannot be shown to be CL compliant simply because they are syntactically less anarchic. Nonetheless, these languages can still be thought of as CL compliant in a robust, well-defined sense. Specifically, where L is a CL language, we define a subset L′ ⊆ L to be indirectly compliant 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 compliant, one must simply provide a recursive specification of L′ relative to some CL language L. Typically, of course, a specification of an indirectly compliant language will be provided independent of any specific CL language. The class of interpretations for an indirectly compliant 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 compliant language. A language will be said to be CL compliant (compliant, for short) just in case it is either a CL language or indirectly compliant relative to some CL language. Standard FOL: An Example of Indirect ComplianceThe standard language of first-order logic, relative to some choice of constants, is a prime example of an indirectly compliant language. Specifically, let L be a CL language for some lexicon λ. Let arity be a total recursive function from some subset of Con into the set of natural numbers. Let τ ∈ Con. We say that τ is an n-place predicate (relative to arity) if arity(τ) = n. Otherwise we say that τ is an individual constant (relative to arity). We then define the standard first-order sublanguage L1 of L determined by arity to be those formulas of L which contain no sequence variables and whose atomic subformulas α are all such that α = App(π,τ1,…,τn), where π is an n-place predicate and each τi is an individual constant or an ordinary variable of λ. L1 is clearly indirectly compliant. Notes1. 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 compliant 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. We will discuss this in Section ?? 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. 7. More exactly, where s = 〈e1,…,en〉 and s′ = 〈en+1,…,en+m〉, cnct(s,s′) = 〈s1,…,sn+m〉. |