Re: SUO: Question
Randall / John,
I believe that I can accept the definition of a theory that Randall offers
from Enderton including the substitution of "unsatisfiable" for "false" without
it making much difference to the concerns I expressed to John Sowa regarding
his proposal of a lattice of all possible theories..
I also oppose admitting ill-formed theories (axioms/modules, etc.) into the
lattice John proposes. The difficulty is that with a very large number of
theories in the lattice ("all possible theories") and no requirement for
inclusion, how would one know that it is ill-formed. It seems to me that
John specifically allows for this in his proposal. The problem Randall poses
of how they could be evaluated if they are ill-formed is one John should
discuss in his tutorial.
In comparing two well-formed ontologies (theories/modules) for compatible
use for a particular purpose, if they pass some minimal bar ( e.g. their
supremum is not the top and/or their infinimum is not the absurd) the user
must then refer to annotations to the modules that are not evaluated by the
lattice operators. I can see that the lattice operations do provide some
structure useful for analysis (e.g. the patterns formed by the results of
the lattice operations) but it does not offer automated assistance in selecting
modules useful for a particular purpose - in fact it appears to create an
n to n mapping problem with a very large n.
It is also very possible that I do not understand John's proposal or fail
to appreciate its utility. In the mid 90's John, Fritz Lehmann and I discussed
an idea of using lattices and lattice operators in a very different manner
to create ontologies. If I remember correctly we called it a factored combinatorial
structure that resulted in a lattice (John/ Fritz this is the discussion
we had at Stanford / CSLI and later discussed with Doug Lenat). One of the
purposes of the theory discussions at Heidelberg was to develop a list of
primitives that could be used as factors to semi automatically generate a
"standard" Reference Ontology using this combinatorial methodology. I think
the other participants in the Heidelberg theory discussions were John Sowa,
Fritz Lehmann, Nicola Guarino, John McCarthy, Chris Menzel, Bill Anderson,
Peter Simons and Pat Hayes.
John, I look forward to your tutorial. Even if it does not create a "standard"
ontology usable for most purposes, a technique that provides evaluation of
the mapping of ontologies to each other will be very useful, even if it is
one to one.
Bob
Randall R Schulz wrote:
5.1.0.14.2.20020408224239.02705f58@pop3.cris.com">
At 22:32 2002-04-08, Robert Grayson Spillers wrote:
John,
In your proposal of an (infinite) lattice of all possible theories, do modules
that are ill formed also fit into this lattice (e.g. do not have any stated
or consistent methodology, are defective or inappropriate in some other
way)? I assume so since it is "all possible theories" even poorly formed
or simply false theories ( I am using what I believe is a widely accepted
definition of a theory - something that can be assigned a truth value).
If one can have both p and ~p in the lattice how will one decide which to
use? How will one know that both p and ~p are present (or not present)
in the module of theories one selects to use? It seems to me that one must
have some test of compatibility if one is asked to select some theories
from a much larger (infinite?) number to use.
Robert,
It sounds to me like you're equating a formula with a theory.
I understand "theory" to be what Enderton defines in "A Mathematical Introduction
to Logic:"
Section 2.6, page 144
"Theories
"We define a theory to be a set of sentences closed under logical implication.
That is, T is a theory iff T is a set of sentences such that for any sentence
sigma of the language,
T |= sigma ==> sigma elementOf T."
In general a theory is not a finite set, so computer representations must
remain somehow incomplete for theories whose T has a transfinite cardinality.
I don't see the point in even contemplating admitting non-well-formed formulas
into any logical system. What interpretation can they be given? None--they're
not well-formed.
You may see it as quibbling, but a theory cannot be "false," but it can be
unsatisfiable. (A sentence can have a truth value, however.)
That said, you're correct, conjoining theories requires some sort of "truth
maintenance" to ensure that consistency remains after merging them. It's
also necessary that the theories' models are identical or are somehow consistently
mergeable as well.
Randall Schulz
Mountain View, CA USA
...
A tutorial would be very welcome.
Bob