Hi Chris, (01)
Chris Menzel wrote: (02)
>On Thu, Mar 09, 2006 at 01:04:24PM -0500, Michael Gruninger wrote:
>
>
>>>Structuring is even more crucial for proving consistency of
>>>ontologies. It is much easier to prove inconsistency (i.e. derive
>>>false using a theorem prover) than prove consistency (e.g. by
>>>constructing a finite model using a SAT solver, or by using a
>>>resolution prover for finding a saturated set of clauses not
>>>containing the empty clause).
>>>
>>>
>>Consistency proofs can also be done in the metatheory by characterizing
>>all possible models of a theory and classifying them up to isomorphism.
>>
>>
>
>Michael, I may be misunderstanding (been known to happen :-), but how
>does such a classification yield consistency? From the fact that you've
>partitioned the models of theory T into isomorphism classes (I take it
>this is what you mean by "classifying them up to isomorphism") it
>doesn't follow that there *are* any such models. Granted, it may be
>obvious in some cases that there are, but if the specification of a
>model is complicated enough, it may not be.
>
>>This is what we have done with the PSL Ontology. For each theory
>>within the ontology, we specify a class of structures and then prove
>>two theorems: Satisfiability: any structure in the class satisfies the
>>theory.
>>
>>
>
>But again, consistency doesn't follow from satisfiability in this sense
>alone (so "satisfiability" might actually be a misnomer here). We also
>need to know that the class of structures in question is nonempty.
>Fortunately, as you know better than anyone, in the case of PSL, you can
>prove (in ZF) that the relevant class is nonempty pretty easily. But,
>conceptually anyway, that's a separate proposition that might, in
>general, require a distinct proof.
>
>
> (03)
Yes, the wording is a little clumsy; more accurately, the methodology is: (04)
1. Specify a class of structures
2. Existence Theorem : show that this class is nonempty
3. Classification Theorem: classify the structures in this set up to
isomorphism
4. Show that each structure in the class is a model of the theory
5. Show that each model of the theory is elementarily equivalent
to a structure in the class. (05)
Pedantically speaking, these are relative consistency proofs, since the
structures are typically defined with respect to classes of graphs,
geometries,
ordered sets, groups, semigroups etc. which we assume exist and are
nonempty. (06)
The classification theorem is not always necessary, but it does give the
best
"picture" of the possible models of the theory, alerting people to
models that
are potentially unintended. It also gives more insight into the theory.
For example, you could say that a group is any structure that satisfies the
group theory axioms, but this doesn't tell us much; you get much more sense
of the models from the classification theorem and structure theorems
that tell
you how to decompose groups into subgroups. (07)
- michael
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/uos-convene/
To Post: mailto:uos-convene@xxxxxxxxxxxxxxxx
Community Portal: http://ontolog.cim3.net/
Shared Files: http://ontolog.cim3.net/file/work/UpperOntologySummit/uos-convene/
Community Wiki: http://ontolog.cim3.net/cgi-bin/wiki.pl?UpperOntologySummit (08)
|