On Thu, Feb 01, 2007 at 05:21:04PM -0500, Conrad Bock wrote:
> I'm with Pat that intended models have a "deja vu" effect, and it's
> unclear at first why there is any benefit to relating axioms to
> intended models, when intended models are necessarily less formal than
> axioms. You can't really prove things about this relation in the
> strict sense of showing an axiomatic proof, because the representation
> of intended models isn't itself a set of axioms. (01)
Well, yes, of course, models aren't axioms, but facts about the relation
between a theory and its intended models can *most definitely* be
expressed and proved in a completely formal, axiomatic way. It is true
that we usually do model theory in "mathematical English", but the same
is true of most mathematics. Fact is, though, model theory is just an
application of Zermelo-Fraenkel (or whatever) set theory. Just as we
can define the numbers to be set theoretic objects, languages can also
be represented as set theoretic objects as well (or you can take them to
be sui generis and use ZFU, i.e., ZF with urelements). Model structures
are themselves set theoretic objects, of course, and all of the usual
semantic relations between a language L and an appropriate class of
model structures (notably, truth in a structure) defined by an
interpretation of L are rigorous mathematical relations. Moreover, it
is perfectly possible within this framework to declare a certain class
of models of a theory to be intended. For instance, in ZF, we can
declare omega-models to be the intended models of PA. This is all
*completely* rigorous. For example, we can say with great precision
precisely what the structure of all countable, non-omega models of PA
look like (N + QZ for logic nerds, where N, Q, and Z are the order-types
of the natural numbers, rational numbers, and integers, respectively) --
from which it follows immediately that no such model is intended. (02)
> So model theory can't be a completely rigorous methodology for
> determining ontological correctness. (03)
Whether it is a *useful* methodology is one thing, but there is no doubt
about its rigor. (04)
> For example, the intended models you (Michael) use for PSL are notated
> in a mathematical notation that is not itself an axiomitization. To
> me the mathematical notations, and the even more informal pictures
> that go with them (I know you draw these!), are an intermediate form
> between the fully formal axiomitization and the vagua meanderings of
> thought. (05)
All of Michael's pictures are informal descriptions of completely
rigorous mathematical structures that are formally definable in ZF. (06)
> The only point of establishing the relation of the axioms to these
> less formal representations is for your own assurance, and others who
> know those less representations. Mathematics happens to be designed
> to make it easier for people to reach agreement about it, so is a good
> candidate for representing intended models. However, for people who
> don't know it, it isn't much assurance that a set axioms can be mapped
> to it.
>
> If it happened that people found axiomitizations perfectly
> perspicuous, then intended models would not be necessary. Perhaps Pat
> is one of those people. For me, I find the intended models of PSL,
> for example, very useful it understanding the axioms and checking that
> they are what they should be. Can we measure the amount of this
> "assurance" provided by a model theoretic semantics ? Not so clear
> how to do that. (07)
It is quite clear if you have a completeness proof -- my own doubts
about Michael's methodology concern the question of how many truly
useful complete theories there are. I find Pat's point about OWL's use
of XSD datatypes particularly worrisome for the model theoretic
approach. (08)
Chris Menzel (09)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Subscribe/Config: 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 Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (010)
|