RE: SUO: OpenCyc Motion Open for Discussions
Hi John;
To ask a naïve question, what would the down side of not including tautological axioms in the top of a lattice of theories? 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 ;^)).
It seems to me that they should be treated the same as all the rest of the axioms out there that are invited to join a theory solely at the discretion of the theories author.
But I suspect I'm using the wrong metric to measure their value.
Thanks in advance,
-Eric Peterson
> -----Original Message-----
> From: John F. Sowa [mailto:sowa@bestweb.net]
> Sent: Saturday, April 05, 2003 11:24 PM
> To: cg@cs.uah.edu; standard-upper-ontology@ieee.org
> Subject: Re: SUO: OpenCyc Motion Open for Discussions
>
>
> Radu,
>
> The lattice of theories was first defined by Adolf Lindenbaum
> (a student of Tarski's) in the 1930s. There are actually
> many different lattices, depending on which version of logic
> you use to express your theories. For simplicity, I'll assume
> conventional first-order logic, but it is possible to use any
> version of logic (and in fact, the IFF framework is general
> enough to support any number of lattices). Following is a
> brief summary of the FOL version:
>
> 1. The top of the lattice is the theory that has no axioms.
> It includes all tautologies -- i.e., propositions that
> can be proved with no assumptions whatever.
>
> 2. The partial ordering is defined by implication (using
> whatever definition of implication your logic may have).
> If X implies Y, then every proposition of Y is implied by
> the conjunction of axioms of X. Every theory in the
> lattice implies the top theory T.
>
> 3. The bottom of the lattice is the absurd theory, which
> contains all propositions and is therefore inconsistent.
> The bottom theory implies all others.
>
> 4. Given two theories X and Y, the supremum of X and Y is
> the most specialized theory that is implied by both X
> and Y. The infimum of X and Y is the most general theory
> that implies both X and Y.
>
> Since there are infinitely many tautologies, such as p->p,
> (p&p)->p, (p&p&p)->(p&p), etc, the top theory T includes infinitely
> many propositions. Since every other theory contains T as
> a proper subset, they are all infinite. If you restrict the
> lattice to finitely axiomatizable theories, then there are a
> countable infinity of theories. But if you like, you could permit
> theories that can only be axiomatized with an infinity of axioms.
> Then there would be an uncountable number of theories in the lattice.
>
> Clearly, it is not possible to implement an infinite lattice,
> and it is not possible to represent all the propositions of any
> theory in the lattice. But it is possible to represent any finitely
> axiomatizable theory, and those are the ones that are most important
> for practical applications.
>
> The operators on the lattice can be implemented by the usual
> inference engines for first-order logic.
>
> John
>