The vocabulary introduced in the preceding subsection allows us to encode properties of expressions in and of themselves. In this section, we add some vocabulary that allows us to change levels of denotation, i.e. to relate expressions about expressions with the expressions they denote.
The term (denotation ) denotes the object denoted by the object denoted by . A quotation denotes the quoted expression; the denotation of any other object is .
The term (name ) denotes the standard name for the object denoted by the term . The standard name for an expression is (quote ); the standard name for a non-expression is at the discretion of the user. (Note that there are only a countable number of terms in KIF, but there can be models with uncountable cardinality; consequently, it is not always possible for every object in the universe of discourse to have a unique name.)
The final level-crossing vocabulary item is the relation constant true. For example, we can say that a sentence of the form (=> (p ?x) (q ?x)) is true by writing the following sentence.
(true '(=> (p ?x) (q ?x)))
This may seem of limited utility, since we can just write the sentence denoted by the argument as a sentence in its own right. The advantage of the metanotation becomes clear when we need to quantify over sentences, as in the encoding of axiom schemas. For example, we can say that every sentence of the form (=> ) is true with the following sentence.
(=> (sentence ?p) (true `(=> ,?p ,?p)))
Semantically, we would like to say that a sentence of the form (true ') is true if and only if the sentence is true. In other words, for any interpretation and variable assignment, the truth value is the same as the truth value . In other words, for every truth function , true is our language's name for .
Unfortunately, this causes serious problems. Equating a truth function with the meaning it ascribes to true quickly leads to paradoxes. The English sentence ``This sentence is false.'' illustrates the paradox. We can write this sentence in KIF as shown below. The sentence, in effect, asserts its own negation.
(true (subst (name `(subst (name x) `x `(true ,x))) `x `(not (true (subst (name x) `x `(not (true ,x)))))))
For any truth function that maps true to itself, we get a contradiction. If of this sentence is , then by the rules for assignment of the logical operators contained in the sentence, we see that must make the sentence . If assigns the value , then, again by the rules for assignment of the logical operators, we see that it must assign it the value . In either case, we get a contradication.
Fortunately, we can circumvent such paradoxes by slightly modifying the definition of true. The treatment here follows that of Kripke, Gilmore, and Perlis. Although the approach is a little complicated, it is nice in that the intuitive interpretation of true is in all important cases exactly what we would guess, yet paradoxes are completely avoided.
(<=> (true ) )
Given a sentence , we define to be the sentence obtained from as follows. If the sentence is logical, then all occurrences of not are pushed inside other operators. If the sentence is (not (true )), the is (true (listof 'not )).
Since the truth of a sentence (true ) is determined by the truth value of , not , the potential for paradoxes is eliminated. For most sentences, and are the same. For apparently paradoxical sentences, the two differ and so no contradiction arises. (See Perlis for the description of a model for databases containing this axiom schema.)