Reddit mentions of From Frege to Godel: A Source Book in Mathematical Logic, 1879-1931 (Source Books in History of Sciences)

For the development of modern mathematic logic, a great volume with primary sources is From Frege to Godel.

http://www.amazon.com/From-Frege-Godel-Mathematical-1879-1931/dp/0674324498

Kneale & Kneale is definitely the go-to source for a broader history.

> and i got the impression that may be i should also learn about the history, the context, the development and the goals of mathematical logic in order to appreciate it fully

I don't know that this is really necessary to be honest. It's certainly interesting, but isn't necessary to having a firm grasp on logic as done in mathematics departments.

That being said, here are some suggestions. You should start by consulting Peter Smith's Teach Yourself Logic, which is a huge document listing any and every source you'll ever need to learn logic.

As for history - that's a bit trickier. Frege's a tough place to start. He's a clear writer and the origin of analytic philosophy, but his Begriffsschrift notation is a pain in the ass to read (it doesn't resemble anything you will be familiar with). Also his logic is second-order, which isn't exactly standard (although it's more accepted nowadays).

If you want to start with Frege, I recommend reading his Begriffsschrift (Concept Script, a formal language of pure thought modelled upon that of arithmetic) and his Grundlagen (The Foundations of Arithmetic). The latter is much more important in my opinion. If you decide you want to get to the real nitty-gritty, you can consult the brand new, first ever full translation of the Grundgesetze, which includes a huge appendix which teaches you the notation.

For a broader perspective Kneale & Kneale's The Development of Logic is a great (secondary) source. If you want primary sources, van Heijenoort's From Frege to Gödel is the place to go.

> apparently mathematical logic is supposed to be a rigorous analysis of logic?

I wouldn't really characterise it this way. In my experience, most people split the study of logic into three main camps: mathematical logic, philosophy of logic and philosophical logic. The first camp is the proving of theorems in various logical systems, usually with an eye towards mathematical application. The last camp is the application of logic and logical tools to philosophical problems. And the philosophy of logic is the study of the nature of logic itself. That's a bit closer to the types of things you touch on at the end there.

Many, many people just study one of the branches I list, and you can too, without worrying about the philosophy.

This book refocused my life. It gave me the recognition of the value of my CS degree I did not have while I was doing my degree.

After I read GEB I read this:

https://www.amazon.com/gp/aw/d/0674324498/ref=mp_s_a_1_1?ie=UTF8&qid=1524603692&sr=8-1&pi=AC_SX236_SY340_QL65&keywords=frege+to+godel

I didn’t understand most of it and I didn’t follow most of the proofs, but reading the words of these men was quite a wild ride because I knew where the story would end, and reading the arguments between these brilliant people and seeing how each was so convinced of their view, and how wrong they were, and how some had grace and others lacked it... really fascinating thing to bear whiteness to.

If you are interested in studying the development of mathematical logic and the philosophical disputes surrounding the foundational questions (viz., the disputes between logicism, formalism, intuitionism, etc.) then Russell should not be studied in isolation from Frege, Hilbert, Brower, et al. Perhaps: http://www.amazon.com/From-Frege-Godel-Mathematical-1879-1931/dp/0674324498

This might be too technical, I don't know!

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)