Chris, (01)
I was talking about the many different ways of using a statement in
a logic, such as FOL. Theorem proving is only one use among many.
In fact, it is probably very far down the list of things one might
want to do with logic. For example, (02)
1. Communicate some information -- i.e., transmit an assertion. (03)
2. Check whether somebody's assertion is consistent with the
facts -- i.e., evaluate truth in terms of a specific model. (04)
3. Form a generalization from a list of assertions -- induction. (05)
4. Generate a hypothesis -- abduction. (06)
5. Form an analogy between two different statements. (07)
6. Check whether a given statement is true of all possible models
-- prove a theorem. (08)
Point #6 happens to be a very high priority among logicians who
think that the primary use of logic is to form the foundation
for mathematics. But the other uses are probably much more
important for most people. (09)
JFS>> The paternalistic approach assumes that all users are trying to
>> prove a theorem that is valid for all possible models. But most
>> people who ask a question are only interested in a specific model,
>> such as the current DB. (010)
CM> This isn't clear to me at all. If I'm just trying to describe
> a certain conceptual domain like, say, human physiology... (011)
First of all, physiology is an experimental science. In the
development of that science, the most important use for any kind
of precise notation (say ordinary language expressed in a way that
could be translated to FOL) is to state observations and form
generalizations. That is communication (#1 on the list above),
fact checking (#2), and induction (#3). (012)
CM> ... it doesn't seem to me that any inferencing is done vis-á-vis
> any sort of fixed finite model. (013)
I have no idea what kind of inferencing you are talking about.
Physiologists aren't the kind of people who state anything in
axioms. They are much more likely to be doing #1, #2, #3, #4,
and #5 above than #6. (014)
And as a matter of fact, physiologists do have a fixed finite
model. It's called the typical average human body, from which
they have derived their descriptions by induction. Those
descriptions are guaranteed to be consistent because they
have been verified on multiple models (usually cadavers). (015)
When they find descriptions that vary from one cadaver to the
next, they state the generalizations and mention the exceptions
in footnotes and/or case histories. They are very unlikely
to prove any kind of theorem more complex than instantiating
a general case to a specific instance. (016)
Even physicists state in a tone of derision that they "don't
do axioms" -- that is in response to things like von Neumann's
axioms of quantum mechanics. Philosophers of science may have
a high regard for von Neumann's axioms, but physicists do not
have a high regard for philosophers of science. (017)
CM> It's just done on the basis of the axioms of the ontology... (018)
The physicists and physiologists who say that they "don't
do axioms" would speak even more derisively about ontology.
However, one could claim that they do some rather simple
ontology at the level of identifying and classifying their
terms in a simple hierarchy. If you gave them full FOL,
they would never use more than a subset -- except perhaps
in asking a question about a database of cadavers. (019)
CM> which, if expressed in full FOL, raises the possibility
> of intractability. (020)
That possibility is only slightly more likely than the chance
that the world will end tomorrow. Nobody but a professional
mathematician or logician is even capable of "thinking" of
an intractable statement, let alone worrying about whether it
can be proved. (021)
Please note that mathematicians have been using FOL for millennia.
They were blissfully unaware of computational complexity or
undecidability. Yet it never caused the slightest problem for them.
All the FOL statements that Whitehead and Russell stated in the
_Principia Mathamtica_ can be proved in a fraction of a second with
modern theorem provers. (022)
CM> I'm not saying [intractability] can't be managed -- obviously,
> it can, if only by putting temporal bounds on searches for proofs
> and countermodels. But that there might be a need to do so if
> one uses full FOL does need to be expressed. (023)
Yes, such checks should be part of the development methodology. (024)
But Cyc has also had 25 years of experience in using a *superset*
of FOL, and they have *never* encountered any example where the
expressive power created problems. The kn. engineers have often
written false or buggy statements. But expressive power was not
a problem. (025)
John (026)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (027)
|