Quoting and unquoting variables in KIF

sowa <sowa@turing.pacss.binghamton.edu>
Reply-To: cg@cs.umn.edu
Date: Sun, 11 Apr 93 18:06:24 EDT
From: sowa <sowa@turing.pacss.binghamton.edu>
Message-id: <9304112206.AA06224@turing.pacss.binghamton.edu>
To: schubert@cs.rochester.edu
Subject: Quoting and unquoting variables in KIF
Cc: cg@cs.umn.edu, interlingua@isi.edu, sowa@turing.pacss.binghamton.edu

Len,

I sympathize with your points.  The syntax ,(name ?x) is what
Mike told me to write in KIF.  His reasoning is roughly what I
summarized in my previous note, and it is strongly influenced by
the desire to allow KIF to be parsed by the Common Lisp reader.
Since KIF is a new language that will be processed by many systems
that are not using Lisp at all, I don't believe that is a strong
argument.  However, I will leave that issue to the KIF designers 
to decide.  My primary concern is to make sure that I can translatee
conceptual graphs to and from KIF in a fairly straightforward way.

Re propositions:  I define a proposition to be an equivalence class
of statements in one or more languages.  Given formal languages
L1 and L2, each with its own rules of inference and with mappings
Mij from Li to Lj, assume the following conditions on the mappings:

 1. Mij is defined for every statement in language Li, but it does
    not necessarily cover all of language Lj.

 2. Therefore, the concatenated mapping MijMji maps Li to a subset
    of Li.

 3. If a statement s in any language Li is mapped into any other
    language Lj and then back to Li, the result Mji(Mij(s)) is
    provably equivalent to s by the rules of inference of Li.

 4. If s in Li is mapped to Lj and back again, the collection of
    nonlogical predicates in s and Mji(Mij(s)) must be identical.

Conditions #1 and #2 ensure that any statement in any of the languages
can be mapped into any other and back again.  Condition #3 ensures that
if all the languages have sound rules of inference, then all the
mappings preserve truth.  Condition #4 ensures that you don't gain
or lose ontological content; i.e. you can't map "Every cow is a cow"
to another language and back again and get the statement
"Every unicorn is a unicorn", but you might get "No cow is not a cow."

Given such languages and mappings, I define two statements s and t
in L1 to be equivalent iff s=M21(M12(t)) or t=M21(M12(s)).  Observe
that this definition is indeed an equivalence relation, and therefore
it must divide L1 into equivalence classes; furthermore, the set of
equivalence classes of L1 is isomorphic to the equivalence classes of
L2.  Therefore, I define a proposition to be a pair (C1,C2) where
C1 is an equivalence class in L1 and C2 is the corresponding class
in L2.  This definition can be generalized to any number of languages
and mappings, although the definitions and theorems would be simplified
by the use of category theory (at least for those who know category theory).

I'm not completely satisfied with the four conditions on the mappings
Mij stated above, and it might be better to add another condition like
the following:

 5. If any language Li has definitional facilities, no symbol may be
    replaced by its definition in order to prove that two statements
    s and t in Li are provably equivalent.

This condition means that the statement "All unmarried men are unmarried"
would not be considered equivalent to "All bachelors are unmarried."
It also means that a person might know the definition of factorial
and know the rules of arithmetic without knowing that factorial(6)=720.
In other words, two statements express the same proposition only if
you can convert one to the other with "obvious" transformations 
and no appeal to definitions.

The point of this approach is that you should be able to talk about
two different languages (such as CGs and KIF) expressing the same
proposition without appeal to mental entities and without making
all tautologies and mathematical theorems collapse to a single
proposition T.

John Sowa