FOM: Intuitionism, Godel

[Harvey Friedman]

Reply to Pratt 7:24PM 3/7/98

>Encouraged by Torkel Franzel, I took a closer look at your quotation
>of Goedel (a 1932 review of Heyting's "The intuitionist's way of
>founding mathematics", 1931) and now do not see how you infer from
>the quotation rejection by Goedel of *any* aspect of intuitionism.

I didn't say it was from there. You'll find it in his philosophical papers
in the Collected Works.

> Nowhere in this
>famous paper is there the slightest hint of rejection of intuitionism,
>to the contrary it is hard to see how to take it as other than strong
>technical support for intuitionism.

Not after you read his philosophical papers in the Collected Works.

>What are the "great many writings" that you had in mind?

His philosophical papers in the Collected Works. My "great many" was of
course silly.

There are plenty of better historical experts on Godel than me on the fom,
and they can set you straight on this.

Pratt 8:06PM 3/7/98:

>For myself I fully support the thesis that intuitionistic logic is no less
>meaningful a logic than classical, as I hope my recent postings in this
>thread made clear (but my support could have been phrased more crisply).

This is at the present state of knowledge, an absurd thesis which is, I
think, based on perhaps a milder misunderstanding of foundations than the
one that causes you to frequently confuse various algebraic studies with
logic. I've never seen a coherent philosophical account of, say, iterated
intuitionistic implication. All attempts are quite clumsy. Completeness
theorems, even to this day, are quite awkward and unconvincing - despite
some new ones I developed. And if classical f.o.m. frustratingly leaves
basic questions open, then intuitionistic f.o.m. in comparison settles
virtually nothing. These are just some of the comparisons. Nevertheless,
intuitionism still has a kind of formal coherence, and constructivity a
kind of intellectual coherence, at least sufficient to be useful in various
contexts, and to make it worthwhile to turn it into something truly
coherent. The mathematics community never bought into it, preferring to
phrase related issues in totally classical terms - e.g., is there an
algorithm or decent bound for such and such. Falting's theorem is grossly
nonconstructive in content and proof right now. It has the form that
something is true in the integers with finitely many exceptions, without a
bound on the number of exceptions, and certainly not a bound on the size of
the exceptions. The same with Roth's theorem on approximations to algebraic
numbers. And mathematicians accepted this as great mathematics without
hesitation. They do know about the problem of getting bounds and
algorithms, and respect this problem - but avoid phrasing it in terms of
intuitionism or constructivity.

>I also don't see intuitionistic logic as the end of the line in that
>progression.  *The* end of the line is linear logic, there is nothing
>beyond it in the same sense that, going in the other direction, there
>is nothing beyond classical logic.  Classical and linear logic are the
>endpoints in a spectrum of logics that range from the logic of pure
>separation to its dual logic of pure connection.  Intuitionistic logic
>lives within that interval, close to the classical end.

This is an illustration of the confusion between algebra and logic that I
spoke of above. Although one can study profitably Heyting Algebras, this
algebraic construction and study is not what is at the essence of
intuitionism and constructivity. They are not algebraic at all. They are
proof theoretic or semantic or logically formal or a mixture of these; but
they are not algebraic studies.