**Mail folder:**Interlingua Mail**Next message:**schubert@cs.rochester.edu: "Re: Quoting and unquoting variables in KIF"**Previous message:**sowa: "Re: Contexts and quantifiers in KIF"**Reply:**schubert@cs.rochester.edu: "Re: Quoting and unquoting variables in KIF"

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