Difference between logics and theories

sowa@ranch.poly.edu (John F. Sowa)
Date: Sat, 10 Sep 94 13:46:02 -0400
From: sowa@ranch.poly.edu (John F. Sowa)
Message-id: <9409101746.AA03702@ranch.poly.edu>
To: cg@cs.umn.edu, interlingua@isi.edu, srkb@cs.umbc.edu
Subject: Difference between logics and theories
Cc: sowa@ranch.poly.edu
Sender: owner-srkb@cs.umbc.edu
Precedence: bulk

In my earlier reply to the discussion between Fritz Lehmann and
Pat Hayes about the CCAT (Conceptual Catalog), I was responding to
a point that may have been different from the one that Fritz and Pat
had in mind.  When they look at the CCAT ontology, they see lots of
labels like Know, Believe, Think, etc.  This immediately suggests
the kinds of things that people who are developing epistemic logics,
intensional logics, modal logics, etc., are talking about when they
develop model theories as a semantic basis for their logics.

When I respond that all I am providing in CGs (or in KIF) is a mechanism
for supporting very lightweight contexts -- just boxes that map into
KIF quotes -- people immediately ask where is my model theory for those
boxes.  Then I reply that it is just a first-order logic with a hierarchy
of metalanguages, all of which are also purely first order.  But then
they jump on my response and ask how I can say that I am supporting
all those labels like Know, Believe, Think, etc., with such a lightweight
model theory.

My answer, which I keep repeating again and again in various phrasings,
is that it's not my job.  It's the job of the people who are using the
CG and KIF languages to axiomatize their theories of belief, modality,
or whatever.  I see my job as providing the metalanguage in which they
can do that axiomatization.  It's up to the users of CGs or KIF (or the
ontologists who provide ontology packages for the end users) who have
to develop theories of belief, etc., to write their theories in the
language of KIF or CGs.

I believe that the confusion comes from the terms "epistemic logic"
vs. "epistemic theory".  Lots of people in AI and philosophy have been
developing "logics" where they incorporate intensional notions directly
in the language and its rules of inference.  With KIF and CGs, we are
providing empty boxes with a metalanguage in which you can develop a
theory of belief and axiomatize it.  The net result is that you can
do the same kinds of things that a "logic" does, but the responsibility
for developing a model theory lies with the user of KIF or CGs, not
with the people who are defining KIF and CGs.

I will certainly admit that we, as definers of KIF and CGs, have a
responsibility to demonstrate that our metalanguage is capable of
supporting a theory of truth, modality, or whatever.  But if anyone
writes inconsistent axioms in our formalism, it's not our fault.

In other words, if you get in trouble with your theory of truth,
we can just walk away, like Pontius Pilate, and say "What is truth?"
If you get crucified, it's not our problem.

John Sowa