SUO: *Date 22 Apr 2002 -- Theory Weary
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
BA = Bill Andersen
JA = Jon Awbrey
JA: I have been making a dedicated effort to take this
first-order logic, formal semantics, model theory
approach to our so-called real existence seriously,
and maybe it's just the end of the week let-down,
but there just seems to be some definite problems.
JA: The kicker came when I ran into the first-order
description of 'group theory' as it comes to be
embedded within these layers of formal batting.
Here is an abridged version of what it takes to
say what a 'group' is, as a model of a certain
first order theory -- patience, it takes a bit:
JA: http://suo.ieee.org/email/msg08383.html
BA: First let me say that I agree with your frustration.
A couple of comments, however:
BA: a) Everything you wrote before getting to the axioms for
Group Theory is supposed to be considered background for
anyone who wants to use logic to talk about mathematical
(or any other) theory. Thus, it's a bit of a red herring
to complain about the weight of machinery involved.
BA: b) I can't imagine what the machinery would look like to talk
about our talking about Group Theory in English, for example.
In that sense, FOL looks a lot simpler to me. Did you have
some other mechanism other than natural language in mind?
Oh, sure, I had a bad cold all last week and was pretty much
worn out when I wrote that, but if you know how much I hate
typing you would know I didn't type all that stuff in just
to say it was useless. I took that course in model theory
back in '86 and C&K is still my favorite book on it, but
the thing is this -- it's a particular way of looking at
a subject, group theory, ontological theories, whatever,
and it's even true that you can use it to obtain some
theorems that you would probably not easily notice
from any other point of view, but still, it fails
to capture many important aspects of the way that
productive practitioners actually regard their
subject most of the time.
Put that way, it's a thoroughly trivial remark, of course,
but I think sometimes that some people have a tendency to
forget that you can't pursue hardly any subject at all in
a creative fashion from one, single, fixed point of view.
There were models and proofs for a long time before
there were model theory and proof theory, leastwise,
in their modern renditions. And the people who have
given us the greatest share of our models and proofs
for the last couple and a half millennia never spent
a lot of their time thinking about model theory and
proof theory -- they spent their time proving things
about mathematical objects. And I think that it's
fair to say that our contemporary versions of
model theory and proof theory tell us almost
nothing about how that is really done.
In the days before I knew the distinction before a "pure" mathematician
and any other kind, I never used to think about these things, either.
Only when I was forced to turn to the computer in hopes of some help
someday did I have to start reflecting on the nature of the process.
I started out with all of the most fashionable opinions of the day --
"abstractness is all" -- "proof within the limits of syntax alone" --
and in my "hopelessly naive" sort of way I sat down and started
to write out a program that explored proposition space by means
of inference rule operators in a brute force generate and test.
It just isn't done that way.
Without some kind of continuous attention to the aim of one's inquiry,
without some form of persistent guidance by the object of one's desire,
the task of proving anything in particular, much less anything of worth,
is simply hopeless.
In time, I learned the difference between model theoretic ways
and proof theoretic ways of approaching the whole problem of
computational inference. Incidentally, I found out that you
can learn a little bit of proof theory from model theorists,
but nothing at all about model theory from proof theorists.
Why that is I don't know, it's just an asymmetry I noticed.
Group theory is not an exercise in sentence generation --
it is an exercise of the imagination. One has an object
of interest in mind -- a general, imaginary, vague object,
for sure, and to different degrees in different dimensions
at different times -- but an interesting object nevertheless.
Now of course nobody cares about your idiosyncratic imaginings,
and so, in the course of time, at the end of the inquiry, as in
every other science, the final description, the summary report,
theorem and proof, theory and justification, all have to appear
as if they always operated within the constraints of acceptable
syntax, deductive inference, and standard styles of presentation,
but these rudiments of axioms, bounds, and constraints are never
truly generative of the subject in and of themselves.
The question is, what is?
Jon Awbrey
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤