[CL] Re: Some comments on future directions

[John F. Sowa]

Enrico,

You mentioned Kripke semantics in order to point
out that different logics require very different
model theories.  But I pointed out that with Dunn's
semantics, you can use a single model theory for
a very wide range of what you and many other people
call "different logics".

EF> I don't care about Kripke vs FO semantics. But I
 > do care about the properties of the relational
 > structure in the semantics of your logic (any: CL,
 > modal, FOL, DL, etc) you use to model the world.

I wasn't suggesting pure first-order semantics as a
replacement for Kripke semantics.  I was recommending
Dunn's semantics, which uses two levels of FOL:
pure FOL at the object level, and pure FOL at the
metalevel for axiomatizing the object level.

I believe that Dunn's semantics provides what
you are asking for with a much simpler and more
general structure.

EF> If, on the other hand, you want to axiomatise the
 > structures in your logic, you have to *prove* that
 > the axiomatisation is sound and complete wrt the
 > original specific algebraic specification, and that
 > this axiomatisation is possible at all.

JS> No.

EF> Yes! I don't understand why not. This is a true
 > point of disagreement; see below.

I'm sorry.  I should have clarified my point.  I agree
that soundness and completeness are important.  But
when I said "no", I meant that with Dunn's approach,
you don't have to prove it -- you get it for free.
The point is that all rules of inference are purely
first order.  Therefore, they're sound and complete.

EF> This is approach (a). In approach (b), I would have
 > the meaning of each mode or intentional verb builtin
 > in the semantics, no additional axiom, it is just
 > implicit in the meaning of its own dimension.

But changing from one logic to another whenever you
use a new verb is a very big jump.  With Dunn's
semantics, you have one system of logic, and you
add whatever axioms you need for only those verbs
that occur in your application.

That is essentially what you do with any ontology.
If you are talking about houses, you add axioms
for houses. If you are talking about flowers,
you add axioms for flowers.  But you don't have
to change your logic for every change of subject.

EF> Yes, but this axiomatisation has to be proved
 > correct, otherwise you are outside a logical
 > approach. Why do you say you don't want to make
 > such a proof for each added dimension?

The ontologist who adds axioms for any particular
subject matter -- whether it is houses, flowers,
or the verb "authorize" -- has the responsibility
of ensuring that those axioms are consistent and
true of the subject under discussion.  But that
is the responsibility of the ontologist, not
the responsibility of the logician who defines
the system of logic.

Dunn's semantics allows you to split the job:
one small group of logicians deines the logical
structure.  Then anybody who wants to axiomatize
any domain of knowledge can write axioms for the
ontology of that particular subject.

EF> Of course it is by no means trivial to prove
 > the soundness/completeness of a set of axioms.
 > It means to have first a semantics of the
 > original problem (i.e., the specialistic semantics
 > that approach (b) is considering), and then show
 > that the axiomatisation captures *exactly* such
 > semantic structure.

That's the weakness of approach (b), which forces
the logician to create a new logic for every domain.
But with approach (a), you only have one logic, whose
rules of inference are always sound and complete.
Then the ontologist who adds new axioms is only
responsible for ensuring that those axioms are
consistent with one another and true of the subject.

This approach makes the job simpler for everybody.
The logician is finished after defining the general-
purpose logic.  And the ontologist can prove consistency
by a very simple method:  select one model for which
the axioms are true.  That can be done by choosing the
most important or interesting model of some domain
first and writing axioms that are true of that model
(and perhaps some other similar models).  That method
guarantees that you have consistent axioms that are
true of at least the primary model of interest.

EF> Of course, with your approach (a) you then have
 > also to prove that your universal CL-based theorem
 > prover terminates its computation for each frangment
 > of logic which is known to be decidable with its own
 > semantics; otherwise, it is of no practical use.
 > Good luck.

I don't rely on luck.  I depend on a proper design.
By restricting all rules of inferece to FOL, I ensure
soundness and completeness.  Then I allow the people
who implement applications to choose whichever subset
of FOL is appropriate for their application.  For
some applications, that may be a DL logic.  For query
languages, it may be some SQL-like language.  For
computations, it may be some Horn-clause logic.

And there may be some applications for which full
FOL is required, and the implementers are willing
to turn on their theorem prover and let it run.
For some problems, it stops; and for others, it
doesn't.  But that is the choice of the implementers.
I can make suggestions and give them guidelines, but
they are adults who are capable of making their own
decisions for their applications.  I am not going to
treat them like babies who are not allowed to walk
outside the playpen.

John