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