SUO: A disclaimer about 'new KIF'
As I have referred in a number of messages to the 'new KIF' that is
going to be out soon and have several neat features, I ought to
explain that this is the product of an ad-hoc group with no
particular official status, and that although we have been in
consultation with Mike Genesereth, the author of the original KIF,
our ideas for a modified version have not yet been approved by him or
indeed by anyone else.
Pat Hayes
PS. That said, I should respond to something thatJohn Sowa said in a
recent message:
The language of core KIF is pure first-order. But we have been
talking about extending KIF to a sorted language, which can be
used as a metalanguage for arbitrary many metalevels. A sorted
first-order language can indeed support true HOL, if you allow
sorts that have uncountably many members.
Actually, sorted FOL/KIF has exactly the same expressive power as
unsorted FOL/KIF, and cannot support true HOL. Also, it seems that
the best way to understand the semantics of KIF (and certainly of the
'new KIF') is that it is in fact a small but significant extension of
pure first-order logic, in that some of its expressions are best
thought of as finite encodings of infinite expressions in the
infinitary logic Lw1w.
John goes on:
But in any case, defining all the terms of mathematics is
almost trivial in comparison to defining all the words of
English. ...
and I entirely agree.
---------------------------------------------------------------------
IHMC (850)434 8903 home
40 South Alcaniz St. (850)202 4416 office
Pensacola, FL 32501 (850)202 4440 fax
phayes@ai.uwf.edu
http://www.coginst.uwf.edu/~phayes