ONT Re: Zeroth Order Theories (ZOT's)
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
CM = Chris Menzel
JA = Jon Awbrey
CM: What does this baroque framework do that a hundred other little
programs for doing propositional logic and model theory don't do?
As with every other comprehensible part of your work that I've seen,
you are simply reinventing the wheel -- illustrated with ASCII art.
JA: Coming as it does from a fan of Bach, I will take take the "baroque"
as a compliment, ...
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*?
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: Why should anyone give a rip? Do they enable us to
represent knowledge that is otherwise unrepresentable?
No, not in principle, of course.
But yes, in practice, when you
consider how often we give up
representing things, much less
trying to reason about things,
that exceed our capacities
for doing the actual work
of actualizing principles.
CM: Can they be used to improve the computational
efficiency of existing theorem-proving engines?
Yes, I think so, though it depends on what you have in mind
under "existing theorem-proving engines" and the inherent
plasticities of that term and those forms of enginuity.
At any rate, the system of syntax in question has
already served to improve the efficiency and the
conceptual grasp of one existing theorem prover,
namely, yours truly.
"On jugera", he says.
CM: Do they enable us to see anything that we didn't see before?
In principle, no.
In practice, yes.
To understand the difference between "principle" and "practice",
or, to sharpen the issue up into something a bit more concrete,
the correlated difference between "effective" and "efficient",
we might study the equivocation that is often bandied about
under the phrase "polynomial time equivalence class" (PTEC)
in regard to the efficiency of different implementations
of the same procedure, in effect, the felicities of
diverse denotations of a shared formal object.
I know a whole class of people who will consider -- who will "say"
that they consider -- all concrete implementations of an abstract
specification that happen to fall into one and the same PTEC as
being "all the same to them" -- "in principle", "in theory",
I can almost hear them numbling under their common breath --
but I say that they embroil themselves in an uncritical
and unreflective self-deception if they say that.
CM: By my admittedly often dim lights, the answer in each case is "No".
All this impressive energy of yours would seem to me to be far more
usefully turned to, say, the construction of real ontologies.
Or maybe to writing poetry.
Believe me, nobody wants to see that.
Jon Awbrey
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤