From: pratt@Sunburn.Stanford.EDU (Vaughan R. Pratt)
Subject: Re: Russell's Paradox (was re: Of apples and their skins)
Organization: Computer Science Department,  Stanford University.
Date: Fri, 16 Oct 1992 23:58:22 GMT

In article <MARTINC.92Oct10200731@grover.cs.unc.edu> martinc@grover.cs.unc.edu (Charles R. Martin) writes:
>I love it.  We have had, in roughly a month and in one news group, the
>formalist, "realist", Platonic, and intuitionist approach to
>foundational issues espoused.  Can't we find a good constructivist to
>jump in and complete the set?

This is comparing apples and oranges.  A constructivist can reasonably
be construed to mean anyone with a dislike for nonconstructive proofs.
One doesn't have to have even heard of intuitionism to be a
constructivist.  The head of Sydney's computer science department for
upwards of three decades, John Bennett, was a confirmed constructivist,
but I'm not aware that he ever looked seriously into logical
frameworks.

Intuitionism as it has evolved today provides a good logical framework
for constructivists.  If you have a nonconstructive proof that a
certain x exists, intuitionistic logic lets you say that it is nonsense
for x not to exist ("not not exists x"), without compelling you to
treat this as identical to "x exists".  I like to pronounce "not not"
as "surely."  Boolean logic is inflexible in insisting that "surely" is
vacuous, namely the identity.  This shows the advantage of
intuitionistic logic over Boolean: it lets you prove everything a
classical logician could prove, while preserving such distinctions as
constructive vs.  nonconstructive proofs of existence in a way that
classical logic cannot.

In his book "The Emperor's New Mind," Roger Penrose says "If we go
along with intuitionism, we must deny ourselves the use of very
powerful kinds of argument within mathematics, and the subject becomes
somewhat stifled and impotent."  This perpetuates the myth that
intuitionistic logic is less expressive than classical, when in fact
classical proofs can be faithfully translated into intuitionistic
proofs, with the "surely"'s that classical logic glosses over properly
reinstated.

A variant of constructivism permits only *effective* constructions,
e.g. via partial recursive, recursive, or more extremely
polynomial-time-computable functions.  The sentiment here is that a
construction is of no use if it cannot be carried out.

Another variant of constructivism focuses on reasons rather than
constructions.  In this variant A is said to entail B *constructively*
when not only do we know *that* B follows from A but *how*.  We then
interpret the entailment A |- B not as a truth value (0 or 1) but as
the set of proofs of B that become possible when A is available.  If we
identify those proofs that can be interconverted by proof normalization
we end up with a notion of abstract proof that is formally equivalent
to the notion of morphism in a category, making proof theory a branch
of category theory.

Yet another form of constructivism emphasizes relevance: we may only
claim that A entails B when A is actually used in an essential way in
proving B.  This is catered for by Anderson and Belnap's relevance
logic.  Linear logic further strengthens relevance logic by requiring
that every premise be used not merely at least once but *exactly*
once.

Literature:
Troelstra, "Aspects of Constructive Mathematics", in
Barwise, "Handbook of Mathematical Logic," North-Holland, 1977.
Beeson, "Foundations of Constructive Mathematics", Springer-Verlag, 1985.
Nerode and Odifreddi, "Lambda Calculi and Constructive Logics", to appear.
-- 
Vaughan Pratt   pratt@cs.Stanford.EDU     exp(n pi sqrt(163)/3) for n=1..30