Tuesday, December 20, 2005
Lattice of ontologies
John Sowa’s replies to Prueitt’s questions
A lattice of theories is *not* developed. It is like the integers: it has resided for all eternity in a Platonic heaven of mathematical structures.
It imposes no restrictions whatever on how anybody does or should or might think or act. It's like the integers: they don't tell you how many people do or should or might be counted in the next census. But they provide us some assurance that there will exist an appropriate integer in that Platonic heaven to count whatever number of people might exist at the time the census counting is done.
> So how are lattice of theories developed?
What are developed are particular statements of theories that people or computers write (or type).
When a theory is developed, an integer can be plucked out of that Platonic heaven, such as #17, and be pasted as a label on that theory.
Instead of using integers to label the theories, I am proposing that we adopt that lattice from the Platonic heaven. The reason why a lattice is better than the integers is that the integers are linearly ordered, but a lattice has a partial order, which allows more options in the way one theory is related to any other.
Then whenever anybody writes a theory, we may be able to show where it fits in the lattice in relation to any other theory that has been developed or the infinitely many other potential slots for theories that nobody has yet developed (or written or typed).
There is one qualification that I haven't mentioned: to show whether theory A is a generalization, a specialization, a sibling, or a distant cousin of another theory B requires a theorem prover. Sometimes that theorem prover will give us an answer very, very quickly. But other times, it might take a long time -- perhaps it might never come back with an answer.
But not to fear: this limitation is exactly the same limitation that programmers face every day: proving that any given program is correct or even that it will eventually stop is undecidable.
Yet programmers live with that undecidability every day, and they even take *advantage* of the insights from the idea to adopt *structured* methods for designing programs so that it is possible to guarantee, in advance, that they will stop or that they will have certain desirable properties.
That is my fundamental reason for recommending a lattice: it suggests certain *structured methods* for designing a theory so that it is determined *in advance* where it will fit in the lattice -- sometimes the exact place and sometimes within the right ballpark -- i.e., there may be cases where it is unknown whether two apparent siblings happen to be identical twins.
There is more to be said about structured methods, but the main point I want to make is that they are like structured programming: lattices don't restrict the subject matter of the ontologies you write, but they provide guidelines that make them easier to analyze, understand, debug, and test.