SUO: *Date 18 Apr 2002 -- Theory Query
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
1. Model Theory
The model theory revue continues to play on the ontology sublist.
These last three installments provide a quick summary of all the
basic terms and definitions, and a preview of coming attractions:
30. http://suo.ieee.org/ontology/msg04020.html
31. http://suo.ieee.org/ontology/msg04021.html
32. http://suo.ieee.org/ontology/msg04022.html
2. Theory Query
JA = Jon Awbrey
JS = John Sowa
JS: There are lots of things to worry about in mathematics, science,
and life. But there is a difference between worrying about the
definition of a mathematical construction and its theoretical
implications and worrying about how and whether it might
be used or abused in practice.
JA: 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.
JA: So I worry about that.
JS: I agree that it is an issue that is worth being
concerned about when using the idea in practice.
But that same question arises in slightly different
guises in every other approach -- formal or informal.
JS: The reasons why I like the Lindenbaum lattice are that it brings
these questions into the open, it provides a systematic perspective
on them, it classifies the kinds of operations that may be performed
on the theories, and it unifies many diverse operations as different
aspects of a common underlying formalism.
JS: Bottom line: The Lindenbaum lattice doesn't solve all the world's
problems, but it provides a systematic view of some important problems,
and it provides a convenient framework in which they can be addressed.
I'm not saying that it isn't a workable idea.
I'm just thinking through the questions that
come up as I try to see how it would work in
practice. Yet another great chain of being
is one thing -- but we were talking about
an "embedded and situated implementation",
which is not as easy as it sounds.
And of course these problems have a familiar ring --
we have Morning*Axioms and we have Evening*Axioms --
and there are all sorts of cases where we have to
work from a diversity of axioms and beliefs while
keeping the questions of their consistency and
equivalence in suspension for very long times.
Axiom sets are like any other signs that may
or may not denote their ostensible objects,
and so that tension between the sign pole
and the object pole is always with us.
The question is, how do we do this?
What sort of semiotic architecture
supports this ability, and how can
build it into our implementations?
That is what I have been thinking about,
and when I say "I worry about that" it
just means that I do not automatically
know the answers. But I am willing to
bet that a sign relational framework
is a key to making it work.
I guess the gist of it would be this:
The lattice you are talking about is
an architecture whose structure is
only known for certain at the end
of the inquiry to that purpose --
and I'm just asking about what
sorts of shelters we can find
in the meantime.
Jon Awbrey
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤