ONT Re: Zeroth Order Theories (ZOT's)
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
CM = Chris Menzel
JA = Jon Awbrey
CM: Well, ignoring the inference from "S thinks baroque music is good"
to "S thinks anything baroque is good", as in music so in logic.
Detail and ornamentation are good when they have a purpose.
My objection to your stuff, as clever and even as elegant
as it might be, is that, as far as I can see, it just has
no purpose. It either provides nothing that isn't already
available in familiar (and generally far more straightforward)
forms, or else it does things that appear to be utterly pointless.
CM: What are the data structures depicted by your ASCII art *for*?
JA: They are for representing the same things that propositional expressions
in every other adequate syntax represent, only with a better articulation
of the invariant structures in these objects themselves and thus with what
most folks who consider the matter would consider a better conceptual grasp
of these objects, and, incidentally, but not entirely coincidentally, with
a better address of their computational complexity and thus with a better
mean-real-time computational performance, other things being equal.
CM: Sounds good, but I really have no idea what you mean by the invariant
structures of propositional expressions that would make this claim true.
Perhaps you could tell us. The only invariant structures I can think of
(e.g., some representation of indicative statements, some representation
of boolean operators, operator scope, etc) would, as far as I can see,
be pretty much as fully articulated in one representation as another.
Though "degree of articulation" itself is an awfully vague and
subjective notion to carry much scientific weight.
Okay, I feel like I have "articulated" all of this in slightly better detail
and quite a bit more exactly several times already, but perhaps there were
distractions that I introduced into the account. I have already made my
numerous off-list excuses to individual querents about the way that
I communicated when I first washed up on SUO shores -- I had just
spent ten years of mind-numbing nitty-gritty work on eighty odd
drafts of my dissertation and was in no mood to settle down to
more of the same here. That fun's over, but some folks have
yet to forgive and/or forget.
When I speak of "propositions" at this level of glibness,
I am of course speaking with a forked tongue, and here
is just one of several explanations that I have given
of the quasi-commutative diagram that explains the
forking of it:
| If this is starting to sound a little bit familiar,
| it may be because the relationship between the two
| kinds of pictures of propositions, namely:
|
| 1. Propositions about things in general, here,
| about the times when certain facts are true,
| having the form of functions f : X -> B,
|
| 2. Propositions about binary codes, here, about
| the bit-vector labels on venn diagram cells,
| having the form of functions f' : B^k -> B,
|
| is an epically old story, one that I, myself,
| have related one or twice upon a time before,
| to wit, at least, at the following two cites:
|
| http://suo.ieee.org/email/msg01251.html
| http://suo.ieee.org/email/msg01293.html
|
| There, and now here, once more, and again, it may be observed
| that the relation is one whereby the proposition f : X -> B,
| the one about things and times and mores in general, factors
| into a coding function c : X -> B^k, followed by a derived
| proposition f' : B^k -> B that judges the resulting codes.
|
| f
| X o------>o B
| \ ^
| c = <x_1, ..., x_k> \ / f'
| \ /
| o
| B^k
|
| You may remember that this was supposed to illustrate
| the "factoring" of a proposition f : X -> B = {0, 1}
| into the composition f'(c(x)), where c : X -> B^k is
| the "coding" of each x in X as an k-bit string in B^k,
| and where f' is the mapping of codes into a co-domain
| that we interpret as t-f-values, B = {0, 1} = {F, T}.
In short, there is the standard equivocation ("systematic ambiguity"?) as to
whether we are talking about the "applied" and concretely typed proposition
f : X -> B or the "pure" and abstractly typed proposition f' : B^k -> B.
Or we can think of the latter object as the approximate code icon of
the former object.
Anyway, these types of formal objects are the sorts of things that
I take to be the denotational objects of propositional expressions.
These objects, along with their invarious and insundry mathematical
properties, are the orders of things that I am talking about when
I refer to the "invariant structures in these objects themselves".
"Invariant" means "invariant under a suitable set of transformations",
in this case the translations between various languages that preserve
the objects and the structures in question. In extremest generality,
this is what universal constructions in category theory are all about.
In summation, the functions f : X -> B and f' : B* -> B have invariant, formal,
mathematical, objective properties that any adequate language might eventually
evolve to express, only some languages express them more obscurely than others.
To be perfectly honest, I continue to be surprised that anybody in this group
has trouble with this. There are perfectly apt and familiar examples in the
contrast between roman numerals and arabic numerals, or the contrast between
redundant syntaxes, like those that use the pentalphabet {~, &, v, =>, <=>},
and trimmer syntaxes, like those used in existential and conceptual graphs.
Every time somebody says "Let's take {~, &, v, =>, <=>} as an operational
basis for logic" it's just like that old joke that mathematicians tell on
engineers where the ingenue in question says "1 is a prime, 2 is a prime,
3 is a prime, 4 is a prime, ..." -- and I know you think that I'm being
hyperbolic, but I'm really only up to parabolas here ...
CM: But let me put my cards on the table. The reason I have been challenging
your views rather stridently is because of your earlier portentous rumblings --
wholly devoid of argumentation -- about the devastating consequences of using
KIF and other standard logic-based KR languages for ontology. All that you have
provided us with is a repackaging of first-order logic, basic set theory, and a
bit of recursion theory -- in a word (or two) nothing new, save some novel and
perhaps heuristically or pedagogically useful new representations -- which,
in and of themselves, I encourage and applaud. But your dire warnings
against the use of KIF and its ilk for ontology are utterly without
foundation. Frankly, you should retract them.
I have already refined my criticism so that it does not apply to
the spirit of FOL or KIF or whatever, but only to the letters of
specific syntactic proposals. There is a fact of the matter as
to whether a concrete language provides a clean or a cluttered
basis for representing the identified set of formal objects.
And it shows up in pragmatic realities like the efficiency
of real time concept formation, concept use, learnability,
reasoning power, and just plain good use of real time.
These are the dire consequences that I learned in my
very first tries at mathematically oriented theorem
automation, and the only factor that has obscured
them in mainstream work since then is the speed
with which folks can now do all of the same
old dumb things that they used to do on
their way to kludging out the answers.
It seems to be darn near impossible to explain to the
centurion all of the neat stuff that he's missing by
sticking to his old roman numerals. He just keeps
on reckoning that what he can't count must be of
no account at all. There is way too much stuff
that these original syntaxes keep us from even
beginning to discuss, like differential logic,
just for starters.
Jon Awbrey
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤