"Introduction to mathematical logic" book from a formalist perspective

Question

I'm looking for books that introduce the reader to mathematical logic assuming the perspective of a formalist. I've found that many books are more or less written for the platonist - like Kunen's Foundations of Mathematics, where he even implicitly says on pp. 191 that his book, if I understood it right, is primarily written for platonists, but also explains how a formalist would understand his book (in a whopping 3 pages compared to a couple of sentences for platonist view!).

I'm looking for a book that doesn't wait until page 191 to explain this to me, but constantly conveys the formalist viewpoint.
It is important that the books clearly explains the distinction between theory and metatheory and where different theorems of the metatheory live in (e.g. the soundness theorem can be perceived to be a theorem of ZFC since the relevant parts of the metatheory can be coded in ZFC).

I looked at every book from the thread Ask for recommendations for textbook on mathematical logic and none was what I was looking for. Closest to my needs came Kunen - who at least mentions formalism and how his book should be read according to this perspective. This contrasts with other logic books who don't mention anything, and Cori and Lascar's book - for their excellent introduction concerning the vicious circle in what mathematical logic studies - and Goldrei's book on logic, which is not on the list.

To give an explanation for this, perhaps, unusual request: I find it that I understand mathematical theories best when the setting in which the theory "lives" in is clearly outlined so that working in that theory is just formal manipulations of symbols - of course I can attach meaning and intuition to these manipulations, but there has to be a "fixed" setting to work in. From what I've read this aligns understanding aligns best with the perspective of formalism. But sadly mathematical logic is always somewhat vague and in basic core always seems to be somewhat obscure (Kunen says in the above mentioned book for example on page 190 that

we cannot say exactly

what metatheory is. Now I accept that we can't begin with formal setting based on nothing, because there has to be an informal description of the most basic formal elements of our setting, but I would hope that there are books that explain in more detail that in a single paragraph what metatheory really is. Additionally the lecturer at a course I'm taking also believes in some absolute mathematical objects - I assume he is a platonist - since he frequently says things like "no, now we're not talking about a formalized version of the natural numbers, we're talking about the real natural numbers", which totally annoys me because for me, there are no real natural numbers).

Answer 1

One example a bit closer to what you seek might be:

• George Tourlakis, Lectures in Logic and Set Theory, volumes 1 and 2, Cambridge studies in advanced mathematics, vol. 83. Cambridge University Press, Cambridge, UK, 2003.

You can see my review, which appeared in the Bulletin of symbolic logic, vol. 11, iss. 2, p. 241, 2005:

This is a detailed two-volume development of mathematical logic and set theory, written from a formalist point of view, aimed at a spectrum of students from the third-year undergraduate to junior graduate level. Volume 1 presents the heart of mathematical logic, including the Completeness and Incompleteness theorems along with a bit of computability theory and accompanying ideas. Tourlakis aspires to include “the absolutely essential topics in proof, model and recursion theory” (vol. 1, p. ix). In addition, for the final third of the volume, Tourlakis provides a proof of the Second Incompleteness Theorem “right from Peano’s axioms,...gory details and all,” which he conjectures “is the only complete proof in print [from just Peano arithmetic] other than the one that was given in Hilbert and Bernays (1968)” (vol. 1, p. x). In the opening page of Chapter II, Tourlakis provides a lucid explanation of the proof in plain language, before diving into the details and emerging a hundred pages later with the provability predicate, the derivability conditions and a complete proof. Tempering his formalist tendencies, Tourlakis speaks “the formal language with a heavy 'accent' and using many 'idioms' borrowed from 'real' (meta)mathematics and English,” in a mathematical argot (vol. 1, p. 39). In his theorems and proofs, therefore, he stays close to the formal language without remaining inside it.

more, including criticism...

Answer 2

I'd like to elaborate a bit on the suggestion, mentioned by some others, that your complaint is not really about platonism versus formalism, but about the common practice of being not completely clear about the metatheory. Given that the distinction between theory and metatheory is so important, why don't the books make it completely clear at all times which metatheory is in force?

To some extent this can be blamed on poor exposition, but I'd like to suggest that there are good reasons behind this practice, which are important to understand. As an example, consider the irrationality of √2. The proof of this theorem is almost always presented in textbooks without any explicit statement about what formal system the proof is supposed to be taking place in. So how is the reader supposed to tell whether the proof is correct? Wouldn't it be better to state at the beginning that the proof is supposed to be carried out on the basis of 1st order Peano arithmetic, or whatever?

Well, this could be done, but there are a couple of reasons why this is not typically done. The most important is that almost everyone finds it easier to understand the proof that √2 is irrational if it is presented in the usual manner. Even if they want to verify a statement such as "`√2 is irrational' is a theorem of PA", they find it easier to do this by first getting an intuitive understanding of the proof, and then making a "second pass" through the proof to verify that each step in the argument can be mimicked by a formal deduction in PA, rather than taking a purely formal string such as ∀a∀b¬(Sa⋅Sa=SS0⋅Sb⋅Sb) and mechanically checking each step of a formal proof of it. A second reason is that it is often the case that we want to verify that "√2 is irrational" is a theorem not only of PA, but of various other formal systems. Again, while one possible approach is to go through the entire formal verification process every time one wants to switch to another formal system, it is far more practical if the reader can understand the "content" of the argument and verify for himself or herself that all the necessary steps can be carried out on the basis of whatever formal system is currently of interest. The flexibility is useful.

My guess is that despite your stated views, you count yourself among the vast majority of people who are able to read and verify the correctness of the proof that √2 is irrational without having to have it completely formalized first. After all, almost everyone who studies mathematics encounters this argument before learning the details about formal systems. My guess is that the trouble begins when the theorems in question get a lot more complicated. For example, consider the proof of Goedel's 1st incompleteness theorem. This is a lot more complicated than the proof that √2 is irrational, and there might be parts that you have difficulty with. This is the point where you might worry about the validity of what's being asserted, and might wish that the metatheory were clearly defined so that you could fall back on formally verifying that A follows from B on the basis of the metatheory. I'd like to suggest, though, that almost always, it's not the lack of clarity about the metatheory that's the real problem; it's that the reasoning is just not being explained clearly enough for you. With rare exceptions, if the reasoning is correct, it's going to be correct in any "reasonable" choice of metatheory.

At this point you might say, "I understand everything you're saying, but still, the textbooks and professors sometimes talk about sets and integers as if they're real things, and I just don't believe that they're real! So I can't follow what they're arguing, and I have a sneaking suspicion that they're using philosophically unjustified assumptions about the reality of integers or sets in their supposedly mathematically rigorous proofs." Don't worry, this isn't what is happening. Any time that someone refers to the "actual" integers or the "standard model" or something like that, you can always make sense of it by taking your metatheory to be some set theory such as ZFC, inside which there is a unique set of natural numbers. People don't always say ZFC explicitly, for the same reason as before: It doesn't have to be ZFC; various other set theories would work just fine, and it's useful to be flexible.

In the end, I think that rather than look for a book that presents things from a formalist point of view, you are better off developing the skill of reading a proof and recognizing what assumptions are needed to carry it through. Eventually you need to develop this skill anyway. For example, for the proof of Goedel's 2nd incompleteness theorem, you need to be able to go through the proof of the 1st incompleteness theorem and verify that it can be formalized in (for example) PA. If you have this skill then you don't need to be explicitly told which metatheory is in force. And probably the best way to develop the skill is to do some formalization exercises. Looking for such exercises (perhaps in the context of modern proof assistants such as Coq or Mizar) might be more fruitful than looking for a formalist textbook.

Answer 3

(This was supposed to be a comment, but I do not have enough reputation right now, so will extend my answer and try to both answer your question and make side comments).

I personally think the question is somewhat ambiguous since I cannot really see how the difference between Platonist approach and formalist approach could be visible in a textbook (except, details of formalizations and keeping proofs and arguments closer to how they would "formally" look).

I do not think it would really matter which philosophical view you are siding with, because when it comes to doing mathematics, you have to act like a "formalist" anyway, meaning that you will formalize your argument in some fixed formal system and work there disregarding any notion that cannot be formalized inside.

One of the best formal systems you can formalize (pretty much) everything is ZFC. This means that the "setting" you are looking for when you said

I find it that I understand mathematical theories best when the setting in which the theory "lives" in is clearly outlined so that working in that theory is just formal manipulations of symbols - of course I can attache meaning and intuition to these manipulations...

can easily be taken to be ZFC.

My impression from how you asked your question is that you are looking for a textbook that keeps the distinction between formalized concepts and the intuitive ones we have in mind. For example, we have an intuition for what "truth" means in a structure and we can formalize the corresponding satisfaction relation (say, in ZFC). When you or any logic book prove a theorem involving it (let's take the soundness theorem example you gave), then what you really prove is (formal) provability implies (formal) satisfaction.

The only difference between a Platonist and a formalist stating the same theorem is that the former would see no reason to keep the part in parentheses (for they believe the natural numbers and our formalization of it are the one). You apparently would, as you seem to be not believing in the existence of the natural numbers.

Going back to main question, any textbook that was suggested on MO should be precise enough for you to formalize all model theoretic notions so that you can "keep a formalist point of view" (whatever that means for you).

Specifically, for set theory, I can say that Kunen's book (Set Theory: An Introduction to Independence Proofs) and Jech's book (Set Theory) both make clarifications about formalizations and metatheory time to time, which is sufficient to eliminate confusions.

Answer 4

I don't know of logic textbooks which adopt an explicitly formalist viewpoint (which is not to say I think none exist), but for what it's worth, I'd say that books on categorical logic tend not to adopt a Platonist point of view. Abstract methods of categorical algebra naturally tend to promote the idea of there being different universes (e.g., toposes) in which to do mathmatics, and a seasoned category theorist is quite comfortable mentally inhabiting worlds where one is a straight-up model of ZFC, and another is a world where every function from the reals to itself is continuous, etc. The book my Mac Lane and Moerdijk on topos theory, and the book by Lambek and Scott on higher-order categorical logic, come to mind as examples of books which encourage this way of thinking. (The Lambek-Scott text has a bit of philosophy where they suggest possible bridges between platonism, formalism, and intuitionism.)

Probably books on categorical logic are not what you're looking for, but in that case you might try seeking online lecture notes on more traditional topics written by categorical logicians, who seem to have a habit of looking at metatheoretic contexts. One example I bumped into recently are Jaap van Oosten's notes on Peano arithmetic and Gödel incompleteness phenomena. Again, it's not that an avowedly formalist position is declared; it's more the style of writing that eschews appeals to Platonic intuitions about the "real" natural numbers (which I don't care for either). If you make your question more specific about exactly which topics you want to see, maybe a more specific answer can be made.