Re: languages and model theory (was KIF standardization)
On Mon, Jul 24, 2000 at 04:58:47PM -0700, pat hayes wrote:
> ...one has to face up to the fact (because it really is a fact) that
> it is in general provably impossible to *fully* capture the
> "intuitive" meaning.
>
> >This means that we specify some class of intendedstructures (e.g.
> >graphs, lattices, vector spaces) which are isomorphic to the
> >extensions of the predicates, functions, and constants in the
> >nonlogical lexicon.
>
> Well that is one way to proceed, but by no means the only way. I think
> it is often (usually?) a mistake to proceed by first doing a kind of
> pure-math modelling and then trying to axiomatize the mathematical
> model. Often the most salient facts one wants to have in the ontology
> have nothing to do with mathematically interesting structures, and
> vice versa.
Right, Pat, just so long as we don't ignore the cases that do.
Premature math modeling is probably ill-advised if one is working on an
ontology for a fairly concrete set of concepts -- liquids, say. ;-) But
for concepts that are somewhat more abstract and general -- process and
its kin, for instance -- then Michael's approach makes more sense, as
such concepts often have interesting, but perhaps initially somewhat
inchoate, structural properties that can be *clarified* via mathematical
models. If you'll excuse the presumption, I suspect that you had math
models aplenty in your head when you were writing up your catalog of
temporal theories!
> >The problem is that there are classes of such intended structures
> >that are not first-order definable. For example, the classes of
> >connected and planar graphs are not first-order definable, as well as
> >more famous examples from arithmetic. In such cases, we will need to
> >use a second-order language if we really want to completely
> >characterize the intended models.
>
> Sorry, in this case you are stuck. Just using a second-order
> *language* isnt going to rule out any models: to do that you need a
> classical second-order semantics,
I suspect Michael meant 2nd-order language + 2nd-order semantics.
> and while you can indeed claim to have such a semantics, there is no
> way your inference process will be able to give the claim any
> substance. There is NO mechanizable inference process which can
> restrict interpretations to classical second-order interpretations.
There's the rub. This is the point that always makes me wonder about
Fritz's advocacy of 2nd-order logic. From Cyc's point of view, this
point seems to make the 1st-order/2nd-order distinction moot. (No need
to respond, Fritz; perhaps we can resurrect this controversy in Austin
next week! :-)
> >IMHO, I believe that we should probably focus first on what the
> >nonlogical lexicon of the SUO should be, then specify the classes of
> >intended structures, and then use the language necessary to
> >completely axiomatize these classes of structures.
>
> IMHO, this program is doomed before it starts, since even the simplest
> mathematical structures have no RE theories.
True enough, but there are a number of interesting domains one might
model (again, processes spring to mind) whose intended structures don't
necessarily include any nonaxiomatizable mathematical substructures.
And even if they do, I think Michael's approach here might still be
worth considering if we just clobber the word "completely" (where
"complete" is taken in its formal logical sense). As you imply, most
interesting theories are incomplete anyway.
-chris
ps: I've been trying my darndest to help keep Mike U's blood pressure
down by posting only to the IEEE SUO list, but I notice that several
messages that seem quite relevant to that list (the exchange between
Michael and Pat, f'rinstance) are only going to the onto-std list, so
I've double posted this one. I haven't seen any activity on onto-std
that hasn't been relevant to the SUO list, so should we avoid the former
list altogether? Any guidelines here? Is anybody on onto-std who isn't
on SUO (but ought to be)?
--
Christopher Menzel # web: philebus.tamu.edu/~cmenzel
Philosophy, Texas A&M University # net: chris.menzel@tamu.edu
College Station, TX 77843-4237 # vox: (979) 845-8764