SUO: Re: In Praise of Zeroth Order Logic
Jon Awbrey wrote:
>
> ¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
>
> Michael Gruninger's note had such a positive ring
> to it that I thought I might try to chime in, though
> in a lower register or a minor key, as befits my range.
>
> It's true that thinking too much about all the stuff
> that we want and can't have, all the things that we'd
> like to do and can't, all this cant about "no go there"
> which is all we seem to hear from logicians these days,
> can be downright dispiriting, if not utterly paralyzing.
>
> Of course there is no going back, no choice but to recognize
> our limitations -- only disaster ensues from ignoring that --
> but still, sometimes you need to think about all of the good
> and useful things that you can do with even the simplest and
> the most gratuitous of basic materials.
>
> So let this song be taken in the spirit of the general enchoiry,
> in praise of the splendid things that we can actually accomplish
> with so humble an instrument or organon as propositional calculus.
>
> Well, as often happens, I have used up my breath and my time,
> for now, with all of this preliminary fanfare, so I will get
> back to it later on, resting content, for now, that my theme
> is well-augured, if none of its variations are yet opportuned.
>
> ZOL!
>
> Jon Awbrey
>
> ¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
ZOL SIG:
I wanted to get back to this hopeful thread before
I forgot what I had in mind, but the re-stringing
of the original harp may be a bit rough at first.
I like to think of ZOL as the ground floor or the lower bound
for any brand of useful logic. It is obvious that we cannot
do everything that we want within its realm, but when we do
find that a problem reduces to this level, then it is quite
advantageous to have a syntax and a set of inference steps
that is as efficient and as flexible as possible.
Anyway, this is the conclusion that I reached in the middle 80's,
when I began my first trials and tribulations with what was then
called the "automatic theorem proving" (ATP) branch of AI, and
after my first experiences with one or two primitive tribes of
"general resolution theorem-provers" had led me to believe that
a lot of the thrashing around that they were doing then was due
to computational complexities that had not been managed properly
at the purely propositional level. I know, NP-completeness and
all that, but at the time it was something of a revelation to me.
Now, in those times I was even more arrogant than I am today --
try to imagine! -- and I believed moreover that I held a secret
key to all of the previously recalculant doors, in the form of
Peirce's work on graphical logics. Well, I would not say, even
today, that this unabashed and completely unwashed opinion was
entirely false, but, of course, nothing is ever quite that easy.
I am just telling you this so that maybe you won't imagine that
I made all of this stuff up just the other day, or something.
The reason why I think that all of this is worth bringing up in the
context of the discussions that we have been having lately is this:
1. When you have a logical system for which complete algorithms
are available to find all of the satisfying interpretations
(truth value assignments to the variables) of an expression,
then several different styles of reasoning become feasible,
with features that are distinctly different from those that
we commonly take for granted.
2. In particular, we acquire the option of using equational modes
of inference, with logical equivalences between the expressions
at each successive step.
3. Given a decent calculus for propositions, modeled as functions of
type f : B^n -> B, whose "fibers" (f^(-1))(1) are subsets of B^n,
it becomes possible to exploit many partial analogies between the
"universes of discourse" of conjoint type <B^n, B^n -> B> and the
spaces and functions of conjoint type <R^n, R^n -> R>, R = Reals,
that are of interest in "real analysis", comprising the subfields
of analytic geometry, functional analysis, and differential geometry.
There is in this the beginnings of a novel way -- novel in the sense
that it was new with Newton -- of dealing with change and diversity
in logical frameworks.
Coming Attractions: "Propositional Equation Reasoning Systems" (PERS).
May the whetstone of your wit
Not go un-whetted by this bit,
For we have much yet to carve,
All your wit's edges to crave.
More, Later,
Jon
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤