Re: SUO: OpenCyc Motion Open for Discussions
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
John,
Axiom sets and theories are set of sentences -- syntactic beasts --
lattice element are mathematical objects -- objective critters --
For example, Groups: there is a set of three axioms for groups
that most folks use most of the time, but there are six or seven
others that have their fanatic followings, and that even turn out
to be useful on occasion. It can take a lot of work to show where
an axiom set or a theory belongs in the proper objective lattice.
A minimal amount of "semiotic awareness" (SA), not to mention
computational and mathematical realism, demands that we keep
this distinction constantly in mind.
The inconsistent theory is one which has all wffs as thms.
That makes it Top as far as subsets of formal languages go.
I'm sure that there is a nice galois connection between this
right side up view of the world and how things look when one
stands on their head, but the connection has to be constructed.
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
John F. Sowa wrote:
>
> 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
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o