"Cool Mathematics"

From Foundations of Mathematics from the perspective of Computer Verification by Henk Barengregt:

Computations alone will not do, as there are many undecidable statements that are provably correct. Considering the Mathematical Universe as a fixed entity gives the working mathematician a strong drive, but one forgets that some properties require a lot of energy to find out (sometimes infinitely much, i.e. one cannot do it). Systems using formal intuitionism for computer mathematics, like Coq and Nuprl have found the right middle way. On the other hand, if intuitionism is considered as a philosophy that states that mathematics only exists in the human mind, one would limit oneself to what may be called in a couple of decades 'pre-historic' mathematics. True, the theories that can be fully run through in our mind constitutes romantic mathematics. But the expected results fully checked by computers that have been checked (by computers that have been checked)ⁿ by us will be cool mathematics.

...

Astronomy and biology have also had their romantic phase of going out in the fields and studying butterflies, plants and stars. The biologist at first could see everything with the naked eye. Then came the phase of the microscope. At present biologists use EM (electro-microscopy) or computers (the latter e.g. for gene sequencing). Very cool. The early astronomers could study the planets with the naked eye. Galileo started using a telescope and found the moons of Jupiter and mountains on the earth's moon. Nowadays there are sophisticated tools for observations from satellites. Again, very cool. Still, even today both biology and astronomy remain romantic, albeit in a different way. In a similar manner, the coolness of Computer Mathematics will have its own romantics: human cleverness combined with computer power finding new understandable results.

Post Holiday Update

I'm back in Boston after a lovely visit to New York. Vacations provide an excellent opportunity to pretend that you have the time to be reading the books that you shouldn't be reading, and this was no exception. I managed to get through Haskell Curry's Outline of a Formalist Philosophy of Mathematics, as well as Philip K. Dick's Ubik, and some reading on the history of science and the science wars. I received a copy of Lucky Jim which I'm about a third through and loving as well.

As a veteran couch surfer, I've found that one way to kill a day while waiting for your host to return home is to go to a library, grab a pile of random books, and just start poking through them. It was in one of these that I found the following about Alonzo Church, which I found interesting enough to share:

He looked like a cross between a panda and a large owl. He spoke slowly in complete paragraphs which seemed to have been read out of a book, evenly and slowly enunciated, as by a talking machine. When interrupted, he would pause for an uncomfortably long period to recover the thread of the argument. He never made casual remarks: they did not belong in the baggage of formal logic.

The full passage can be found here.

Colbert on Turtles

Stephen Colbert uses Catholicism to explain the "Turtles All the Way Down" philosophy:

Hear me out. I’m a Roman Catholic, the one true faith. And I know Roman Catholicism is the one true faith because Roman Catholicism tells me it is the one true faith, and if you remember from earlier in this sentence, “Roman Catholicism is the one true faith,” so how can it be mistaken?

A Modest Discipline

It is perhaps worth while saying that semantics as it is conceived in this paper (and in former papers of the author) is a sober and modest discipline which has no pretensions of being a universal patent-medicine for all the ills and diseases of mankind, whether imaginary or real. You will not find in semantics any remedy for decayed teeth or illusions of grandeur or class conflicts. Nor is semantics a device for establishing that everyone except the speaker and his friends is speaking nonsense.

From antiquity to the present day the concepts of semantics have played an important role in the discussions of philosophers, logicians, and philologists. Nevertheless, these concepts have been treated for a long time with a certain amount of suspicion. From a historical standpoint, this suspicion is to be regarded as completely justified. For although the meaning of semantic concepts as they are used in everyday language seems to be rather clear and understandable, still all attempts to characterize this meaning in a general and exact way miscarried. And what is worse, various arguments in which these concepts were involved, and which seemed otherwise quite correct and based upon apparently obvious premises, led frequently to paradoxes and antinomies. It is sufficient to mention here the antinomy of the liar, Richard's antinomy of definability (by means of a finite number of words), and Grelling-Nelson's antinomy of heterological terms.

--Alfred Tarski, The Semantic Conception of Truth and the Foundations of Semantics

A Little "Fashionable Nonsense"

The layers of this "archeology" represent, roughly speaking, a historicized form of the formalist philosophy of mathematics. Where Hilbert relied on the a priori (but ahistorical) "finitary intuition," Foucault formalizes something that romanticism called the historical a priori. In this manner, one gets a discrete sequence of historical configurations, each one being a "meta-theory" for the next. There is no continuity between these archaeological layers; they are presented as incommensurable historical facts, which ultimately makes it seem like Kant is the meta-theoretical condition of possibility of the Spice Girls--the epistemic ground on which they boogie. More seriously, the effects of this approach are nicely described by Sartre...

Vladimir Tasic, from Mathematics and the Roots of Postmodern Thought

British Syntax

This from A History of Mathematics by Carl B. Boyer. My copy was plundered from John Wiley during their move to Hoboken.

The British contributors to algebra belonging to the generation of Abel and Galois, on the other hand, set out to establish algebra as a "demonstrative science." These men were strongly affected by the fact that England's analytic contributions lagged behind those of the Continent. This was attributed to the superiority of "symbolic reasoning," or, more specifically, of the Leibnizian dy/dx notation over the fluxional dots still prevalent in England.

I find this to be rather funny, but also a bit of an object lesson. Essentially, the British blamed their analytic inferiority on bad notation. It wasn't that they lacked the machinery to do analysis, just that their representation of it was difficult to work with to the point of impeding their progress. To put it another way, they blamed their lack of achievement on bad syntax. It was beaten into me in several math classes in college that good notation leads to insight. I don't see why a programming language's syntax should be thought of any differently.

This Post is False

Via Kleene's Introduction to Metamathematics, a nice restatement of the Russell Paradox, apparently due to Russell:

A property is called 'predicable' if it applies to itself, 'impredicable' if it does not apply to itself. For example, the property 'abstract' is abstract, and hence predicable. the property 'concrete' is also abstract, and hence is impredicable. What about the property 'impredicable'?

Quine Quotes

I picked up a copy of Set Theory and Its Logic by one Willard Van Orman Quine. Few good quotes thus far (emphasis mine):

If the sentence represented by 'F x' happens to contain a quantifier capable of binding the y of 'F y', then an evasive relettering of the quantification is to be understood...

I think evasive relettering is a much more user-friendly term than α-conversion.

From the preface to the First Edition (emphasis still mine):

Because the axiomatic systems of set theory in the literature are largely uincompatiblewith one another and no one of them clearly deserves to be singled out as standard, it seems prudent to teach a panorama of alternatives. This can encourage research that may some day issue in a set theory that is clearly best. But the writer who would pursue this liberal policy has his problems. He cannot very well begin by offering the panoramic view, for the beginning reader will appreciate neither the material that the various systems are meant to organize nor the cconsiderationsthat could favor one system in any respect over another. Better to begin by orienting the reader with a preliminary informal survey of the subject matter. But here again there is trouble. If such a survey is to get beyond trivialities, it must resort to serious and sophisticated reasoning such as could quickly veer into the antinomies and so discredit itself if not shunted off them in one of two ways: by abandoning the informal approach in favor of the axiomatic after all, or just by slyly diverting the reader's attention from dangerous questions until the formal orientation is accomplished. The latter course calls for artistry of a kind that is distasteful to a science teacher, and anyway it is powerless with readers who hear about the antinomies from someone else. Once they have heard about them, they can no longer submit to the discipline of complex informal arguments in abstract set theory; for they can no longer tell which intuitive arguments count. It is not for nothing, after all, that set theorists resort to the axiomatic method. Intuition here is bankrupt, and to keep the reader innocent of this fact through half a book is a sorry business even when it can be done.