SUO: *Date 17 Apr 2002 -- Theory Query
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Theory Query
JA = Jon Awbrey
JS = John Sowa
JS: What I had in mind is the Lindenbaum lattice, as I presented it
in Chapter 2 of my KR book. A summary of that presentation is
also contained in Section 6 of my paper on causality:
JS: http://www.jfsowa.com/ontology/causal.htm#s6
JA: In this context, we have the notion of a first order predicate language $L$,
plus the set !L! of its 'sentences' (i.e., formulas with no free variables).
JA: According to one standard usage, a 'theory' is any set of sentences,
in which case we already have a natural lattice of theories, namely,
the power set !P!(!L!) of !L!.
JA: Is that what you have in mind?
JS: No, the set of all subsets of FOL sentences is
a much bigger lattice. What you need to do
is to take the quotient space generated by
the provability relation |- of FOL (or the
semantic entailment operator |= which is
equivalent to provability for FOL).
JS: In effect, the Lindenbaum lattice is the set of equivalence classes
of axiomatizations. Any set of FOL sentences may be adopted as a
set of axioms (or axiomatizations). Any two axiomatizations are
equivalent (i.e., in the same equivalence class) iff they have
the same deductive closures (i.e., exactly the same implications).
JS: The top of the lattice is the set of all tautologies (i.e.,
everything provable from or entailed by the empty set).
JS: The bottom of the lattice is the collection of all FOL sentences (i.e.,
everything provable from any contraction of the form p & not-p).
JS: The partial ordering of the lattice is determined by implication (i.e.,
if p implies q, then q is more general and p is more specialized).
Okay, so far so good.
That pretty much accords with the intuitive notion --
to put topology near the top, projective geometry in
the middle, and euclidean geometry more down to earth,
for instance -- but when I start thinking about how to
make this sense of things more formal, enough to make
such a lattice effectively negotiable by computer,
then I run into some further worries.
I will need to hang onto the language parameter, $L$ ("Script L").
And I will use the terminology C & K, since all this has forced me
to brush up on what I can remember of it. They call your "theory"
a "closed theory", so that's an easy adjustment. And I think that
the way that they use "set of axioms" is confluent with your usage.
A thing they do that bothers me is to define $L$ as the basic set
of symbols, what you call the "vocabulary", I think, but then use
it also to refer to the set of sentences. I'll use !L! for that.
The first thing that worries me is the way that $L$
changes from point to point of the informal lattice.
C & K use the pair expansion/reduction to describe
changes in the symbol set:
| We occasionally pass from a given language $L$ to another language $L$’
| which has all the symbols of $L$ plus some additional symbols. In such
| cases we use the notation $L$ c $L$’ and say that the language $L$’ is
| an 'expansion' of $L$, and that $L$ is a 'reduction' of $L$’. In the
| special case where all the symbols in $L$’ but not in $L$ are constant
| symbols, $L$’ is said to be a 'simple expansion' of $L$. Since $L$
| and $L$’ are just sets of symbols, the expansion $L$’ may be written
| $L$’ = $L$ |_| X, where X is the set of new symbols.
|
| Chang & Keisler, 'Model Theory', pages 18-19.
| http://suo.ieee.org/ontology/msg04005.html
They use the pair extension/submodel to talk about the models:
| We use $A$’ ç $A$ to denote that $A$’ is a submodel of $A$, and
| the symbol 'ç' for the submodel relation between models for $L$.
| The reader should show that ç is a partial-order relation and
| that, if $A$ ç $B$, then |A| =< |B|. We say that $B$ is
| an 'extension' of $A$ if $A$ is a submodel of $B$.
|
| Chang & Keisler, 'Model Theory', pages 21-22.
| 23. http://suo.ieee.org/ontology/msg04009.html
But the main thing that worries me is this:
I have to draw a distinction between things
that can be in my head and things that cannot --
where "in my head" is misleading figure for
"signs that I can embody in the media over
which I have some modicum of control, from
brain and body to the extensions thereof" --
and it is important to keep track of the
things, like elephants and numbers, that
are not of that sort. And, of course,
there is the analogous bit-barrier
"in the computer".
The point is that a full-fledged mathematical object,
like an infinite lattice, is not the sort of thing
that can be in my head or explicitly detailed in
a finite information device like a computer.
The nice thing about a lattice is knowing
where you are in some ordering, in other
words, where the objects of your present
attention fit into the scheme of things.
And here the power set lattice !P!(!L!)
and the quotient space lattice !L!/|=
seem to have very different statuses.
!L! is at least a bunch of signlike things,
a finite sample of which I can have in mind,
or in a belief-base (BB) in a real computer.
And even if I can't quite grasp the whole
power set lattice of sentences, I can know
lots of local relationships exactly, from
looking at finite subsets and inclusions.
In effect, there are definite points of
the lattice that I know and can know
where they are in that ordering.
But when it comes to the quotient lattice,
it is my experience that proving different
axiom sets equivalent can be rather tricky,
and so you may never know where your favorite
axiom set is located in the lattice of theories.
So I worry about that.
Jon Awbrey
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤