Re: SUO: OpenCyc Motion Open for Discussions
Eric,
The lattice of all possible theories is a mathematical
structure that can never be implemented in its entirety.
Its purpose is to provide a framework of operators for
organizing, indexing, combining, and relating whatever
theories (or microtheories) you intend to implement.
> To ask a naïve question, what would be the down side
> of not including tautological axioms in the top
> of a lattice of theories?
The topmost node of the lattice has zero axioms.
It is the theory whose implications include everything
that is provable from the empty set. Therefore, it
contains all sorts of tautologies, such as p->p,
P & p -> p & p & p & p, etc. Those are not the
*axioms* of the topmost theory -- they are its
implications. (And by the way, the tautologies
are also the implications of every theory.)
So there is really nothing to "implement". It is
represented by its axioms -- namely the empty set.
It is like the number 0 in the integers. You never
"implement" zero, but it is the marker of what
happens when you take everything away.
> I note that I have survived without them in my work
> using lattices of theories in Cyc, Ontolingua,
> VerticalNet's Protégé-like environment, and even
> using Common Lisp's package system (Lisp symbols
> within a package can be viewed as 0-ary predicates
> and Lisp functions can of course be viewed as
> logical functions ;^)).
You have been using the topmost node all that time
without realizing it. Whenever you start to edit
an empty file with nothing in it, you are looking
at a blank page. That blank page represents the
empty set, which is the totality of axioms from
which all tautologies can be derived.
As soon as add one axiom to the empty set,
you have specialized your theory to another node
farther down in the lattice. Then when you type
a second axiom, you have specialized it to another
theory that is a specialization of the previous one.
You have been using the lattice of theories all that
time without realizing it. The only point I am making
is that we should recognize that fact and take advantage
of it by designing our tools in a more systematic way.
John