This is a dynamic document which is subject to continual change and revision. Please make sure you have the latest version before citing or commenting. Comments and feedback welcome, on anything from typos to philosophy, helpful or hostile. Please especially remark on anything that seems obscure or hard to follow, as it is intended to be readable.
This version created
@@boldface like this@@ indicates stuff not yet done, side comments for the CL cognoscenti, or a direct request for feedback/comment.
TO DO:
EDITORIAL references, links
TEXT more examples, section on representing sorts, vocabulary for sorts, namespace draft.
Abstract
Introduction
Logical names, strings, etc.
Numbers and strings as datatypes
Namespaces
Terms and atoms
Classes and properties: a note
Propositional names
Sentences
Sequence variables
Comments, text, importing and resources
IKL and description logics
Datatypes and literals
Contexts, holdings and referential opacity
Referring to things inside contexts
Referring to things at different times
Best Practices, sinkholes, tar-pits and examples.
Appendix A: vocabulary listing
Appendix B: EBNF
References
This is a description of the current state of the IKL language specification, intended as a general informal guide and overview. It does not give formal details of syntax or semantics, and some of it is provisional. Feedback, comments are welcome.
IKL is a variant of Common Logic, extended in several significant ways, most notably by providing for terms denoting propositions, which are first-class entities in IKL. Common Logic (CL), in turn, is a proposed ISO standard for a general-purpose first-order information exchange language, based loosely on KIF. The design rationale for CL is explained in [CL], but in summary, it is designed to remove or avoid as many restrictions as possible on what can be said in a first-order language. As a result it has many features often associated with richer languages such as higher-order logic.
Although it provides for the expression of contextual and time-dependent truths, IKL is not a context logic or a temporal logic. Assertions made in IKL are simply asserted to be timelessly true: they should not be understood to be asserted in a context or at a time. All such relativizations of assertion or truth must be made explicit in IKL by referring explicitly to the context or time-interval relative to which they are intended to be understood. Several special syntactic forms are provided or suggested for such uses. Similarly, names used in IKL are understood to refer to their referents in a single referential framework: they do not change their referents when used in a different context. Any such variations in reference should be made explicit, for example by the use of functions from contexts to referents. What this means in practice is that equality substitution applies throughout IKL reasoning: IKL is referentially transparent. (This requires particular care when representing information about traditionally opaque contexts such as beliefs: more details below.) IKL is not sorted or typed, so that any name may be used in any context, but it has provisions for describing sortal restrictions in other frameworks. IKL provides a number of specialized vocabularies for referring to situations, times, contexts and 'frameworks', where a framework refers to one of the alternative notations or ontological settings from and to which IKL can be translated. The universe of discourse of IKL is intended to encompass all of these other frameworks, and to be able to express relationships between them. Thus, one will typically expect that IKL quantifiers range over a larger universe of entities than those in most of the other frameworks.
IKL syntax is based on CLIF, the KIF-like syntax defined for ISO Common Logic [ISOCL]. For a full description of CLIF syntax, see [CL]. Briefly: it looks like a conventional logic, except that atomic sentences and terms are written with the relation or function name after the opening parenthesis, so one gets things like
(Married (fatherOf Arthur) Ygraine)
rather than
Married(fatherOf(Arthur), Ygraine)
This same style is used for the quantifiers and connectives, which are all written as prefixes rather than as infixed, so that one gets things like
(forall (x y) (if (Married x y)(Married y x)) )
rather than
forall (x) ( Married(x, y) implies Married(y, x) )
Fuller details are given below. We explain the language by building up the syntax from the simplest elements to the highest-level constructions.
IKL does not place any restrictions on the character strings to be used as logical names or identifiers: almost any string of Unicode characters can be used, no matter how long. (It must contain at least one non-whitespace character and must not be a numeral, or any of certain words reserved for special use in IKL.) This enables things like URIs, or even paragraphs of text, to be used as logical identifiers. (Note however that such names are identified strictly by lexical identity as normalized Unicode character strings, including characters such as line breaks and carriage returns, so re-formatting a paragraph could change it into a different identifier.)
If the string contains characters which would break the normal IKL parsers, such as whitespace, parentheses or quote marks, it should be enclosed inside double-quote characters. For example, this is a legal IKL atomic sentence, containing two names, the second being 'foo':
("A very long predicate name which (while syntactically legal)
is probably not best taken as a \"guide to good practice\"" foo)
The enclosing quote characters are not considered to be part of the name: to include a double-quote character, prefix it with a backslash, as shown. (To include a backslash, precede it with another backslash. To include non-ASCII characters in an ASCII character stream, use a backslash followed by the Unicode hexadecimal encoding. All other occurrences of backslash are considered to be lexical errors.) A logical name may be written using any Unicode characters, which include those from a large variety of human alphabets and technical notations. Unlike KIF, IKL does not standardize case: names are case-sensitive.
Any consecutive string of whitespace characters counts simply as a single lexical break, so IKL text allows (but does not require) the use of layout conventions such as indenting with spaces or tabs, or vertical alignment of matching parentheses. Since parentheses are treated as lexical break characters, names which include parentheses must be enclosed in double-quote marks.
A similar construction using single instead of double quotes, called a quoted string, is a logical constant with a fixed meaning, and it denotes the string itself (with backslashes treated appropriately, see below). Note that this is a very different usage: a quoted string cannot be used as a logical name. Thus, it is important to bear in mind the difference between single and double quotes: they are not interchangeable. This differs from the XML conventions. As above, the enclosing quotes are not considered to be part of the string, and to include a single quote mark or a backslash inside a quoted string, precede it with a backslash. Backslashes not followed by a single quote, Unicode hexadecimal code or backslash are considered to be lexical errors.
IKL does not have a special notational convention for variables. In fact, strictly speaking, there is no such thing as a variable in IKL: a "bound variable" is simply a name that is bound by a quantifier, and any "free" variables are simply treated as logical names. The wide lexical freedom of IKL name strings means that IKL can usually accomodate to any special lexical conventions for variables which users might like to adopt. Examples of these include the Prolog convention of using upper case for variables, and the widespread use of a '?' prefix to mark a variable. However, several widely-used conventions regarding free variables do not apply in IKL. Any free names are treated as logical constants, even such names as '?x', so all quantifiers should be indicated explicitly.
IKL, following CL, does not distinguish lexically between different categories of names, such as individual, property, relation, class, datatype or function names, etc.. Any name may be used in any of these roles, and the same name may be re-used in any other role, and any name in any role or position may be bound by a quantifier. This also applies to the number of arguments which a relation is allowed to have: all relations and functions in IKL can be given any number of arguments as far as the logic is concerned. Thus, the concept of arity (the number of arguments a relation or function is allowed to have, considered as a lexical or syntactic constraint on wellformedness) has no logical meaning in IKL (or, if one prefers, all relations and functions are variably polyadic). If one wishes to indicate restrictions, such as that a particular name is intended to be used only with, say, two arguments, or only as a relation symbol, this must be done by asserting user-defined properties, for example
(and (isRelation R)(arity R 2))
but these do not in themselves make other uses of the symbol logically inconsistent or illegal.
Names which begin with the three-dot sequence '...' are used in a special way in IKL as sequence variables (explained below), so should not be used as logical names. The character sequences reserved to identify the quantifiers and connectives, the equality sign and so on, should not be used as logical names, and the single and double quote marks cannot be used as the first character in a name. Finally, IKL uses decimal numerals to denote integers, so numerals should not be used as names, nor as the first character in a name.
Quoted strings and numerals are given fixed meanings in IKL. These can be regarded as two special cases of a more general category of literals, i.e. expressions with a fixed meaning (in more philosophical terminology, rigid designators; in less philosophical terms, proper names) which are represented generically in IKL, following RDF, by a string together with a name denoting a datatype, which is understood to have its meaning fixed by some external authority. In IKL, the datatype name indicates a function applied to the string.
Any name can be used to identify a datatype, but as the burden of interpreting a literal is quite high, axioms should use only datatype names which are recognized by all applications as meaningful. Typically, application languges will advertize such lists of allowable datatypes as part of their specification: for example, RDF recognizes the primitive datatypes of the XML Schema datatype suite. IKL does not impose any such recognition requirements itself.
The IKL name for the datatype of integers is ikl:number and for character strings it is ikl:string. The class of all datatypes is called ikl:datatype; note that the denotation of this is determined by the conventions adopted for the entire network. Datatypes and literals are described more fully later.
Semantic Web languages are the first to be designed for use on an open network, and one novel aspect of the resulting design is the requirement that they use names which are globally unique, achieved typically by including a URI, i.e. a unique global network identifier, as part of the name, and using the XML namespace conventions to abbreviate the resulting (often very long) names. This produces qualified names which combine a namespace prefix, defined in the header of an XML document, with a local name, joined with a single colon, as in rdf:type, abbreviating http://www.w3.org/1999/02/22-rdf-syntax-ns#type which is globally unique by virtue of containing the unique URI http://www.w3.org/1999/02/22-rdf-syntax-ns. This mechanism has several operational advantages, and is adopted in IKL.
A namespace is a collection of names, and is itself identified by a globally unique identifier, and has a prefix, both of which are IKL names. We will often simply identify the namespace with its name and/or its prefix. Names in the namespace are written in the form prefix:name and are understood to be a shorthand for a global name of the form identifier#name. The namespace is, technically, the set of global names,. but is usually identified with the prefix. This is essentially the XML namespace design [XMLNS http://www.w3.org/TR/REC-xml-names/].
The PURL domain /NET/IKL (identified by the Permanent URI http://purl.oclc.org/NET/IKL) has been created for IKRIS use. The namespace prefix ikl is the abbreviation of the URI http://purl.oclc.org/NET/IKL/base, and should be so identified in XML headers, etc..
IKL follows conventional logic in building its simplest atomic sentences out of terms, which are similarly formed by applying a function to some arguments, which themselves might be terms or simply names. The earlier example is such an atom:
(Married (fatherOf Arthur) Ygraine)
in which the first argument, (fatherOf Arthur) is a term formed by applying the function fatherOf to a single argument. As mentioned earlier, IKL follows CL (and KIF and, ultimately, LISP) in enclosing the function or relation name inside the parentheses.
However, IKL also allows the relation or function to be represented by a term. The functions of these terms have values which are functions or relations. This allows IKL to express what appear to be higher-order facts (they are still first-order in their semantics, because of how quantifiers are treated in IKL). Although many KR formalisms have traditionally avoided these kinds of construction, they can be quite useful. For example, a functional relationship between relations, such as owl:inverseOf, can be axiomatized and used directly as a function on relations:
(forall (r x y)(iff (r x y)((owl:inverseOf r) y x) ))
Note that second atom in the biconditional has a term, not merely a name, in the relation position. owl:inverseOf can be viewed as a functional, ie a 'higher-order' function from relations to relations. As this example also shows, a quantifier may bind a name (r) which occurs both in a relation position and as an argument. This is legal in IKL: any logical name can be bound by a quantifier, including names of relations, functions, etc.. One can now write, for example
((owl:inverseOf Married) Uther Ygrain)
which is (assuming the above axiom) exactly equivalent in meaning to
(Married Ygrain Uther)
The ability to apply functions and relations to relations, and to quantify over relations, allows IKL axioms to describe a number of what are usually considered to be meta-level conventions. For example, consider allowing an intuitively unary property, say a class name such as isHuman, to take any number of arguments, so that
(isHuman Fred Bill Mary)
abbreviates
(and (isHuman Fred) (isHuman Bill) (isHuman Mary))
This convention does not of course apply to all three-place relations, but it can be defined as a property of a relation - let us call it Predicative - and one can write
(Predicative isHuman)
to indicate that the abbreviation convention applies to this relation. Predicative can itself be axiomatized in IKL, using sequence variables (described later): the case for three arguments can be written as the IKL sentence
(forall (r)(if
(Predicative r)
(forall (x y z)(iff (r x y z)(and (r x)(r y)(r z)) ))
))
If dealing with a large number of such relational classifications, one could use the same abbreviational convention on Predicative itself by asserting
(Predicative Predicative)
allowing such abbreviations as
(Predicative isHuman isAnimal isFish)
This illustrates another important freedom in IKL, the lack of a type heirarchy. IKL is a completely type-free language, and does not restrict the applications of functions and relations to arguments by checking their types or sorts. In particular, as illustrated here, it is quite legal to have 'loops' of applications.
The quantifier (forall (f... in the first example above can be read intuitively as saying 'for all functions'; although it is important to bear in mind that 'all' here means only 'all functions which are in the universe' , and that this might be a considerably smaller set of functions than 'all possible functions' or 'all mathematically definable functions'. In general, such 'higher-order' quantifications in IKL should be understood as applying only to functions or relations which have explicit names. IKL does not have any function or relation comprehension principles built into it which guarantee the existence of functions or relations: if these are required they must be stated explicitly as axioms.
As noted earlier, the fact that a name is used as a relation does not prevent it being also used for relations with other numbers of arguments. Note that the axiom given above for Predicative uses the parameter r only with three arguments and with one argument. This means that no consequences would follow from this axiom and an assertion with some other number of arguments, e.g. the above axiom plus
(Predicative BinaryExample)
(BinaryExample a b)
does not entail
(and (BinaryExample a)(Binaryexample b))
In general, one can think of each 'use' of a name, e.g. as a relation with 3 arguments, or as a function with 2 arguments, as separate from the other 'uses'. (Sequence variables, described below, allow one to write axioms which apply to uses of a name with any number of arguments. The above conclusion would be entailed by the more general definition of 'predicative' given later, which is designed to cover all numbers of arguments.)
One special case of an atom is an equation, in which the equality sign acts syntactically just like a binary relation name. However, equality is considered a special logical sign, and cannot be used as an argument, quantified over or treated as an individual thing. In particular, while one can establish relational identity using equality:
(= owl:sameAs anotherIdentityRelation)
this is illegal:
***WRONG*** (= anotherIdentityRelation =)
Equality applies to all uses of the name. Thus if one asserts that (= rel1 rel2) then all uses of the name 'rel1' - as an individual thing, a relation with any number of arguments, as a function or as a propositional variable - will be exactly the same in meaning as the similar use of 'rel2'. (This is why the first relational-identity statement works.)
If one wants to establish a more limited notion of identity, e.g. that two relations are true for the same arguments, but not that they are necessarily identical, then use an explicit axiom, e.g.
(forall ((x isMammal)) (iff (isHuman x)((AND hairless bipedal) x) ))
rather than
(= isHuman (AND hairless bipedal))
One can axiomatize such relations and name them, eg
(forall (x y)(iff (sameProperty x y)(forall (u v)(iff (x u v)(y u v))) ))
(forall (x)(iff (sameClass x y)(forall (u)(iff (x u)(y u))) ))
The recently defined semantic web languages RDF, RDFS and OWL, following terminology introduced by the description logic community, refer to classes and properties. These are usually naturally rendered in IKL as relations taking one and two arguments respectively, as illustrated in the above definitions of sameClass and sameProperty. Thus, the RDF triple
ex:aaa ex:property ex:bbb .
is naturally transcribed in IKL as the atomic sentence
(ex:property ex:aaa ex:bbb)
but if the property of the triple is rdf:type, so that the object of the triple is considered to be a class, then it is more natural to write
(ex:aaa ex:bbb)
These two (and other) conventions can be used together and related by IKL axioms, such as
(forall (x (y rdfs:Class))(iff (rdf:type x y)(y x)))
There are other 'natural' exceptions, particularly for RDF graphs which use the RDF collection or the OWL/RDF vocabularies (see [SW2CL] for a complete translation of RDF, RDFS and OWL into CLIF) , but this is usually the best way to transcribe RDF in the absence of any other information. In general, we will simply subsume the terms 'class' and 'property' under the category of relations in IKL.
Note, however, that it would usually be incorrect to assume that every unary relation was an OWL or RDFS class, or that every binary relation was an RDF or OWL property, as these languages are less expressive than IKL.
IKL treats propositions as first-class entities, so that one can refer to propositions by name, quantify over them, have relations between them and other entities, define functions which apply to them, and so on. (What it does not have, however, is a truth predicate, i.e. a way to assert that a described proposition is true. This helps avoid paradoxes.) Since sentences indicate propositions, a sentence in IKL can be understood either as an assertion or as the name of proposition, which introduces a potential ambiguity which IKL resolves by a special construction. A sentence enclosed inside the operator that is a name, denoting the proposition expressed by the sentence. Thus for example,
(Married Ygrain Uther)
is an IKL sentence which can be asserted, but
(that (Married Ygrain Uther))
is an IKL name, denoting the proposition that Ygarin and Uther are married. The name simply denotes the proposition, and says nothing about its truth. Such an expression, consisting of a sentence enclosed inside that, is called a proposition name. A proposition name has exactly the same meaning as the enclosed sentence: the proposition it denotes is the very same proposition expressed by the sentence. Proposition names are so called because although they may have a complex sentential structure, considered as propositions they all act as simple names, and play the same role in propositional term syntax that simple names play in regular term syntax.
Note that that is not simply a function, but must be regarded as a logical operator, as it plays a special role in the syntax: the expression occurring inside (that ...) must be parsed as though it were a sentence.
The names occurring inside a proposition name are understood to have the same references that they have in normal IKL text, so that one can bind them with quantifiers in the same way. This allows 'quantifying in' to a proposition term:
(exists ((x isHuman)) (Believes LoisLane (that (= x Superman)) ))
Note, sentences, and hence proposition names, in IKL are referentially transparent, which means that attributions of belief have to be handled with some care. We enlarge on this below.
The IKL semantics guarantees that all IKL sentences denote a corresponding proposition, and all such propositions are first-class 'things' in the universe of discourse, so can be referred to by other names and quantified over. However, to avoid ambiguity, one should use the form (that p) rather than the simple name p, when the name is intended to refer to a sentence and is used inside another term or atom. Applying that to a simple name is legal, and the resulting expression is also categorized as a proposition name. These can play the role of a 'propositional variable' referring to an arbitrary proposition. If the inner simple name is bound by a quantifier, the effect is to quantify over all propositions (i.e. all the propositions that can be expressed using the IKL vocabulary.) For example, to say that Bill believes some proposition which Joe believes to be false, one could write
(exists (p) (and
(Believes Bill (that p))
(Believes Joe (that (not p)))
))
The second argument of Believes applied to Joe is a propositional name, indicated by that. Note that in the second example there is no need to write (that (not (that p))) since the only legal way to parse the 'inner' name is as a sentence. In general, the use of 'that' is required only where the sentence or name might be misunderstood as a term or a non-propositional name. One can think of that as a coercion operator which forces its argument to be parsed as a sentence and hence interpreted as denoting a proposition, and the connectives and quantifiers already apply this coercion. Note however the difference between
(P (f a))
and
(P (that (f a)))
Both are legal atomic sentences, but the second refers to a proposition: f plays the role of a relation name, and(f a) is an atomic sentence expressing a proposition, which has the property P. In the first, (f a) is a normal term denoting an object. This is a case where that must be used in order to avoid ambiguity. In general, it is best to insert that when one wishes to refer to a proposition, an case there is doubt about whether it may be safely omitted. The that operator is idempotent, i.e.
(forall (p) (= (that (that p)) (that p) ))
so it does no harm to include it where it is not strictly needed.
Although sentences name propositions, there is no 'unique naming' convention. Different sentences might name the same proposition. The use of a different bound name in a quantifier does not give a different proposition: (that (exists (x)(loves Jim x))) denotes the same proposition as (that (exists (y)(loves Jim y))). Merely using a different name to refer to something in a sentence does not change the proposition: if Venus is the evening star, then the proposition that Venus is bright is the same proposition as that the evening star is bright. These are required to ensure that quantification works in the same way throughout the language. However, these are the only equivalences that IKL actually imposes on propositions, as a matter of logic.
One might argue that logically equivalent sentences should always express the same propositions, or that only 'obviously' equivalent sentences should (e.g. (that (and p q)) vs. (that (and q p))), but it is tricky to come to universal agreement on what counts as 'obvious'. The Interoperability WG therefore has decided to not impose any such 'obviousness' conditions on IKL propositions, but to include in IKL a predefined relation of propositional equivalence, written =p=, embodying what IWG considers to be the most universally appropriate such conventions, and intended to be used as a 'practical' propositional identity relation, intuitively meaning 'saying the same thing'. Users who prefer to use a different notion may define and axiomatize their own notions of propositional equivalence. IKL propositional equivalence is reflexive, transitive and symmetric and satisfies the following identities:
(forall (p q)(and
(=p= (that (and p q)) (that (and q p)) )
(=p= (that (or p q))(that (not (and (not p)(not q)))))
(=p= (that (if p q)(that (or (not p) q)) )
(=p= (that (iff p q))(that (and (if p q)(if q p))))
(=p= (that (and p p) (that p))
))
In addition, propositional equivalence satisfies the the deMorgan equivalence: for any name n and any sentence PHI,
(=p= (that (forall (n) PHI)) (not (exists (n) (not PHI ))) )
In addition, as stated above, the IKL semantics ensures that for any names n and m, and any sentence PHI containing a free occurrence of n which does not occur in the scope of any quantifier which binds m,
(= (that (forall (n) PHI)) (that (forall (m) PHI[n/m] )) )
must be true, where PHI[n/m] is the sentence obtained by substituting m for n in PHI. That is, expressed less formally, changing the bound variable name in a quantifier does not get you a different proposition. And, proposition names are referentially transparent, so that if
(= n m)
is true, then so must
(= (that PHI) (that PHI[n/m] ))
be true; so, of course, they are also propositionally equivalent, since
(forall (p q)(if (= p q)(=p= p q))).
John Sowa ( http://www.jfsowa.com/logic/proposit.htm ) shows that =p= (called 'f4' in that document) can be decided by transforming all sentences to a normal form and then comparing the resulting character strings, using a transformation that is at worst nlogn in the length of the sentence: it reduces sentences to the vocabulary (exists, not , and), removes duplications and puts atomic sentences and bound variables into an aribtrary but fixed lexical order. One important property is that equivalent propositions are always 'about the same things', i.e. if two sentences express equivalent propositions, then the set of things referred to by the names which occur free in the sentences are the same.
@@We don't yet have a truth predicate. One thing that does require a truth-predicate, or something equivalent, is to be able to say eg that everything that Joe believes is true, ie to relate propositions inside a context to assertions of truth. We can do this 'one at a time', but to quantify over them requires a truth-predicate. Question: is this needed? If so, we will probably have to make IKL propositional variables into a distinct sort in order to avoid paradoxes. This is ugly :-( but easy and likely to be quite manageable in practice for users, eg we can 'type' with a prefix, replacing (that p) with prop:p or maybe something like **p . Or we could just advise users to not do anything paradoxical, and leave it at that. I'm sure nobody has any strong views on this topic. @@
We have already seen examples of the boolean sentential connectives and the quantifiers. The full list of IKL connectives is:
not |
negation, takes a single argument |
and |
which can have any number of arguments, including zero: (and)can be used as the truth-value true. |
or |
similarly: (or) is the truth-value false. |
if |
implication, takes precisely two arguments. This is called implies in CLIF, written '=>' in KIF. |
iff |
biconditional, takes precisely two arguments. Written '<=>' in KIF. |
Note a possible source of misunderstanding: many of these can be naturally read as though they were written as infixes, so that for example (and A B C) can be read as A and B and C, but this heuristic reading is misleading for implication, since (if A B) means if A, then B, but when naively rendered as an infix, it means the opposite: A if B is the natural rendering of if B, then A. One way to guard against this is to think of the implication syntax as an abbreviation for if...then: (if A [then] B). Another way is to remember that the direction of the implication is always from left to right, so that (if A B) means that A implies B. The old KIF symbol makes this vividly clear. (This symbol was abandoned in CL because in XML-compliant text it looks like this: =>)
IKL has two basic quantifier forms, exists and forall, but each can be elaborated in various ways. The basic quantifier form consists of a quantifier label, a list of bound names, and a body which is a sentence. Any of the names may be restricted, by enclosing it followed by a term (usually a simple name), which is understood as identifying a class or category, as in:
(forall ((x isHuman)) (exists ((y Car))(Owns x y)))
Restrictions must be applied to variables singly, and are optional. This is legal:
(forall ((x isHuman) (y isHuman) z (u isAnimal)) ...
but this is not:
***WRONG*** (forall ((x y isHuman)) ...
Restrictions are often 'class names' , but an arbitrary term may be used:
(forall ((x y (ClassType time))) ...
Note that this is equivalent to (forall (x y)(if ((ClassType time) x)... , not
***WRONG*** (forall (x y)(if (ClassType time x)...
Names in a classifying term may be bound by an outer quantifier, but not by the same quantifier that binds the names they are classifying:
***WRONG*** (forall ((x (foo x))) ...
Numerical quantifiers are indicated by a non-zero numeral immediately following the quantifier:
(forall ((x isHuman))(exists 10 (y) (and (Toe y) (PartOf y x)) ))
Zero is excluded because (exists 0 (y) ... amounts to (not (exists (y)... .
Numerical quantifiers can bind only a single variable. This is not legal:
***WRONG*** (exists 3 (x y) ...
(it would not have a well-defined meaning in any case: are there 3 <x,y> pairs, or 9?) But the variable can be restricted, so this is OK:
(forall ((x isHuman)(exists 10 ((y Finger))(PartOf y x)))
Notice that this does not assert that humans have only ten parts: the numerical quantification applies only 'within' the restriction.
If a term other than a numeral appears in the position immediately following the quantifier, then it is understood to be a name denoting a nonzero natural number. Users are cautioned that some reasoners may not be able to make complete use of such expressions. For examples see the IKL translations of description-logic cardinality constraints, below.
@@Note this also differs from CLIF syntax, where this would have been a guard. Numerical variables in quantifiers are too useful to pre-empt, eg check out the new transcriptions of the DL cardinalities below. Ive left guards out of IKL, but we can invent a special syntax for them if/when they are needed, eg (forall (ikl:guard p)(x) ...) @@
IKL, following KIF, allows a special name which allows a single sentence to stand for an infinite number of cases, called a sequence name. A sentence containing a sequence name stands for an infinite number of normal IKL sentences, each obtained by replacing the sequence name by a finite sequence of names. If the name is bound by a universal quantifier, the sentence is logically equivalent to the infinite conjunction of all such sequence-substitutions. This is typically used to represent a schematic pattern of assertions which apply when a function or relation can take any number of arguments. For example, the earlier definition of 'Predicative' can be generalized to cover relations with any number of arguments:
(forall (r)(if
(Predicative r)
(forall (x y ...)(iff (r x y ...)(and (r x)(r y ...)) ))
))
Here the sequence variable '...' is used: in the (rare) cases where one needs several sequence variables they may be any string beginning '...'. This axiom scheme stands for the infinite set of axioms
(forall (r)(if
(Predicative r)
(forall (x y)(iff (r x y)(and (r x)(r y)) ))
))
(forall (r)(if
(Predicative r)
(forall(x y x1)(iff (r x y x1)(and (r x)(r y x1)) ))
)))
(forall (r)(if
(Predicative r)
(forall (x y x1 x2)(iff (r x y x1 x2)(and (r x)(r y x1 x2)) ))
)))
...
and so on, an infinite sequence of such axioms.
Suppose now we assert (Predicative F) and (F a1 a2 ... an); the n-th axiom in this sequence allows us to conclude that (F a1 a2 ... an) iff (and (F a1)(F a2 ... an)); the previous axiom in the sequence allows us to conclude that (F a2 ... an) iff (and (F a2)(F a3 ... an)); and so on, until the first axiom , for the case where the sequence is empty, allows to conclude (F an-1 an) iff (and (F an-1)(F an)). Putting all this together and simplifying, we can conclude that the original assertion (F a1 a2 ... an) is equivalent to the conjunction (and (F a1)(F a2)... (F an)).
Since the use of a bound sequence name implies an infinite set of sentences, expressions containing bound sequence names should not be posed as goals to be proved, or as queries. A logic in which this is permitted would not be compact, and hence not first-order. While it is possible to state a natural deduction system for such a logic, it is unlikely that IKRIS applications will have mechanical reasoners available which could handle such queries. Bound sequence names should therefore be restricted to axioms.
As the above example illustrates, the appropriate use of a bound sequence name has the same effect as a tail-recursion on the argument sequence, by providing each case of the recursion as a separate instance of the axiom. As with any recursive or inductive definition, it is important to get the base or 'zero' case correct. In this example the recursion terminates naturally, but other examples of the technique require a little more care. Take for example the convention, used in OWL and elsewhere, by which a relation with more than two arguments is encoded as a binary relation between its first argument and a list of the remaining arguments. In IKL we can describe lists as a general-purpose function which takes any sequence of arguments and has the list as value:
(forall (...) (isList (list ...)))
and the convention can then be described directly:
(forall (r x ...)(iff (r x ...) (r x (list ...)) ))
This is so useful, in fact, that list and isList are considered to be reserved vocabulary in IKL.
The RDF language family follows several database-oriented systems in ony allowing binary relations as native forms, and encoding higher arities as properties of lists. We can describe a similar convention in IKL, by defining a category of relations which are 'listable':
(forall (r ...)(if (ListableRelation r)(iff (r ...)(r (list ...)) )))
(The initial 'if' here is deliberate: a biconditional 'iff' would not be correct.) It seems useful to allow this to take any number of arguments:
(Predicative ListableRelation)
Using sequence variables we can go further and write axioms for list itself, essentially defining lists in terms of some simpler (usually binary) construct. Various possibilities arise here. The LISP encoding of lists as S-expressions can be defined by these axioms:
(= (list) nil)
(forall (x ...) (= (list x ...)(cons x (list ...)) ))
(forall (x y)(and (= (car (cons x y)) x)) (= (cdr (cons x y)) y) ))
while the RDF collection vocabulary [RDF] for describing lists can be defined by these:
(= (list) rdf:nil)
(forall (x ...) (and
(rdf:first (list x ...) x)
(rdf:next (list x ...) (list ...))
))
In all these examples the pattern should be clear: the case of a variable-plus-a-sequence, i.e. in effect a sequence of length (n+1), is defined to be equal, or equivalent, to a suitable combination of the case for the variable alone (or, as it may be, for two or more consecutive variables) and the 'recursive' case for the sequence alone, i.e. of length n (or n-1, etc.); and a suitable terminating axiom must usually be provided for the case of the empty sequence. The technique will be familiar to anyone who has programmed in a language with recursion.
Other examples of sequence variable use include :
(forall (r x)((chain r) x)))
(forall (r x y ...)(iff ((chain r) x y ...)(and (r x y)((chain r) y ...)) ))
(notice the 'trivial' terminating case) allowing one to write, for example,
(= ascendingOrder (chain lessThan))
and hence infer
(ascendingOrder 2 5 7 13 144)
One can similarly define an elastic equality:
(forall (x)(allEq x))
(forall (x y)(iff (allEq x y ...)(and (= x y) (allEq y ...)) ))
so that (allEq a b c d e) abbreviates four equations. Even more usefully, an elastic inequality abbreviates o(n|2) negated equations. This involves a double recursion, done here by usng an auxiliary definition:
(forall (x y ...) (iff (diffFromAll x y ...)(and (not (= x y))(diffFromAll x ...)) ))
(forall (x)(diffFromAll x))
(forall (x y ...)(iff (allDiff x y ...)(and (diffFromAll x y ...)(allDiff y ...)) ))
(forall (x)(allDiff x))
Then (allDiff a b c d) is equivalent to
(and
(not (= a b))(not (= a c))(not (= a d))
(not (= b c))(not (= b d))
(not (= c d))
)
@@ More examples here: coding multiple quantifiers; nth-argument. @@
@@Do we want an XML top-level syntax to wrap the CLIF-style syntax in? Advantages include ability to attach metadata to text as properties. Any comments? Pros and cons?? Any XML mavens want to draft one??? (The preceding is an example of a direct request for feedback/comment.) @@
Any IKL expression may be given an attached comment by using a comment wrapper, which is an expression of the form
(comment <comment> <body>)
which has the same syntactic category and logical meaning as <body>. That is, comments are logically transparent. The comment may be either a quoted string or a single name (this allows the use of either single or double quotes.) The body may be any expression, from a single name to an entire sentence, and may itself be commented, so that comment wrappers may be nested. For example, this is a legal IKL sentence
(comment "<revision date=\"9/04/2005\"> date=\"8/21/2005\" </revision>"
(comment 'author="Pat Hayes" date="8/21/1944"'
(isFather (comment 'An expatriate Irishman' AlexanderHayes) PatrickHayes)
))
which is logically identical to
(isFather AlexanderHayes PatrickHayes)
Note that the outer comment in this example is a name enclosed in double quotes, requiring the double quotes used inside it to be escaped with a preceding backslash.
Comments may also be encoded as values of the comment property in an XML item, for details see @@@
The topmost level of IKL is text. An IKL text is a sequence of IKL sentences, bare comments or importations. (Although the ordering of elements of a text has no logical meaning, it should be preserved because it may have extralogical meaning.) A bare comment is a comment without a body, and an importation is an expression of the form
(import <name>+ )
where the names are network identifiers, i.e. names which can be used to identify and retrieve IKL text from some network source. Exactly what counts as a network identifier depends on the network conventions in use: on the Web, these would be URIs with prefixes identifying Web transfer protocols such as FTP, HTTP or HTTPS. The intended meaning of an importation is that it re-asserts the named texts inside the importing text, just as though they had been copied into place there. Notice that this means that the vocabulary of the importing text includes that of the imported text, even when it is not used explicitly in the expressions occurring there. This means that the space of propositions, for example, may be larger than one would suppose. We anticipate that importations will be used to access 'standard packages' which define useful vocabularies for various purposes, with their defining axioms.
In order for this to be useful, of course, it must be possible to assign an identifier to a text, and we allow this by including the identifier name as an option into the syntax, which then reads:
<text> ::= (text <name>? (<sentence>|<comment>|<importation>)* )
IKL texts are intend to be rigidly identified by their attached names. Texts are syntactic entities which do not change, and have no state. (To represent a 'dynamic' text, use the related notion of an information resource, described below.) Importing is transitive and idempotent, so the importation of a text imports all texts which it imports, and loops are harmless.
The result of importing a name which does not identify any IKL text is defined to be a non-op, i.e. it has no influence on the meaning of the importing text, like a bare comment. However, applications may treat this condition as an error.
@@The following extension to the CL spec was added here to satisfy a request. Chris W., is this what you wanted? (Another direct request for feedback/comment. ) @@
An IKL information resource is a network entity which acts as a Web resource in the sense used in [REST], i.e. as a time-dependent source of IKL texts. Information resources may have network identifiers and may be imported, but the result of such an importing is dependent on the state of the network, and may change between successive 'calls' of the importing. This means that the meaning of a text which imports an information resource cannot be specified logically or axiomaticaly, so no syntactic provision is made for defining the content of an information resource.
Description logics provide a repertoire of operations which can be used to define new classes in terms of other classes and properties, both of which correspond to IKL relations. The meanings of these operations can be defined in terms of simple first-order axioms in well-known ways, which can of course be written in IKL. In addition, however, the syntactic flexibility of IKL allows the operators to be axiomatized directly as functions from relations to relations. To illustrate, we give transliterations of the main constructions of the semantic web description logic OWL-DL. (Note, this is not claimed to fully capture the OWL-DL specifications, which require a great deal of attention to such details as distinguishing between datatype values and other entities. A more exact translation of semantic web languages into IKL is given in [SW2CL http://www.ihmc.us/users/phayes/CL/SW2SCL.html http://purl.oclc.org/net/ikl/docs/SW2CL])
The awkwardly named owl:intersectionOf is simply conjunction applied to classes, i.e. unary relations, so a better name for it would be AND. The axiom for AND must use sequence variables to capture the fact that intersection can be applied to any number of classes, including zero:
(forall (x) ((AND) x) )
(forall (c y ...)(iff
((AND c ...) y)
(and (c y)((AND ...) y)
)))
Similarly, owl:unionOf is OR:
(forall (x)(not ((OR) x)))
(forall (c y ...)(iff
((OR c ...) y)
(or (c y)((OR ...) y))
))
Notice the null case: it takes a little care to get these right. (AND) is the universal class, i.e. the universally true predicate, corresponding to owl:Thing (although with a somewhat wider scope in IKL than in OWL-DL) and (OR) is the universally false predicate, the empty class. Notice that if we assert that AND and OR are ListableRelations:
(ListableRelation AND OR)
then we get the equivalence of (AND a b ... ) with (AND(list a b ...)), corresponding exactly to the OWL use of RDF lists to attach arguments to owl:intersectionOf and, similarly, owl:unionOf.
Similarly, owl:complementOf is NOT:
(forall (c y)(iff ((NOT c) y)(not (c y)) ))
In fact, we can mirror all the connectives as similarly named operations on classes, for example
***???*** (forall (c d z)(iff ((IF c d) z)(if (c z)(d z)) ))
although in OWL this particular pattern is described as a relation owl:subClassOf between classes, rather than as a function on relations. Cyc uses 'genls' for this relationship:
(forall (c d z)(iff (SUBCLASS c d)(if (c z)(d z)) ))
The similar OWL term for IFF, whose defining axiom is left as an exercise for the reader, is owl:sameClassAs.
Description logic restrictions can be similarly seen as packaged pieces of quantifier and connective usage. For example, owl:allValuesFrom can be rendered as the operator ALLARE, which takes a binary and a unary relation to a unary relation:
(forall (p c z)(iff ((ALLARE p c) z)(forall (u)(if (p z u)(c u)) ))
For example, (ALLARE BrotherOf Canadian) is a predicate which is true of things all of whose brothers are Canadian. (To illustrate the potential pitfalls of description logic reasoning, this includes cauliflowers, integers and very short pieces of string.) The related OWL construct owl:someValuesFrom corresponds to this:
(forall (p c z)(iff ((SOMEARE p c) z)(exists (u)(and (p z u)(c u)) ))
These can then be used to construct quite elaborate expressions corresponding to DL class definitions, such as this example taken from the OWL wine ontology [Wine]:
(= WhiteNonSweetWine (AND WhiteWine (ALLARE hasSugar (OR Dry OffDry))))
Another useful DL construct is the explicitly listed class, owl:oneOf. This is best represented in IKL using a membership operator on an explicit list:
(forall (x y)(iff (member x (list y ...))(or (= x y)(member x (list ...))) ))
(forall (x)(not (member x (list))))
(forall (x (L isList))(iff ((ONEOF L) x)(member x L)))
Finally, DLs provide cardinality restrictions, which can be used to define things like people who have two children and have visited Paris more than once. These operators can be axiomatized in IKL by using numerical quantifiers and one simple arithmetic relation. (With more effort, they can be axiomatized without using numerical quantifiers: see [SW2CL] for details.)
(forall (p x (n ikl:number))(iff
((ATLEAST n p) x)
(exists ((m ikl:number)) (and
(ikl:lesseq n m)
(exists m (y)(p x y))
))
))
(forall (p x (n ikl:number))(iff
((ATMOST n p) x)
(exists ((m ikl:number)) (and
(ikl:lesseq m n)
(exists m (y)(p x y))
))
))
(forall (p x (n ikl:number))(iff
((EXACTLY n p) x)
(exists n (y)(p x y))
))
The property mentioned above could then (assuming a suitable basic vocabulary) be described by a single term::
(AND (EXACTLY 2 hasChild)
(ATLEAST 2 (AND isTravelEvent (ALLARE mainDestination (ONEOF (list Paris)))))
)
All the rest of the OWL vocabulary can be straightforwardly transcribed into IKL: full details are in [SW2CL].
Description languages often use pre-defined datatypes to distinguish constant values of various categories. This can be reproduced in IKL in various ways, but one way is recommended, in which the datatype name plays three roles: as a predicate, to mark lexical welformedness, as a function on strings, and as an identifier. We will illustrate this with the primitive datatypes from the XML Schema datatype specification.
A datatype is thought of as a function, called the lexical-to-value mapping, from a set of character strings, called lexical forms, to a value space. When the datatype name is used as a function name, it denotes the lexical-to-value mapping function: when used as a class name, it indicates the value space. In IKL all functions are total, so a datatype mapping has a value even when applied to a character string (or indeed anything) which is not in its domain. By convention, we require that in this case the value of the datatype function is not in the value space. Thus for example the string 'abc' is not a numeral, so (xsd:number 'abc') is not an integer, so (xsd:number (xsd:number 'abc')) is false; similarly, (xsd:number (xsd:number x)) is false if x denotes anything other than a character string.
As noted, IKL has special syntax for numerals and character strings, both of which can be regarded as built-in datatypes. IKL uses the reserved names ikl:number and ikl:string as the names for these datatypes. Thus, (ikl:number 346) and (ikl:string '346') are true with any numeral replacing 346 and any quoted string replacing '346'. If we define
(forall ((x ikl:datatype) (s ikl:string))(iff (LegalStringOf x s)(x (x s))))
then LegalStringOf is the relationship between a datatype and its legal lexical forms. Lexical forms are always character strings:
(forall (x (d ikl:datatype))(if (d (d x)) (ikl:string x))
One can think of a datatype D as a name with three roles – a function on strings, a predicate on values and a network identifier – whose meaning is determined by two infinite but R.E. sets of axioms which determine, for any character string s, either (D (D s)) or (not (D (D s))); and for each pair of strings s1 and s2 with (D (D s1)) and (D (D s2)), either (= (D s1)(D s2)) or (not (= (D s1)(D s2))). Certain datatypes may provide other extra information also, e.g. the integers in IKL are ordered by ikl:lesseq.
Datatypes are first-class entities in IKL, so can be quantified over, have properties, etc.. For example, one might reasonably assert any of the following:
(= ikl:number xsd:number)
(forall ((x ikl:string))(and (= x (ikl:string x))(= x (xsd:string x)) ))
(forall ((d ikl:datatype) x)(if (d (d x))(ikl:string x) ))
(forall ((d ikl:datatype))(Predicative d) )
The last, in particular, allows one to classify a whole list of things using a single atomic assertion.
As noted, IKL sentences in IKL text are understood as timeless assertions made outside of any particular context. To support the common use of contextual or temporal assertions, understood as being true 'in' a context or 'at' a time, IKL users should treat such sentences as propositions which are asserted to be suitably related to entities such as time-intervals or contexts, and write suitable axioms using propositional terms of the form (that <sentence>) rather than simply <sentence>. IKL imposes no logical constraints on entities such as time-intervals or contexts, nor on the nature or number of the relations which can hold between them and propositions.
Common examples of such relations include ist, a relation between a context and a proposition whose intuitive reading is "is true throughout"; holds, a similar relation between a temporal proposition and a time-interval, and occurs, a relation between (a proposition understood as describing) an action and the interval which exactly contains the action. As with most axiom-writing, IKL can support a large variety of possibilities, so the examples below should be taken as illustrative rather than normative.
[Makarios] distinguishes various cases of how ist might distribute over propositional structure. One way to describe this in IKL would be to use several ist relations, but another is to classify types of context by how they support distribution. (We will state this only for the binary case of conjunction and disjunction, for simplicity: it is easy to show as a meta-theorem that it also follows for the general case.)
(forall (c) (iff
(ContextAndDistr c)
(forall (p q)(iff
(ist c (that (and p q)))
(and (ist c (that p)) (ist c (that q)))
))
))
(forall (c) (iff
(ContextOrDistr c)
(forall (p q)(iff
(ist c (that (or p q)))
(or (ist c (that p)) (ist c (that q)))
))
))
(forall (c) (iff
(ContextNotDistr c)
(forall (p)(iff
(ist c (that (not p)))
(not (ist c (that p)))
))
))
The usual convention for holds is that it applies only to atomic sentences. There is no way to easily represent this restriction explicitly in IKL, but the same effect is obtained by allowing holds to distribute freely over the connectives:
(forall ((i timeinterval) p q) (and
(iff (holds i (that (and p q)))(and (holds i (that p))(holds i (that q))))
(iff (holds i (that (or p q)))(or (holds i (that p))(holds i (that q))))
(iff (holds i (that (not p)))(not (holds i (that p))
))
Other properties of these relationships can be established by suitable axioms, e.g. that holds is preserved over sub-time-intervals:
(forall ((i timeinterval)(j timeinterval) p) (if
(and (holds i (that p))(subintervalOf j i))
(holds j (that p))
))
When describing contexts involving possible re-interpretations of textual meaning, such as subjective reports of beliefs or overheard conversations, it is important to bear in mind that in IKL names are not re-interpreted in different contexts. A name in IKL text refers to the same 'real' thing wherever it occurs in the text, even inside a proposition name that is being used to represent someone's false beliefs, and even when those false beliefs involve the name itself. If one reads such contextual assertions in the commonly used de dicto way, which is often done, the results can seem unintuitive. To illustrate with a familiar fictional example, Lois Lane knows one person by the names 'Clark Kent' and 'Superman', but believes, wrongly, that these names refer to two different people. We say, informally, Lois doesn't know that Clark is Superman, and it is tempting to render this into IKL by positing a belief-context for Lois in which Clark is not Superman. To do this in IKL, however, requires care over reference. It would be a mistake to assert this:
***WRONG*** (ist LoisBelief (that (not (= Clark Superman)))) ***
since it would follow from this, and the fact (= Clark Superman) that
(ist LoisBelief (that (not (= Clark Clark))))
and Lois is not that confused.
The first claim seems reasonable because if one were to ask Lois, is it true that Clark is different from Superman?, she would say, yes: so, one feels, she believes it, surely. The IKL view, however, is that she would assent to it not because she believes what it actually says (that someone is not identical to himself), but because she is confused about what it says, and so is in fact agreeing to a different proposition, which could be expressed in IKL as
(that (not (=
(entity-believed-by-Lois-to-be-called 'Clark')
(entity-believed-by-Lois-to-be-called 'Superman')
)))
which, note, does not use 'Clark' and 'Superman' as logical names. Put another way, in order to adequately describe Lois' confusion, we have to speak explicitly about what she thinks (wrongly) that the names refer to: and to do that, we cannot simply use the names as names – which would get to the real referents, not Lois' confused notions of what the referents are – but must take a step back away from the actual referents, talk about the names as character strings, and refer to what these strings might denote if the world were really the way that Lois believes it to be.
This suggests a strategy for handling such opaque belief contexts in a referentially transparent logic such as IKL: when a name, when used in some contextual assertion, might refer there to anything other than what it refers to in the actual logical text, the safe strategy is to treat the name as a character string (thereby removing its logical association with its actual referent) and replace uses of the name with a literal term in which the context is used similarly to a datatype, applied to the name string. Such a term can be thought of exactly as a kind of literal, with the context playing the role of a datatype, i.e. as a function on lexical strings which maps them to referents in a fixed way (in this case, determined by the context). We will refer to this as contextual typing or contextual reference. Lois's state of mind can then be described thus:
(ist LoisBelief (that (not (= (LoisBelief 'Clark')(LoisBelief 'Superman')))))
or, assuming that she really does know who Clark Kent, her office colleague, is:
(ist LoisBelief (that (not (= Clark (LoisBelief 'Superman')))))
Although contextual typing imposes a notational burden when writing axioms describing opaque contexts (which are usually related to states of belief in some way), it yields several compensatory benefits. The referential transparency of the overall language simplifies the logic and leads to more coherent reasoning, since equality reasoning can be used throughout all contexts; moreover, these context-reference terms are meaningful outside of their original context, and can be used directly to refer to the (possibly imaginary) entity that Lois believes Superman to be. This enables one to say, for example
(taller (LoisBelief 'Superman') Superman)
One can say Lois knows who Clark is by a simple equation:
(= Clark (LoisBelief 'Clark'))
which is the assumption which justified our re-writing the sentence above.
A similar strategy can be applied to temporal reference, if required. (This is a large topic, here only brief reviewed.) Consider Arthur, a growing boy, and the assertion that he is taller now, in September of 2005, than he was the same time last year in 2004. Such changing facts about an individual, or facts about a changing individual, can be rendered as contextual assertions of time-dependent propositions about Arthur, using holds, or can be stated in terms of 'fluents', a term introduced by McCarthy [SACL] to refer to a relation between things and times, or by using a simple non-temporal relation between temporal 'slices' of Arthur (or, if one prefers this way of talking, of Arthur's lifetime). The latter is similar in spirit to the contextual-reference device described above in that it is the reference to Arthur that is made time-relative, rather than the relation itself, or the assertion of its application to Arthur.
The three styles can be illustrated thus, using a suitable XML schema literal to denote time-intervals, each of a single 24-hour day. The first relativizes propositions to intervals, using holds and that (one could also use ist, as above, provided that intervals are regarded as a type of context):
(exists (x y)(and
(holds (xsd:date '2004-09-01') (that (= (height Arthur) x)))
(holds (xsd:date '2005-09-01') (that (= (height Arthur) y)))
(less x y)
))
Note that the temporal relativity here is on the proposition, and we are obliged to quantify into it in order to refer to the things it mentions. An accurate English rendering might be: The height that it was true in 2004 that Arthur was, is less than the height it is true in 2005 that he is.
The second uses fluents, by putting the time-interval as an extra argument to the relation, by common convention the last:
(exists (x y)(and
(= (height Arthur (xsd:date '2004-09-01')) x)
(= (height Arthur (xsd:date '2005-09-01')) y)
(less x y)
))
Note that contextual assertions are no longer required, and this does not use explicit refernces to propositions. In English, roughly: Arthur's height in 2004 is less than Arthur's height in 2005. (The lack of tense in this English rendering is deliberate.)
The third uses temporally qualified references to refer to Arthur at different times. In this case we can dispense with the quantifiers:
(less
(height (during (xsd:date '2004-09-01') Arthur))
(height (during (xsd:date '2005-09-01') Arthur))
)
The 'during' here plays only a dummy role, in fact, and we could eliminate it and use the date directly as the 'time-slicing' function. The resulting convention is similar to that used earlier for contextual reference, where a context name (here, a term denoting a time-interval) is used to indicate a function which indicates a temporally sensitive reference to its argument:
(less
(height ((xsd:date '2004-09-01')Arthur))
(height ((xsd:date '2005-09-01')Arthur))
)
and an English rendering might be: Arthur in 2004 is less high than Arthur in 2005.
This last is, as noted above, similar to the technique used for describing Lois' beliefs. It differs however in using the name itself rather than a term constructed from the quoted name. This is appropriate for simple temporal slicing since the plain name Arthur refers to a 'continuant', i.e. something which retains its identity through time, so there is no need to make special accomodation here for the possibility that the name means differnt things at different times. If we were to use a name like PresidentOfTheUSA, intending that to refer to different people when used at different times, then issues of temporal identity would have to be dealt with more explicitly. The 'datatyped' technique used for the earlier Superman example, where a simple name is replaced by a term built from the quoted name, is robust enough to handle any kind of identity condition, but more awkward to axiomatize.
The merits (or otherwise) of these various axiomatic styles, and their relationship to various philosophical views on existence and time, have been extensively debated elswhere. Our main point here is that IKL is ecumenical enough to use them all, and even to state conditions under which they are equivalent :
(forall ((t timeInterval)(r temporallySliceableFunction)(x continuant)(z continuant))
(iff (holds t (that (= (r x) z))) (= (r x t) z)
))
(forall ((t timeInterval)(r temporallySliceableFunction)(x continuant))
(= (r x t)(r (during t x)))
))
Both of the above are examples of a general technique for referring to an 'aspect' of a thing, which we tentatively call viewing.
The general case is that one has an entity which can be identified as extending through a variety of partial or complete 'worlds'. These worlds might be contexts, time-intervals, possible worlds, mental perspectives, points of view, etc.., and different philosophical terms are typically used in the various cases: but the logical point is, that one wishes to identify a single thing across a variety of such 'worlds', while allowing for this one single thing to have different properties in those different worlds. The viewing technique, then is to consider the 'world' as defining a viewing function from the entity to those parts or aspects of it which give it an identity in that world, ignoring any other aspects or parts. If we think of entities as being some kind of whole or sum of all their aspects in every world, then this function can be viewed as a kind of selector, which filters out aspects which do not belong in the world in question, leaving a kind of reduced entity to which properties and relations can be attributed without having these attributions contaminated or confused by other aspects of the entity which arise only in other perspectives.
The most appropriate way to describe this in less abstract language depends on the particular kind of 'world' and 'entity' one is talking about. Thus, for worlds defined by times, it is usual to distinguish event-like occurrents – which can be said to have temporal parts, so the time-interval worlds simply contain the contemporary parts – from object-like continuants, which go on from day to day, getting a little older but retaining their essential identity, and are not thought of as having temporal parts. Nevertheless, we can clearly distinguish a continuant at one time from the same continuant at a different time, even though these are not thought of as temporal parts of the continuant: the logical/representational technique applies to continuants and occurrents with equal correctness, since both of them can have temporally changing properties. As the Superman example illustrates, the view need not be temporal in nature: it hardly seems appropriate to call Lois' view of Superman a part of Superman in any mereological sense. Nevertheless, it is possible to think of the name "Superman" as attached to a kind of informational complex which includes Lois' distorted view of reality, and which therefore has an imaginary entity, a kind of ur-Superman doppelganger, as a part or aspect of it. (We might perhaps identify this informational complex with the set of all relations in which Superman takes part, since it is a genuine fact about Superman, the real guy, that Lois believes, of him, that he is not Clark Kent.)
The use of a viewing technique raises the obvious question of what it means to simply assert something about an object simpliciter, with no reference to a view. Again, the answer seems to depend upon circumstances. For temporal views, it seems natural to assume that a bare assertion applies to all possible views, i.e. it is true of the entity regardless of when it is viewed:
(forall (r x (t isTimeInterval))(if (r x) (r (t x)))
Such properties seem to include essential or 'rigid' properties [ref OntoClean] , i.e. properties which cannot be rendered false of a thing without it ceasing to exist or to lose its identity, such as being in a certain basic ontological category, e.g. being human. In fact, we might define a rigid property as one which, if it applies to any temporal view of anything, must apply to the thing directly (and hence to all other temporal view):
(forall (r)(iff
(RigidProperty r)
(forall (x)(if (exists ((t isTimeInterval))(r (t x)))(r x) ))
))
Note, this must be restricted to temporal viewing, since there could be someone who thinks that "Superman" refers to a vegetable (http://www.saturdaymarket.com/kiwi1.htm).
@@ Quantifiers very broad, use of local restrictions and guards: need to get recursions right: contexts and holdings; importing of standardized packages; publishing useful packages.
No truth-function: limitations.
Coding alternatives with triggers (Jerry); coding restrictions as bullets, eg with Ab., eg of deontic actions/events for business rules.
Handling sorts. Sortal organization vocabulary.
Handling arities, other structural constraints. Structural vocabulary? Needs some ideas on handling orthogonal contexts/namespaces.
Richard's examples, Cyc versions of OWL primitives. @@
IKL reserved and built-in vocabulary listing, and useful axioms.
ikl:string
ikl:number
ikl:datatype
ikl:lesseq
ikl:initialsubstring
ikl:distinct
ALLARE
SOMEARE
ATMOST
ATLEAST
EXACTLY
SAME
DIFFERENT
holds
ist
during
list
isList
CL
ISO-CL
KIF
Makarios
OntoClean
OWL
RDF
RDFS
SACL
SW2CL
Wine
XSD