FOM: Constructive Logic and Subjectivism

[Allen Hazen]

    Stephen Simpson asks (in his role of advocatus diaboli) whether
intuitionistic logic (as appropriate to the a priori knowable) and
classical logic (about what objectively exists) can't coexist in the same
system.  They can-- there was a flurry of interest in such systems in the
1980s, under the name EPISTEMIC MATHEMATICS.  Basic idea: use classical
logic for an underlying system ("justifying" it, if need be, by talking
about the objective existence of mathematical structures).  Add a
non-truth-functional sentential operator, K, interpreted as meaning
something like "it is knowable a priori that" or "it is INFORMALLY provable
that" to the formal system, governed by the rules for necessity of the
MODAL LOGIC S4.  (References: Nicholas Goodman, "The Knowing
Mathematician," in Synthese, v. 60 (1984), pp. 21-38, argued that this was
the correct logic for an operator so interpreted (this issue of Synthese
was reissued as a book edited, I think, by Leblanc, Mendelson, and
Orenstein).)
   As pointed out by Gödel in 1932, Heyting's Intuitionistic Logic is
interpretable in classical logic with an S4 modal operator.  The proposal
was made to formulate mathematical theories in this (epistemically
interpreted) modal language, and introduce (formally) intuitionistic
connectives by definition-- so "Intuitionistic" statements would be treated
as definitional abbreviations of statements about mathematical systems AND
WHAT COULD BE KNOWN A PRIORI ABOUT THEM.  (Reference: Stewart Shapiro
edited a collection, "Intensional Mathematics," (North-Holland "Studies in
Logic" v. 113, Amsterdam, 1985) largely devoted to this idea (though also
containing some other modal- logic-and-mathematics papers).  Shapiro
contributed an introductory chapter and a chapter giving details of
"Epistemic Arithmetic," proving that Heyting Arithmetic was interpretable
in it.  Goodman, Journal of Symbolic Logic v. 49 (1984), pp. 192-203,
proved (by proof-theoretic means) that the interpretation was faithful: the
theorems of (first order) Heyting Arithmetic are PRECISELY the
abbreviations of theorems of Epistemic Arithmetic.)
   Interest then seems to have petered out: I guess the feeling was that
this gave an interpretation of constructive mathematics, but that it didn't
help in proving new or interesting  results, and nobody thought of a good
use for the parts of Epistemic Arithmetic that weren't abbreviated to
"Intuitionistic" formulas.
---
    One obvious PHILOSOPHICAL drawback of the project was that, since
Knowledge implies Truth (Kp -> p), this interpretation didn't give any
insight into the sense in which Intuitionism is an ANTI-realistic
philosophy of mathematics: all the apparent "ontological commitments" of
the classical systems are still there in their Epistemic enlargements.  My
personal contribution was to point out that, with a slight change in
translation-scheme, a weaker modal logic (the "Deontic" system D4, or even
the weaker K4, strengthened with the axiom (KKp -> Kp)) could be used,
allowing the interpretation of the operator in some way that didn't
presuppose the literal truth of "mathematically provable" sentences: I
suggested that Intuitionists might be interpreted as saying, not that there
ARE numbers, but that there OUGHT TO be (if we were in a position to
dictate ontology on the basis of our mathematical intuitions).  (Reference:
my work is in my paper in the Belnap festsschrifft, J.M. Dunn and A.K.
Gupta, eds, "Truth or Consequences," Kluwer 1990.  WARNING: I made some
mistakes in this paper, though I think my main contentions were right.  The
correct (I hope) claim about the interpretability of Heyting arithmetic in
the "Deontic" system is parasitic on Shapiro and Goodman's results. There
is also a connection I would like to understand better between this
interpretation and Mycielski's "finitizations" of infinitistic first-order
theories, which feature in Shaughan Lavine's REALLY INTERESTING book
"Understanding the Infinite" (philosophy of mathematics, informed by
history as well as by logic).)
---
  (Wild and wooly top-of-the-head stuff.)  It seems to me that Brouwer's
philosophy of mathematics was clearly "subjectivistic," and that the main
formal innovations of intuitionistic logic stem directly from that (but may
have OTHER interesting uses Brouwer wouldn't have approved of).  If
mathematics is, as Brouwer seemed to think, about his own mathematical
consciousness, mathematical EXISTENCE has to be about the contents of his
thoughts.  A number, for example, doesn't exist unless he has-- at least
implicitly-- thought of it.  And this immediately motivates the rejection
of non-constructive existence proofs: it is just FALSE to say "there is" a
number if that number can't be extracted from the thinking Brouwer went
through in reaching the existence theorem.  There are apparently (I've
forgotten the reference) proper extensions of Heyting's logic that have
"the existence property," but Heyting's logic is at least the most natural
and neatest formalization of this subjective view of mathematical truth.
   But why is Brouwer the "subject"?  Quite independently of Brouwer,
various philosophers in the 1960s and 1970s attacked the idea that
mathematical knowledge is A PRIORI on the grounds that mathematicians
depend on things they have been told by their colleagues: even the best
mathematician is unlikely to have verified personally all the lemmas of a
new theorem.  (Up-to-date expositions of this line of thought would mention
the 4-color theorem and the classification of simple groups.)  But there is
CLEARLY some sense in which mathematics is a priori.  Perhaps, if we are to
say that mathematics is a priori, we should say that the MATHEMATICAL
SUBJECT is, not an individual, but the mathematical community. So, next
stage....
   Dummett, whose philosophical training was from students and followers of
Wittgenstein, is very conscious of language as something COMMUNAL or
SOCIAL, and is not at all sympathetic to the idea of the isolated EGO as a
subject.  But it seems to me that his philosophy of mathematics (on his
intuitionistic days-- he does frequently express caution and uncertainty
about his pro-intuitionistic arguments, and what little I know about him as
a person makes me think these are sincere) is just as "subjectivistic" as
Brouwer's: it's just that the "subject" is the mathematical community or
tradition.  Not surprisingly, the difference doesn't seem to have much
influence on the formal logic or mathematical principles.
   Perhaps (this is speculation-- I have never tried to work out the
details, and know of no one else who has) much the same mathematics and
logic could be motivated by MATERIALISM or Nominalism: numbers (etc) can
only meaningfully be said to exist if they or a representation of them is
implicitly present in the material world.
    The idea of something being IMPLICIT does a lot of work in all these
approaches; it is not obvious that a subjectivist (either individual or
social) or materialist/nominalist is really entitled to it.  Some of
Dummett's critics have argued that his arguments lead, not to intuitionism
but, to STRICT FINITISM: the idea that there is a largest natural number....
   Interest in formally intuitionistic systems from computational types
doesn't imply that THEY are subjectivists.  The features of intuitionistic
systems that interest them, however, are the same as the features that
appeal to a subjectivist philosopher.  The extraction of an algorithm from
a constructive proof is formally the process a subjectivist would describe
as the making explicit of what was implicit in the mathematical thoughts in
the proof.  (But this is only a vague, impressionistic, claim.  PERHAPS in
the context of a formal semantics a precise notion of "implicit" could be
defined, and theorems proven-- but I certainly haven't done it.)