FOM: Books, foundations, intuitionism, NF

[Torkel Franzen]

 Vaughan Pratt says:

  >I don't however see the idea of intuitionism as meaningful as originating
  >with Dummett, but rather with Heyting and Goedel.  (I would even include
  >Brouwer had his mysticism not covered his tracks so thoroughly as to
  >place his case beyond my limited competence to defend.)

  I don't think Brouwer's pronouncements about logic are all that
mystical, or all that different from Dummett's.

  A natural starting point in considering Brouwer is his famous 1908
paper on the unreliability of the principles of logic. To rely on a
set of logical principles in the sense explained by Brouwer in this
paper is to "neglect for some time the idea of the mathematical system
under construction and to operate in the corresponding linguistic
structure, following the principles." Logical principles are reliable only
if the statements thus arrived at are invariably such as can be seen
to be true provided the premisses of the argument are known to be true.

  The substance of these notions flows from a presupposition not
explicitly stated in the paper: "logic cannot deduce truths which
would not be accessible in another way as well". This is to be taken
in the strong sense that there must be associated with each statement
that can occur as the conclusion of a logical argument a notion of
how one could arrive at the truth of that statement without appealing
to the logical principles at issue. The formal machinery of logic is
applicable to a class of statements only if any statement produced
by the machinery when it has been fed with statements known to be true
can itself be seen to be true, where "being seen to be true" does not
involve the use of the machinery.

  Brouwer's notion of the logic-free arrival at the truth of a
mathematical statement was formulated in terms of "languageless
mathematical constructions". There was for Brouwer no need to
insist on the reliability of any logical principles in mathematics
(and no embarrassing second order question of how logical principles
can be known to be reliable), for just as we may cut short an
argument about the feasibility of jumping a fence by jumping, a logical
deduction is ultimately justified by carrying out a mathematical
construction.

  Of course this analogy doesn't really hold water. Negative results
in intuitionistic mathematics are particularly difficult to associate
with languageless constructions, and already Bernays pointed out that
the construction of a large natural number may well be held to be
impossible. Latter day devotees of intuitionism, like Dummett and
Prawitz, have substituted for the languageless constructions so-called
"canonical proofs", which are granted to be largely hypothetical, but
in terms of which the meaning of the statements of intuitionistic
mathematics is to be explained. A valid logical principle then
corresponds to a means of obtaining - at least "in principle" - a
canonical proof of the conclusion from canonical proofs of the
premisses. This is quite close to Brouwer's thinking.

  I would go further, and claim that Brouwer's view on the proper
place of logic make good sense even for classical logic if we adopt a
slightly larger perspective (i.e. twist the views a bit). Two such
Brouwerian observations are (i) "practical logic and theoretical logic
are applications of different parts of mathematics", and (ii) "the
function of the logical principles is not to guide arguments
concerning experience subtended by mathematical systems, but to
describe regularities which are subsequently observed in the language
of mathematics".

  Admittedly, in so far as (i) stresses the priority of mathematics
over logic and the autonomy of the former as a logic-free (because
languageless) constructive activity, it does not carry over to
classical logic and mathematics. The same goes for the distinction in
(ii) between doing mathematics and finding regularities in the
language of mathematics. From Brouwer's point of view, to follow such
regularities in the linguistic representation of mathematics without
paying attention to the structures themselves is to rely on logic, but
in seeing from an argument that a particular construction is possible
(or impossible) one need not rely on any logical principles, and in
actually performing a construction one cannot rely on any logical
principles. In classical mathematics, however, the distinction between
taking the step from "not every real number lacks property P" to "some
real number has property P" as an unreflecting application of a formal
principle and doing so while keeping the mathematical content of the
statements in mind is of doubtful significance.

  To appreciate the application of (i) and (ii) to classical logic,
notice must be taken of another saying of Brouwer's, namely that
"no assertions about the external world can be intelligently made
besides those that presuppose a mathematical system that has been
projected on the world". In accordance with this saying, he expounds
on the "mathematical element" in a syllogism as follows:

       We start by projecting in the world of perception a mathematical
       system, namely a finite set of "subjects", each of which is
       connected with some (none or one or more) elements of another
       set whose elements are called "predicates". It turns out that
       in the human intellect, a part of the world of perception can
       approximately be projected on such a system.

  I claim that whatever the value of these remarks as part of Brouwer's
sweeping account of the human intellect, they aptly characterize the
semantics of classical logic. The "verification" of the logical validity
of a form of inference in first order logic does not involve the
consideration of a variety of substitutions for the schematic letters,
but consists in observations on the order of

       if it is not the case that every individual in some domain
       fails to satisfy a certain condition, then there is at least
       one individual in the domain which does satisfy the condition.

This procedure would be grossly fraudulent if its object were to exhibit
classical logic as a system of universally valid canons of reasoning.
Brouwer tells us that to reason in terms of unspecified individuals,
domains and relations is to make a rudimentary mathematical study of
first order structures; to "apply" classical logic in reasoning about
human beings, thoughts, actions, electrons, shoes, ships, and sealing-wax
is to assume that these objects and their relations may to some degree
of approximation be thought of or represented as first-order
structures. This will indeed often be the case - partly because we like
first order logic and make sympathetic allowances for the distortions
that result when we force statements into the mold of first order
languages - but there is no reason to expect that conclusive arguments
will in general result from substitutions in valid schemata.

  Similarly the remark (ii) is quite acceptable from the point of view
of classical logic, for example as expressing the following modest
admonition: if the applicability of classical logic to some class of
statements, or some body of theory or discourse, is taken to turn on
the correctness, conclusiveness or acceptability of arguments obtained
by substituting in classically valid inference schemata, then it must be
recognized that there is no philosophical touchstone by which to judge
of the correctness of arguments. To be able to speak in any informative
way of correct, acceptable, valid or conclusive reasoning, we must
have in hand some realistic context in which reasoning of the kind under
discussion occurs. This admonition is not wholly toothless - it bears
directlyk, for example, on the interest of the harping on the law of
excluded middle as a central principle of classical logic.

  The above comments should be enough, or more than enough, to explain
why I don't think Brouwer's views on logic are mystical (although there
was no doubt plenty of mysticism in his general thinking) or alien to
classical logic. I think such splendid observations as

   logical deductions which are made independently of perception,
   being mathematical transformations in the mathematical system,
   may lead from scientifically accepted premisses to an inadmissible
   conclusion

are or can be perfectly in tune with the most devoted adherence to
classical logic.

  (I've cheated a bit in the above comments by freely mixing quotations
from earlier and later writings by Brouwer.)

---
Torkel Franzen
Computer Science, Lulea technical university