Every time I read something by an intuitionist, I get the impression
that the writer is either unable or unwilling to distinguish between
the notions of truth and decidability. On the other hand I’ve never
read anything that says this, either by an intuitionist claiming that
there is no difference; or by a critic criticising the intuitionist’s
lack of appreciation of the difference. The closest I’ve seen is a
claim that intuitionistic logic is a modal logic of "provability".
So have I just missed these writings or aren’t there any such? If
not, why don’t intuitionists argue that there is no difference between
truth and decidability, or argue that logic should not be concerned
with truth, or do something similar that shows at least that they
understand the difference between the two concepts? Surely this would
be better than just offering an argument on the non-validity of the
law of the excluded middle based on an undecidable property. To me at
least, these arguments have always looked a bit silly.
—
David Gudeman
gude…@cs.arizona.edu
David Gudeman writes:
>Every time I read something by an intuitionist, I get the impression
>that the writer is either unable or unwilling to distinguish between
>the notions of truth and decidability.
Speaking as a rank amateur in this area, my impression has always been
that intuitionists consider the usual mathematical notion of "truth" as
distinct from "what we can prove" or "what we know" to be nonsense.
Have you looked in Brouwer’s original writings?
—
Ian Sutherland
i…@eecs.nwu.edu
Sans Peur
In article <1voc1o$…@optima.cs.arizona.edu> gude…@CS.Arizona.EDU
(David Gudeman) writes:
>Every time I read something by an intuitionist, I get the impression
>that the writer is either unable or unwilling to distinguish between
>the notions of truth and decidability.
Intuitionistically, mathematical statements are understood and
explained in terms of proofs (in a sense not reducible to derivations
in any formal system). Thus a reflection such as "Even if Poincare’s
conjecture is true, there is no guarantee that it can be proved" makes
no sense on an intuitionistic interpretation of Poincare’s conjecture.
You might try looking at something which contains a fuller description:
say Beeson’s "Foundations of Constructive Mathematics" (Springer-Verlag, 1985)
or Errett Bishop’s papers. There are several brands of constructive
philosphies, of which intuitionism is only one. Some sort of comparison,
like Bridges and Richman "Varieties of Constructive Mathematics"
(Cambridge University Press, 1987) might help put it into perspective.
The more or less original complaint had to do with impredication. This
critcism was due to Poincar\’e's criticisms as well as Brouwer’s. Don’t forget,
though, that "intuitionism" goes back to Kant and emerges through
Dedekind, Kronecker, etc. It was Kronecker who make the comment "The integers
are the work of God, all else is the work of man." A fascinating account of
all this is in Kline’s "Mathematics: the loss of certainty" (Oxford University
Press, 1980).
steve
—
===============================================================================
Steve (really "D. E.") Stevenson st…@hubcap.clemson.edu
Department of Computer Science, (803)656-5880.mabell
Clemson University, Clemson, SC 29634-1906
|> >Every time I read something by an intuitionist, I get the impression
|> >that the writer is either unable or unwilling to distinguish between
|> >the notions of truth and decidability.
My favorite quote in this area, is from one of the more reputable exponents of
intuitionism in its most minimal, merely "constructivist" form: Errett Bishop.
In his own words…
"Nothing is true unless and until it has been proved".
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Bishop is not usually so combative; but if this thought is essential to
constructivism/inuitionism, (which is arguable), it will probably remain
for ever beyond the pale, for most working mathematicians.
——————————————————————————
Bill Taylor w…@math.canterbury.ac.nz
——————————————————————————
Clarity is complementary to truth. (Niels Bohr)
——————————————————————————
In article <C8sn5p….@cantua.canterbury.ac.nz> w…@math.canterbury.ac.nz
(Bill Taylor) writes:
>"Nothing is true unless and until it has been proved".
>Bishop is not usually so combative; but if this thought is essential to
>constructivism/inuitionism, (which is arguable), it will probably remain
>for ever beyond the pale, for most working mathematicians.
I don’t think it’s a good idea to use "intuitionism" and
"constructivism" interchangeably. There are many differences between
constructivist schools, and "intuitionism" is in the literature
usually associated with the doctrines of Brouwer, who invented the
term.
Pronouncements such as the one you quote admit various interpretations.
On one interpretation the quoted statement is incompatible with
intuitionism, since computational statements are held to be true or
false in intuitionism, whether or not they will ever be proved or
disproved.
In article <C8sn5p….@cantua.canterbury.ac.nz> w…@math.canterbury.ac.nz (Bill Taylor) writes:
>My favorite quote in this area, is from one of the more reputable exponents of
>intuitionism in its most minimal, merely "constructivist" form: Errett Bishop.
>In his own words…
>"Nothing is true unless and until it has been proved".
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Does this appear in his writings somewhere?
Or was it "off the record"?
Or was he being deliberately provocative?
–
Alan Smaill JANET: sma…@uk.ac.ed.lfcs
LFCS, Dept. of Computer Science UUCP: ..!mcvax!ukc!lfcs!smaill
University of Edinburgh ARPA: sma…@lfcs.ed.ac.uk
Edinburgh EH9 3JZ, UK. Tel: 031-650-5189
|> >"Nothing is true unless and until it has been proved".
|> > ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|> Does this appear in his writings somewhere?
|> Or was it "off the record"?
|> Or was he being deliberately provocative?
Yes.
No.
Probably!
It appears quite specifically, as above, in a sentence about a standard
constructivist type of example concerning "fugitive sequences".
You can find it in "Foundations of Constructive Analysis" , Errett Bishop,
Chapter 2 section 2, (page 26 in our copy). In the 3rd-last paragraph.
I think Bishop is probably being a little bit provocative, just to make the
reader consider the meaning of the example carefully.
I’m sure he would be prepared to admit some kind of abtract difference between
truth and provability; if straightly tackled. But I could be wrong.
Anyway, the above quote is definitely what he *says*, and most of us would
never be able to swallow it.
——————————————————————————
Bill Taylor w…@math.canterbury.ac.nz
——————————————————————————
Clarity is complementary to truth. (Bohr)
——————————————————————————
In article <C91wJ4….@cantua.canterbury.ac.nz> w…@math.canterbury.ac.nz
(Bill Taylor) writes:
>I’m sure he would be prepared to admit some kind of abtract
>difference between truth and provability; if straightly tackled.
>But I could be wrong.
The statement you quote goes much further than the identification of
truth and provability, since he says that a statement is only true
when it *has* been proved. This is on the face of it incompatible with
intuitionism. However, that all true statements are provable is
indeed basic to intuitionism. This is not an article of faith, but a
consequence of the intuitionistic interpretation of mathematical
statements.
In article <TORKEL.93Jun23095…@anhur.sics.se> Torkel Franzen writes:
]In article <C91wJ4….@cantua.canterbury.ac.nz> w…@math.canterbury.ac.nz
] (Bill Taylor) writes:
]
] The statement you quote goes much further than the identification of
]truth and provability, since he says that a statement is only true
]when it *has* been proved. This is on the face of it incompatible with
]intuitionism.
But that was exactly Brouwer’s contention. He said something like "to
say that a fact is true is to say that I _have_ made a mental
construction of it" [underscores are mine. I could look this up and
give an actual quote if anyone asks.] However, Brouwer’s writing shows
clearly that he was as capable as anyone of using the classical notion
of truth, as he often used this notion (that is, he made statements
whose truth conditions were clearly classical) when trying to explain
intuitionism. Heyting even went so far as to claim that it is not a
problem that mathematical truths can become true that were not true
before (I seem to recall that Brouwer acknowledged this as a problem
and had some sort of solution, but I can’t recall what it was).
]However, that all true statements are provable is
]indeed basic to intuitionism. This is not an article of faith, but a
]consequence of the intuitionistic interpretation of mathematical
]statements.
As an amusing aside, I suggest that these intuitionists who are so
concerned with finiteness are commited to an infinite number of
propositions for each proposition that they prove. If for all
propositions P, P <=> constructable(P), then
P => constructable(P) => constructable(constructable(P)) => …
In fact one could argue that an intuitionist cannot prove P without
first proving the infinite formula that is the limit of the above
chain, and then working back.
—
David Gudeman
gude…@cs.arizona.edu
In article <20afrh$…@optima.cs.arizona.edu> gude…@CS.Arizona.EDU
(David Gudeman) writes:
>But that was exactly Brouwer’s contention. He said something like "to
>say that a fact is true is to say that I _have_ made a mental
>construction of it" [underscores are mine.
Yes, that is the content of a mathematical assertion, according to
Brouwer. However, it is true intuitionistically e.g. that "p is a prime"
is true or false, whether or not "p is a prime" is ever actually
proved or disproved (or any "construction" effected, in Brouwer’s
terminology). We know this intuitionistically on the basis of a proof
that establishes that such a construction "can" be made.
>However, Brouwer’s writing shows
>clearly that he was as capable as anyone of using the classical notion
>of truth
Brouwer’s work in topology was classical mathematics.
>As an amusing aside, I suggest that these intuitionists who are so
>concerned with finiteness are commited to an infinite number of
>propositions for each proposition that they prove.
Intuitionists, unlike finitists, are not particularly concerned with
finiteness. On the contrary, Brouwer’s intuitionistic mathematics is
highly infinitistic.
In article <TORKEL.93Jun23233…@anhur.sics.se> Torkel Franzen writes:
]In article <20afrh$…@optima.cs.arizona.edu> gude…@CS.Arizona.EDU
](David Gudeman) writes:
]
] >But that was exactly Brouwer’s contention. He said something like "to
] >say that a fact is true is to say that I _have_ made a mental
] >construction of it" [underscores are mine.
]
] Yes, that is the content of a mathematical assertion, according to
]Brouwer. However, it is true intuitionistically e.g. that "p is a prime"
]is true or false, whether or not "p is a prime" is ever actually
]proved or disproved (or any "construction" effected, in Brouwer’s
]terminology). We know this intuitionistically on the basis of a proof
]that establishes that such a construction "can" be made.
But I claim that this concept is not available to Brouwer. If P means
"I have proved P", then P\/Q means "I have proved that I have proved P
or I have proved Q". That is, if Brouwer’s account is to be taken
seriously, then one can’t say P\/Q unless and until one has actually
proven either P or Q. The problem is Brouwer’s insistence that
something is not true until it _has_ been proved. This is a weaker
notion than "can be proved". (footnote: and in fact, after making
this observation I should retract my statement that intuitionist logic
is a logic of provability. According to Brouwer it has an even weaker
notion of truth than that). Brouwer is _not_ entitled to claim that
P\/Q means "I have proved that P or Q can be proven" because the
notion that something "can be proven" is not available to him. He
only has access to the notion of "has been proven".
Brouwer’s very weak notion of truth comes from his strong
conceptualist metaphysics. Since math is (according to Brouwer) about
psychological entities, nothing can be true unless and until it has
been mentally "constructed". Yet although Brouwer talked a good game,
I don’t think he was able to remain consistent with his own acount,
for the very good reason that his account is wrong and doesn’t
describe mathematics at all. Brouwer claims that P is true if and
only if P has been proven, but in order to describe and defend his
views, he makes classical statements about P, and this proves that he
understands the classical statements, that he regards them as
meaningful, and that he regards their truth conditions to be reliable
enough to explain his own conditions of truth. In this sense, he
validates classical logic, so he has no business retreating to a
weaker notion of logic. (and I promised myself that I wouldn’t get
dogmatic about this on the net
] >As an amusing aside, I suggest that these intuitionists who are so
] >concerned with finiteness are commited to an infinite number of
] >propositions for each proposition that they prove.
]
] Intuitionists, unlike finitists, are not particularly concerned with
]finiteness. On the contrary, Brouwer’s intuitionistic mathematics is
]highly infinitistic.
I was refering to Brouwer’s limitations on infinity, such as his
unwillingness to beleive in non-denumerable infinities. He allows the
infinite "processes" but only if they can be finitely represented
(classical mathematicians, on the other hand, recognize the existence
of things that cannot be represented). Clearly this does not rule out
a well-behaved infinite sequence of propositions such as I described,
but Brouwer’s penurious notion of infinity contrasts ironically with
the fact that he needs to engage in an infinite process to prove
anything (if you believe my argument on this point).
—
David Gudeman
gude…@cs.arizona.edu
In article <20fo3n$…@optima.cs.arizona.edu> gude…@CS.Arizona.EDU
(David Gudeman) writes:
>But I claim that this concept is not available to Brouwer. If P means
>"I have proved P", then P\/Q means "I have proved that I have proved P
>or I have proved Q".
P doesn’t mean "I have proved P". Brouwer’s statement refers to a
mathematical assertion: in asserting P, I claim that I have "carried out"
a certain construction. This does not mean that P and "I have proved P"
are interchangeable. For example, the content of "if P then Q" is not
"if I have proved P then I have proved Q".
>The problem is Brouwer’s insistence that
>something is not true until it _has_ been proved. This is a weaker
>notion than "can be proved".
You mean stronger, surely. If P has been proved, then P can be proved.
>I was refering to Brouwer’s limitations on infinity, such as his
>unwillingness to beleive in non-denumerable infinities.
It is a theorem of Brouwer’s intuitionistic mathematics that the
continuum is non-denumerable.
In article <C8sn5p….@cantua.canterbury.ac.nz>
w…@math.canterbury.ac.nz (Bill Taylor) writes:
|My favorite quote in this area, is from one of the more reputable exponents of
|intuitionism in its most minimal, merely "constructivist" form:
| Errett Bishop.
|
|In his own words…
|
|"Nothing is true unless and until it has been proved".
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In <C8yovB….@dcs.ed.ac.uk> sma…@dcs.ed.ac.uk (Alan Smaill) writes:
|Does this appear in his writings somewhere?
|Or was it "off the record"?
|Or was he being deliberately provocative?
I’m don’t know whether it was intended to be provocative.
People might want to read an essay called something like "Can the
Philosophy of Mathematics tell us anything about Mind?" which can be
found in a collection titled _The Invented Reality: How do we know
what we believe we know?_. The title is probably not accurate; the
book is currently checked out of our library here.
One should be careful when thinking about intuitionism, and
constructivism in general. One of the major wrinkles, it would seem,
is due to their having a different conception of what a proposition
*is* (or perhaps one could put it, what an act of asserting a
proposition consists in). There is an essay by Dummett in Benacerraf
and Putnam’s volume of readings in the philosophy of mathematics,
which may help to explain it somewhat.
One can ask oneself, what exactly do we mean by a mathematical
assertion qualified with a tense (saying it was true at a given time)?
Is this perhaps a merely semantic issue?
Bishop’s quote would appear to conflict with the acceptance of claims
such as "either (a) there are 1,000,000 positive integers n such that
(3/2)^n has fractional part <1/2, or (b) there are 1,000,000 positive
integers n such that the fractional part of (3/2)^n is >1/2," since,
as far as I am aware, neither (a) nor (b) has already been proven. It
is not clear to me that there really is a conflict, however. This
example is discussed from the point of view of a constructive(-ist)
mathematician in the "Does the philosophy…" essay I mentioned
above. One of the key points is that one has simply taken "either (a)
or (b)" to *mean* that we have, now, a procedure which would, if
executed, yield a demonstration of one of (a) or (b) (e.g. computing
the fractional part of (3/2)^n for n=1 through n=1,999,999 and
counting how many of the fractional parts fall in each category).
I would personally have been rather wary, had I been in Bishop’s
shoes, of using such language, without more explanation, but that’s
based on my impressions of how such things would be received.
Hindsight is 20-20.
Keith Ramsay
ram…@unixg.ubc.ca
In article <ramsay.741050…@unixg.ubc.ca> ram…@unixg.ubc.ca
(Keith Ramsay) writes:
>People might want to read an essay called something like "Can the
>Philosophy of Mathematics tell us anything about Mind?" which can be
>found in a collection titled _The Invented Reality: How do we know
>what we believe we know?_. The title is probably not accurate . . .
The title of the book is accurate: _The Invented Reality: How Do We
Know What We Believe We Know? (Contributions to Constructivism)_
edited by Paul Watzlawick (Norton, 1984). My hardback copy has a
reproduction of Magritte’s "The Heart of the World" on the cover of
the dustjacket (painting of a massive unicorn’s head topped by a tower).
The essay Mr Ramsay refers to is "Can an Inquiry into the Foundations
of Mathematics Tell Us Anything Interesting About Mind?" by Gabriel
Stolzenberg, pp. 257-308.
–
Marko Amnell
amn…@klaava.helsinki.fi
>w…@math.canterbury.ac.nz (Bill Taylor) writes:
>|In his own words…
>|
>|"Nothing is true unless and until it has been proved".
>| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Just curious… do you reckon the double negation here is on purpose?
—
Annius V. Groenink phone (private): +31 30 895261
Mathematics/Computer Science e-mail: avgro…@cs.ruu.nl
University of Utrecht groen…@math.ruu.nl
Netherland ZFC Computing ann…@zfc.nl (dreamtime only)
In article <TORKEL.93Jun25235…@anhur.sics.se> Torkel Franzen writes:
]
]In article <20fo3n$…@optima.cs.arizona.edu> gude…@CS.Arizona.EDU
](David Gudeman) writes:
]
] >But I claim that this concept is not available to Brouwer. If P means
] >"I have proved P", then P\/Q means "I have proved that I have proved P
] >or I have proved Q".
]
] P doesn’t mean "I have proved P". Brouwer’s statement refers to a
]mathematical assertion: in asserting P, I claim that I have "carried out"
]a certain construction. This does not mean that P and "I have proved P"
]are interchangeable. For example, the content of "if P then Q" is not
]"if I have proved P then I have proved Q".
That is a reasonable position, but I don’t think it is one that
Brouwer would accept, not as to disjunction anyway. After all, how
can you prove P or Q without knowing which one you have proven? I
think the only way for this to happen is to offer a proof that is
either a proof of P or of Q, but you don’t know which one it is.
As to implication, I think Brouwer’s interpretation is that the proof
of P "leads to" a proof of Q in some sense. This is not really
expressible by modifying material implication.
] >The problem is Brouwer’s insistence that
] >something is not true until it _has_ been proved. This is a weaker
] >notion than "can be proved".
]
] You mean stronger, surely. If P has been proved, then P can be proved.
I guess it depends on how you intend the stength analogy to be
understood.
] >I was refering to Brouwer’s limitations on infinity, such as his
] >unwillingness to beleive in non-denumerable infinities.
]
] It is a theorem of Brouwer’s intuitionistic mathematics that the
]continuum is non-denumerable.
I went back and found Brouwer’s paper that lead me to this comment and
on rereading it, I see that I mis-understood. He denies the
comprehensibility of several specific statements about non-denumerable
infinities, but does not deny the comprehensibility of all such
statements.
—
David Gudeman
gude…@cs.arizona.edu
In article <20nstm$…@optima.cs.arizona.edu> gude…@CS.Arizona.EDU
(David Gudeman) writes:
>That is a reasonable position, but I don’t think it is one that
>Brouwer would accept, not as to disjunction anyway. After all, how
>can you prove P or Q without knowing which one you have proven? I
>think the only way for this to happen is to offer a proof that is
>either a proof of P or of Q, but you don’t know which one it is.
>As to implication, I think Brouwer’s interpretation is that the proof
>of P "leads to" a proof of Q in some sense.
Every mathematical assertion refers to a "construction": what kind
of construction this is depends on the form of the assertion. This was
the basic idea amplified by Heyting in his formalization of
intuitionistic logic. In the later philosophical literature (Dummett
et al.) these constructions are referred to as "canonical proofs".
Thus a canonical proof of an implication "if P then Q" is a "method"
(sometimes "function") that applied to a proof of P yields a proof of
Q, a canonical proof of "P or Q" is a canonical proof of P or a
canonical proof of Q. A proof of a statement in the ordinary
mathematical sense – sometimes called a demonstration – establishes,
to our intuitive satisfaction, the existence of a canonical proof of
the statement. This is not normally done by actually exhibiting a
canonical proof, but by showing that a canonical proof "can" be
exhibited. Thus Brouwer was content to note that e.g. in the case of a
question of the form "is p a prime?", the corresponding construction
"can always be carried out", and that the statement is therefore known
to be true or false. Thus we can prove a statement "P or Q" in
mathematics, on this view, without producing either a proof of P or a
proof of Q.
It is true that the distinction between canonical proofs and
demonstrations is not infrequently blurred, particularly in polemical
contexts, but it is implicit in the acceptance of intuitionistic logic
as a valid means of obtaining mathematical knowledge. Consider the
demonstration, formalizable in Heyting arithmetic, by which "p is a
prime or p is not a prime" is established. This proceeds by first
giving an inductive proof of "for every n, n is a prime or n is not a
prime". This can indeed be regarded as exhibiting a method that,
applied to any n – or more explicitly, to a construction establishing
that n is a natural number – yields a canonical proof of "n is a
prime" or of "n is not a prime". But then we apply universal
quantifier elimination to conclude that p is a prime or p is not a
prime. This certainly does not amount to applying the exhibited method
to (the construction of) p, since we can’t do this (for large p).
The demonstration is valid, intuitionistically, because it convinces us
that such an application "can" be made even though it will never be
true that it has been made.