:: towards a constructive education ::

From: galathaea (galathaea_at_excite.com)
Date: 02/03/04 

Date: Tue, 3 Feb 2004 12:25:58 -0800

While you are reading this, your retinal rods and cones are interpreting
images projected onto them. Each letter, like the

W

that begins this post is given a neural focus, an "attention", as rhythmic
waves refresh the focus regularly. The transmission through the optic
ganglions and along the optic fibres of the raw inforation of the

W

goes through a processing which has been well studied in the literature.
One successful modeling approach is that of the connectionists or found in
the neural net literature. The oculomotor loop and the importance of
saccades is established. We have many models on how neural nets detect
edges, identify topological components in their optic information, determine
orientation. The retinotopic map is formed.

These models are useful to the extent that there is actual technology built
with these models, and they make good money today. They agree with our
experiments extremely well. We can usefully pattern match the shape

W

with a fair degree of accuracy.

The logic of propositions in the models on shape theory, the theory of the
topological, metrical, and orientation-based classification calculus, the
dynamical logic of the attractor spaces in neural net models, the
region-connection calculus, all of these logics are Heyting.

Of course, human pattern matching involves much additional information
processing. When the

W

is blurry, when the information is vague, we may look to the surrounding

*hile

and call on recollections of known forms of full words. We've learned to
attach meanings to utterances and visual shapes, and while you are reading
this you are building structures of meaning to the words which can assist in
the recognition, determining patterns of abstractions connected in a mental
system of relationship which is still poorly understood. But every year more
information is gathered. The schematic decomposition of the process is
being studied, and regularly receives more insight towards the architectonic
basis of the function and dynamics of thought.

And, we can formalise the game of language. Formal languages have a well
studied mathematical foundation, and the reasoning in a semantic system can
be formalised in a model theory. When we look to the many sources of
"reasoning about", from necessities and modalities to counterfactual
possible worlds, satisfaction (semantic), operational resolution, etc. we
find many different logics. But they are all Heyting, and this substructure
common to all semantic theory allows for a rich functor structure of
equivalences and dualities amongst these logics. There are common
dictionaries to translate between various related semantics.

And there appears to be a very important reason this Heyting substructure is
found so predominantly in the formal languages and foundations of
mathematics. Formal reasoning has a structure of a state and its
transitions, it is in many ways the analysis of an automaton whose
transition graph is specified by the logic of the reasoning. Proof theory
is very intimately related to the theory of computation and the lambda
calculus. The lambda calculus has a well known Heyting structure, and we
have the Church-Turing thesis over our shoulders hinting that this may very
well be the most primary structure found in all algorithmics.

When we look to topics like Martin-Lof type theory to explain the evolution
of the objects of or conceptions and the structure of describing our world,
again we have its Heyting structure well known and studied.

Constructivism is very much the study of process and information, of the
logic of propositions on information structures. Processing information
allows us to channel it to useful decision making. It appears to be prior
epistemically to the abstraction of a "reality".

And we use this structure in our theories about the world around us. In
general, the semantics of evolving collections of objects and causality is
known to be Heyting. Applications of Heyting semantics have been detailed
for antigen-antibody interactions or the deviation of a cancer process, but
one of the most fascinating applications for me has always been the analysis
of quantum propositions and the evolution of quantum systems. In fact, the
work of von Neumann and Birkhoff is one of the most stark expressions of
this generality, where it was shown that contrary to much early physics, the
logic of the universe may very well be that of a Heyting algebra that is not
Boolean.

Now, I appologise for the large crossposting, but I believe this post to be
topical to all newsgroups in my list. I earnestly feel that there is a
common thread which needs to be discussed amongst all of these communities.
I am concerned about the education of constructive theory and Heyting
semantics prior to the study of classical logic and Boole (and Aristotle
when you lack quantifiers, etc.). And when I say Heyting here, prior, and
to come, I also intend co-Heyting, for obviously there are semantics
mentioned who have more reasonable interpretations in the dual algebras, but
that is of course a contravariant functor away.

For some reason, I feel that this sounds like a radical idea, even though I
also get the impression that Heyting algebras are not the controversy they
were when associated more strongly with Brouwer and intuitionism. There are
obviously many communities using them. They appear to be intimately related
with conceptualisation and the thought process.

Yet, going through the college system, I found it rare for non-specialists
to be aware of the more general Heyting structures found in their respective
fields, though they were often well prepared in classical logic. And I
often found that this presented a much _less_ useful tool in which to
evaluate the structures of their fields. The application of Boolean logics
to quantum systems is one of the major sources of "strangeness" under which
quantum mechanics is commonly described, and understanding how to properly
make propositions about quantum systems can clear up much confusion here. In
linguistics and formal foundations, there is regular rediscovery of basic
results on the difficulty of identity and the ambiguity of negation which
are well described by constructive semantics. From the theory of Cohen
forcing to slaving principles and thermodynamic process, from topoi to
decoherence-function-consistent histories, our fields have many Heyting
structures lying just an analysis away.

I am not of the opinion that the Boolean has _no_ use, nor would I even
advocate giving up the Axiom of Choice as a useful tool. But I do believe
that prior to exposing a student to these particular models of mathematical
reasoning, the more constructive foundations should be explained more
thoroughly. Because I do find that alot of misconceptions about
constructivism get propagated at times. In particular, on these newsgroups
I find that questions concerning issues particularly involved with the
general theory around applications of Heyting algebras get a much diminished
audience to that of more classical analyses of reasoning. Sometimes there
is even derision.

John Baez once stated that,

"Intuitionism proceeds by a method known as Winnowing the Audience.
Essentially, one can avoid the use of formal proofs by making the proofs so
long, tedious, and bewildering that only those in agreement bother to read
them."

Obviously, I have placed this without context, and recent comments by Baez
in support of some of Lawvere's programme may comment to possible changes in
position, but the statement is certainly indicative of a trend. Many
pop-foundations (pop-philosophy, pop-mathematics, etc.) books still mention
the various constructive schools of thought as minor players, sometimes with
actual dismissal and often without much detail. Now, this may only point to
a failing of pop books, and although I think most professionals deride the
pop books of their professions, there is certainly a community attitude that
such books commonly intend to convey.

Yet, I also find that there is quite a large group of communities using many
different faces of Heyting structures. And I find that mathematicians as a
whole do seem to appreciate constructive proofs over nonconstructive ones
where they can get them. And on some of these newsgroups I even find most
constructive expositions are well received at times. I just find that those
with a good understanding of the field are either self-trained or studied
directly under a contributer to the field, and there is often lamentation
that the field is more widely applicable. In fact, the field surely seems
more widely applicable than the study of classical Boolean logic, it being
only one form of Heyting structure and not applicable to many of the
structures mentioned or, for example, the well known theory of decidability
founded by Godel or the theory of Kleene truth.

For me, constructivist theories have always been computational theories in
general. For me, I never found anything "tedious, and bewildering" and
certainly have not noticed that it might be common to "avoid the use of
formal proofs" in intuitionism or other constructive programmes. But this
was because I read early on about intuitionism and constructivist theories
as my notions of logic were developing. By accidents of choices and
self-education, I learned constructive logics at about the same time as
learning classical logics. Certainly, constructivist math can be more
difficult since you lack some common tools for proof, and I have found
myself joking about difficulty and obscurity many times in my studies when I
first entered certain topics (like algebraic geometry and the analysis of
varieties and schemes, as an example which I still clearly remember making
similar comments), when the pantheon of objects and their transformation
structure was still poorly known by myself, and I find that quotes like
those of Baez above are often indicative of this early apprehension. So I
get concerned about education.

And these are the questions I have for all of our communities out there:

- is it, with so many applications so fundamentally related in our fields
unified by the common Heyting thread, perhaps time to start teaching our
students more about the theory of the Heyting algebra structure prior to
adding axioms forcing bivalence or existence?
- if not, why not?
- and, somewhat to get a better picture for myself, why do you believe the
more widely applicable Heyting structures and their semantic analysis is
found to be less important to the education of our students than the lesser
applicable Boolean particular case currently taught?

Obviously, I am of the "yes" opinion to the first question. For the third
question, I do see the historical contigencies that have guided modern
education, but after more than a hundred years of constructivist thought
being advocated, from early rumblings of Kroenecker and Poincare, through
Brouwer, Weyl, Heyting, Tarski, and the eventual use of the logical
structure and its semantic analysis in numerous foundational fields, and its
modern ubiquity, such explanations still seem to fail for me for modern
education. Obviously, mathematics is an easier enterprise with the
additional tools of excluded middle and transfinite choice, but again I am
not an advocate of _not_ teaching those tools. I am only curious about why
the constructive logics which seem in numerous ways to be prior to such
tools are not taught prior. They certainly can help in the understanding of
the more classical approaches. My hunch for the third question is that the
desire for classical logic is very similar to the desire to believe in
monotheism, that there is this insecurity in many people concerning the
"absolute" and "reality", and questions of truth and falseness, like
questions of good and evil, should be knowable to some form of completion.
I know that is certainly a controversial opinion in some circles, but I
wanted to throw it out there to give a better view of where I come from and
perhaps to stimulate discussion on the third topic. Paradoxically, I have
found that although I am drawn to multivalent logics and find monotheism
anathema (ironic considering the words origins), I also enjoy studying the
realist interpretations of quantum mechanics, which I suspect are guided by
very similar desires, so perhaps I just like to be contrary...

In philosophy, epistemics, cognition, linguistics, formal models,
computation, and the possible structure of our world, there are unifying
principles of expressability that I find more and more useful. It confuses
me that I find them still poorly understood in crowds where, at least to me,
it has always seemed they should be more well known. So I thought I'd try
to bring some of the more relevant communities together and see if I could
start some discussion on broadening education along these important lines,
for I feel that such is urgently needed to prevent a lot of "wheel grinding"
and repition of already known results in the separate fields. I really
believe that such a consolidation of logical education is needed in all of
our fields to place more focus on our respective advances. 

-- 
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
galathaea: prankster, fablist, magician, liar