What is Reddit's opinion of From Frege to Godel: A Source Book in Mathematical Logic, 1879-1931 (Source Books in History of Sciences)?

From 3.5 billion Reddit comments

You remind me a lot of myself when I was younger.

I actually have a Masters in Logic from the Institute for Logic, Language and Computation in Amsterdam.

This is one of the finest places in the world to go if you want to learn about the intersecting area of abstract mathematics, computer science, linguistics and philosophy. Also it's easy to win a Huygens grant, so you should consider applying since going to graduate school for free is ideal.

You should also consider the following summer programs:

• CMU's Summer School in Logic and Formal Epistemology
• European Summer School in Logic, Language and Information

I strongly encourage you to go to both of these summer schools if you haven't already; they're extremely fun :D

Comparable programs to the ILLC include CMU's Masters in Logic and CUNY's logic program. When I looked into these I didn't find funding to be as easy to get, you should take that into account.

My MSc thesis was pretty typical for people at the ILLC concentrating in mathematics. It consisted of a family of logics of my own invention and elaborate completeness proofs. My adviser (then the head of the department) was largely absentee because I was only obliquely working on his personal research program. You will generally find your life in academia difficult if you are fiercely independent. Anyway, because my advisor kind of sucked I formally verified the correctness of my work in Isabelle/HOL to make sure it was correct. If I could do it again, I would have done it in Coq; Adam Chlipala of MIT has an excellent book here for learning Coq if you are interested.

As I have said elsewhere, you will find that if you attempt to formally verify mathematics you are learning in your classes that your professors generally lack the rigor necessary for these systems. Do not tell them this, they will not believe you.

Of my peers at the ILLC only 1 in 20 people seem to have gone on to academia. Frankly my female friends have all been more successful than my male friends. You should be well aware that burnout is extremely common in theoretical computer science, it hits men harder than women for some reason. The longer you stay in the deeper the dive when you burn out from what I can tell. People who cut out early quickly got jobs in finance. But I had a buddy at a PhD in Stanford who was homeless for a year when he burned out (he finished his PhD and now he's in industry). Other people who burn out just fall into depression and have to live with their families and so on. One dude just landed a job at McKenzie as a consultant which is probably the ideal failure mode :D

When I burned out I was depressed. During that gap year I just plowed through Griffith's books on quantum mechanics and electrodynamics desperately trying to teach myself physics for some reason, formally verified the correctness of Cayley's theorem (also the little known contravariant Cayley embedding they don't teach you in algebra class for some reason), invented a few more logics which I tried to publish (and failed lol) and worked on satellite technology to fill the void. But I was all beta and self-loathing and hating myself for wasting my life with shit, which is apparently rather common.

Then I got into EECS PhD program at a good US university, which I dropped out of after getting a Masters.

While I was there I mostly took machine learning courses.

This has opened doors.

Computational statistics, machine learning, digital signal processing and even old-fashioned 90s artificial intelligence are excellent subjects to study if you want to get a job in industry, especially finance.

You'll get more jobs if you learn clojure than haskell, I've met lots of folks who've fallen from the ivory tower and end up having to program clojure even when they are secretly haskell ninjas. But you'll get even more jobs once you let go and learn to program in whatever.

You are clever and you should basically have the confidence that you can learn on the job to program anything.

You are not statistically likely to make any more money in your lifetime if you get a PhD in Computer Science rather than a masters, by the way. Consider taking this into account as you make your life choices.

With a masters in CS from a good university I have lots of job offers. If you situate yourself right you'll have Amazon and Google knocking on your door all the time. You'll be happy to know there are a number of teams at Google that program haskell :D

Right now I am doing consulting work at MIT on satellite a mission to find planets around other stars (both the science and the engineering). Being a good programmer as well as a scientist means that MIT will pay for all my meals, fly me to conferences in exotic places, gives profound job security, and six figures at 60% time (I am working on a startup in my spare time).

▶︎ Knowing mathematics and theoretical computer science doesn't open doors for me, knowing regular science and programming is what opens all my doors now. ◀︎

But of course you are on your own journey, your milage may vary.

Anyway, you seem to still be in the phase of your life where you are into logic, so I'll give advice on what books to read. I assume you've read Hofstadter's Gödel, Escher, Bach: An Eternal Golden Braid. After that most of us go on to read Jean Heijenoort's Source Book after that since you're clever and you should consider reading Gödel's original proof of his incompleteness theorem when you are ready. After that I would recommend reading Boolos' Logic of Provability and Hersh's 18 Unconventional Essays on Mathematics.

I really wish you the best of luck, I'm sure you're going to go to some interesting places.

But for Christ's sake learn how to program.

You're going to need to get a fucking job in the real world if you theory stuff doesn't work out, okay?

Have a backup plan, making up one as you go kind of sucks.

There's a 1966 book by Jean van Heijenoort that has many of the original talks and writings pertaining to the Hilbert/Brouwer debate. I think that the most interesting (philosophically) is a short note by Hermann Weyl (Hilbert's student who defected to intuitionism and then recanted), in 1927, that explains why both Brouwer and Hilbert are right.

Before posting Weyl's remarks, I'll quote some pertinent bits from Brouwer and Hilbert. As we'll see, Weyl said that all mathematicians were intuitionists, or thought they were, but it was Brouwer who discovered just how much of math was untenable from the intuitionistic point of view. He basically said that much of math was wrong:

Brouwer 1923:

> An incorrect theory, even if it cannot be inhibited by any contradiction that would refute it, is nonetheless incorrect, just as a criminal policy is nonetheless criminal even if it cannot be inhibited by any court that would curb it. … In view of the fact that the foundations of the logical theory of functions are indefensible according to what was said above, we need no be surprised that a large part of its results becomes untenable in the light of more precise critique.

It was Hilbert (the finitist!) who, according to Weyl had to make a radical philosophical jump in order to salvage mathematics, and he who had to defend his position. In 1927, in a talk where he personally lambasted Brouwer (and expressed surprise that he has a following), he explained that math contains "real propositions" with actual content as well as "ideal propositions". Hilbert first claims that his position is defensible in the tradition of math, but says it has two concrete advantages: it can save analysis, and its formal proofs are aesthetically more appealing as they're shorter, more elegant, and distill the essence of the idea of the proof.

> [E]ven elementary mathematics contains , first, formulas to which correspond contextual communications of finitely propositions (mainly numerical equations or inequalities, or more complex communications composed of these) and which we may call the real propositions of the theory, and, second, formulas that — just like the numerals of contextual number theory — in themselves mean nothing but are merely things that are governed by our rules and must be regarded as the ideal objects of the theory.

> These considerations show that, to arrive at the conception of formulas as ideal propositions, we need only pursue in a natural and consistent way the line of development that mathematical practice has already followed till now.

> ... [W]e cannot relinquish the use of either the principle of excluded middle or of any other law of Aristotelian logic expressed in our axioms, since the construction of analysis is impossible without them.

> ... [A] formalized proof, like a numeral, is a concrete and survivable object. It can be communicated from beginning to end.

> ... What, now, is the real state of affairs with respect to the reproach the mathematics would degenerate into a game?

> The source of pure existence theorems is the logical ε-axiom, upon which in turn the construction of ideal propositions depend. And to what extent has the formula game thus made possible been successful? This formula game enables us to express the entire thought-content of the science of mathematics in a uniform manner and develop it in such a way that, at the same time, the interconnections between the individual propositions and facts become clear. To make it a universal requirement that each individual formula then be interpretable by itself is by no means reasonable; on the contrary, a theory by its very nature is such that we do not need to fall back upon intuition or meaning in the midst of some argument. What the physicist demands precisely of a theory is that particular propositions be derived from laws of nature or hypotheses solely by inferences, hence on the basis of a pure formula game, without extraneous considerations being adduced. Only certain combinations and consequences of physical laws can be checked by experiment — just as in my proof theory only the real propositions are directly capable of verification. The value of pure existence proofs consists precisely in the individual construction is eliminated by them and that many different construction are subsumed under one fundamental idea, so that only what is essential to the proof stands out clearly; brevity and economy of thought are the rasion d’être of existence proofs.

> … The fundamental idea of my proof theory is none other than to describe the activity of our understanding, to make a protocol of the rules according to which our thinking actually proceeds.

> ... … Existence proofs carried out with the help of the principle of excluded middle usually are especially attractive because of their surprising brevity and elegance.

He also makes this remark, which turned out to be unfortunate in light of Gödel:

> From my presentation you will recognize that it is the consistency proof that determines the effective scope of my proof theory and in general constitutes its core.

Which brings us to Weyl in 1927 (in the comment below)