Re: INTERNATIONAL STANDARD FOR LOGIC: CSMF
sowa@turing.pacss.binghamton.edu (sowa)
Date: Sat, 10 Sep 94 14:41:56 EDT
From: sowa@turing.pacss.binghamton.edu (sowa)
Message-id: <9409101841.AA14429@turing.pacss.binghamton.edu >
To: cg@cs.umn.edu, fritz@rodin.wustl.edu, interlingua@ISI.EDU,
srkb@cs.umbc.edu
Subject: Re: INTERNATIONAL STANDARD FOR LOGIC: CSMF
Cc: E.Hunt@cgsmtp.comdt.uscg.mil, bhacker@nara.gov, duschka@cs.stanford.edu,
genesereth@cs.stanford.edu, jksharp@sandia.gov,
msingh@bcr.cc.bellcore.com, msmith@vax2.cstp.umkc.edu,
roger@ci.deere.com, scott@ontek.com, sharadg@atc.boeing.com,
skperez@mcimail.com, sowa@turing.pacss.binghamton.edu, tony@ontek.com,
zeleny@math.ucla.edu
Sender: owner-srkb@cs.umbc.edu
Precedence: bulk
Fritz,
If it will make you any happier, please be assured that we are
indeed "allowing" true higher-order logic within the KIF and CG
frameworks. As I have repeated many, many, many times, we are NOT
providing an FOL framework. We are providing an infinite hierarchy
of metalanguages, all of which have a first order structure.
In that structure, we can define new axioms for languages, including
any version of HOL that you please -- that includes TRUE HOL, with all
its works and pomps, including quantification over all subsets of any set.
All of the examples that you cited can indeed be handled.
I have shown how to do some of them. You can take it from there.
Meanwhile, I am trying to finish my book. I will include therein
many more examples, many more exercises, and answers to the more
interesting exercises in the back.
It will all become clear in due course.
John Sowa