SCL is a simplified version of the Common Logic project @@, which in turn is a proposal to define a 'standard' uniform notation for first-order logic suitable for use as a common notation for a variety of ontology efforts, to facilitate information exchange and interoperability. CL began as an outgrowth of the now somewhat venerable KIF@@ effort, differing from KIF in several respects: a simplified syntax; a more sophisticated semantics; and, by differentiating abstract syntax from concrete syntaxes, providing for a wider range of interoperabilty by linking a variety of existing surface syntactic standards, in particular Concept Graphs@@. SCL attempts to retain these advantages of CL while being somewhat less ambitious, and is consciously intended to also provide a logical notation oriented towards the needs of the emerging Semantic Web@@ effort. In many ways, SCL is nearer in scope to the original KIF.
The 'core' of SCL is presented as an abstract syntax of a rather general logical language with an attached model theory. This core provides the basis for several other aspects of the proposal.
Special cases of the language, which roughly correspond to several known use cases of familiar logical notations, are defined by restricting the syntax in various ways. Syntactically defined sublanguages are referred to as dialects of SCL.
Concrete syntaxes are defined by mapping the abstract syntax into some surface form. These include an S-expression syntax similar to the original KIF@@ notation, an XML-based@@ syntax, a 'classical' infix notation in terms of character strings, a CG@@ version, and a mapping into RDF triples @@. It is anticipated that other concrete syntaxes for SCL and sublanguages will be defined in the future. Concrete surface syntaxes are referred to as syntactic forms.
Extensions of SCL may be defined in many ways, of course, but some particular ways of extending the language by adding new domains with associated lexical forms are defined. This is intended to provide a way of linking SCL with a variety of existing and future efforts on standardizing datatypes@@ of various kinds. Such extensions are referred to as domain extensions.
These are orthogonal, in that any of the dialects can be combined with any domain extension, and the result can be expressed in any of the syntactic forms. However, certain combinations are particularly relevant to some communities in that they closely correspond to existing formalisms and existing 'styles' of formalization, and have been given appropriate names in order to provide some familiar anchoring points for stating conformance conditions.
All the dialects and syntactic forms inherit the model theory of the core language in a uniform way, so that translators between notations can use the abstract syntax as a guide and also as an interlingua for comparing meanings across the various surface notations.
Throughout this section, "SCL" is used to refer to the core language.
SCL is a first-order language with a relatively unrestricted syntax which makes no distinction between relation and individual names, and allows quantification over relations. Since this combination is somewhat unusual, we begin with some motivation and analysis.
It is conventional to define a first-order logic so that the syntax distinguishes
between relation symbols and individual symbols, and allows relation symbols
to be applied only to individual symbols. This 'layered syntax' is
often
asserted to reflect the fact that a first-order theory cannot refer to relations;
but that is an error. The semantics of first-order logic impose no constraint
on
the
nature of the individuals in an interpretation, so there is no prohibition
against a first-order language referring to relations, even to the relations
which are denoted by the relation symbols of that language. This can be seen
by the widespread convention whereby users of a conventional first-order syntax
use a dummy relation to imitate what is often referred to
as "higher-order" syntax by bringing relations into the domain of
discourse. Using this convention, one represents an atomic assertion such
as R(a,b) by writing instead Holds(R,a,b) where the
relation symbol has been translated into a constant symbol. The use of a 'holds
predicate' in this way has several problems, however, the chief one being that
it requires users
to distinguish syntactically between a relation named by a relation symbol
and the same relation named by a constant symbol. Some implementors have allowed
languages in which the same symbol may be used in both senses, but in order
to map this into a conventional first-order syntax, and to interpret it in
a conventional model theory based on Zermelo-Fraenkel set theory, it is necessary
to regard
this as a form of 'punning', ie to treat the two uses of
the same
symbol
as
having
distinct
denotations, in order to avoid an interpretation in which a relation is applied
to itself, a condition which would violate the ZF axiom of foundation.
The axiom of foundation, which requires sets to have a finitely deep layered
hierarchical structure of subsets, was imposed within axiomatic set theory
in part as a
response to the Russell paradox.
It reflected a constructivist view of legitimacy in mathematical structures which
was suspicious of any forms of construction which could not be rooted in finitely
describable However, recent
work @@ in set theories, inspired in part by computational considerations,
has shown that, contrary to the previously accepted view
in
philosophy
of
mathematics,
the
axiom of
foundation
is not required in order to have a coherent theory of
sets,
and
that a wider range
of set theories which include the possibility of an 'anti-foundation'
axiom are all relatively consistent with ZF set theory. Applied to the basic
set-theoretic
framework of model theory, this opens up new possibilities for overcoming the
expressive awkwardness which has long been a regrettable side-effect of the
'layered' syntax of conventional first-order logic. SCL syntax takes advantage
of this flexibility by allowing complete flexibility in using a symbol to denote
a relation which is both an
entity
in the domain of quantification and a relation defined over that domain, thereby
obviating the need for the use of tricks like the Holds predicate.
Although this flexibility is innovative, the resulting language is still first-order
in the conventional sense, and as we will show, conventional inference systems
can be adapted to SCL with minimal changes. The conventional layered first-order
syntax is a dialect of SCL.
It is possible to give SCL a conventional model theory which is indistinguishable from the usual textbook model theory, provided that one understands the set-theoretic constructions as described using a non-well-founded set theory. Since this is likely to be a rather radical move for many readers, we have chosen instead to provide a slightly modified model theory which is based on conventional ZF set theory. By imposing an intensional interpretation on relations, this model theory has other expressive advantages in any case. In later sections we discuss the relationships between these two model theories in more detail.
The other unusual feature of SCL is its inclusion of a special category of variables called row variables. This is an inheritance from KIF, but the treatment has been made more systematic in SCL. The reason for including row variables is to allow users to take advantage of the possibility in SCL of having variadic relations, ie relations which can be true of different numbers of arguments. It is usual for logical languages to require relations to have a fixed number of arguments, often called the arity of the relation; but SCL does not require this, and treats a relation in general as any set of n-tuples. This provides a useful degree of expressive power for many applications, and avoids the awkward use of explicit argument lists and similar constructions (eg the use of explicit lists in translating between OWL and RDF, c.f. @@). It does however pose something of a challenge for the language, which can be illustrated by an assertion that one relation R entails another, Q. If the relations were binary, this could be expressed by saying that for any x and y, if R holds between x and y then Q holds between them. If they were three-argument relations, a similar
One can give a succinct characterization of SCL as a logic of relations. It assumes that there is a universe of things over which the quantifiers range, that relations - sets of n-tuples - are defined over the universe, and that the basic atomic assertion is that a relation holds between some things in the universe. The design of the language follows from taking this description exactly at face value, and trying to impose no other constraints or restrictions on what can be said in the language.
A vocabulary is a set of names, which are distinct syntactic entities. SCL also uses primitive symbols called variables and row-variables. The abstract syntax assumes that names, variables and row variables are disjoint sets, although particular syntactic forms may allow them to be lexically identical.
We state the abstract syntax using an algebraic variation of EBNF, in which a particular syntactic construction is indicated by listing the immediate components of the expression separated by commas. The ordering of these items serves only to distinguish the components and should not be taken as indicating any lexical order in a particular surface syntax. The only ordering contruction used in the syntax is the notion of a row, which is a finite sequence of terms. Alternatives are indicated by | , and brackets '(', ')' are used for grouping. * indicates an arbitrary number, + an arbitrary nonzero number, as usual.
row ::= term*
term ::= name | variable | term, (row | row, row-variable )
atom ::= name | term, (row | row, row-variable )
sentence ::= atom | boolean-sentence | quantified-sentence
boolean-sentence ::= negation | conjunction | disjunction | conditional | biconditional
negation ::= sentence
conjunction ::= sentence*
disjunction ::= sentence*
conditional ::= sentence, sentence
biconditional ::= sentence, sentence
quantified-sentence ::= universal-quantified-sentence | existential-quantified-sentence
universal-quantified-sentence ::= (variable | variable, sentence)+ , sentence
existential-quantified-sentence ::= (variable | variable, sentence)+ , sentence
This syntax is fairly conventional. It allows restrictions on quantifiers and a full range of boolean forms as a convenience. The unusual features include the absence of any syntactic distinction between individual and relational names, and the corresponding lack of any prohibition against general terms appearing in relation position of atomic sentences, and allowing row variables in atoms and terms.
SCL also allows wrappers, which are semantically empty forms which allow comments or other external text to be attached to SCL expressions. Technically, any wrapper has two components, one of which is a unicode character string called the comment and the other may be an SCL expression. A wrapper is treated logically by SCL as being identical in meaning to the enclosed SCL expression, and is considered to have the same syntactic type as that expression, so that a wrapper of a name is a name, of a term is a term, and so on. Particular SCL dialects may use different ways of indicating wrappers and may also restrict the range of unicode characters in the comment, or may require comments to conform to some other grammatical conventions. Wrappers with no enclosed SCL expression are simply called comments. Comments are are considered to be syntactically legal SCL expressions but cannot appear as subexpressions of any other SCL syntax, and have no model-theoretic content.
To illustrate the use of an abstract syntax, we sketch two very different concrete syntaxes for this language which are both realizations of the same abstract syntax. The first uses a conventional linear notation in which atoms and terms are indicated by writing the relational or function name followed by the argument row enclosed in brackets, and the type of a boolean sentence is indicated by inserting a suitable connective name between the subcomponents. The other syntax, inspired by C.S.Peirce's 18@@ notation, is diagrammatic. Here, an atom is indicated by a labelled graph consisting of the relation name linked to the argument nodes by arcs labelled with integers which show the ordering of the argument row; conjunctions are formed by graph union, negations by an enclosing loop, and other boolean combinations are mapped to their conjunctive-negation equivalents; and quantifiers are indicated by placing the variable nodes in suitable places in the nested negation loops. To emphasise, these are in some important sense the same expression, in spite of their different forms; an observation whnich can be characaterized by saying that they have the same abstract syntactic description.
@@ insert diagram using example.
Model theory