# “Introduction to mathematical logic” book from a formalist perspective

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).

-
I would suggest to take a look at both Kleene's Introduction to Metamathematics, and Hilbert and Ackermann's Principles of mathematical logic. –  Andres Caicedo Jan 25 at 17:42
The "real" natural numbers are exactly the numbers of the metatheory... Separately, if you do look at Kleene's book mentioned by Andres Caicedo, you will see a reason why few textbooks are written in that extremely formal style. –  Carl Mummert Jan 25 at 17:48
I know this isn't what you're asking, but it seems related: in my forthcoming book Forcing for Mathematicians I try to draw a clear distinction between the target theory (ZFC) and the metatheory in which consistency and independence results are proven (which I take to be PA). I share your discomfort with expositions which fail to make this crystal clear at the outset. –  Nik Weaver Jan 25 at 19:11
@NikWeaver You cannot imagine how good it feels to me that I'm not the only one who takes issue with this problem - and that it's not just a student but an established mathematician who shares the same discomfort is especially comforting! (Because where I'm located nobody else has the qualms I have and I started to develop a feeling that all people who are working in the field are at leisure with this.) I'm looking very much forward to your book. To you have an approximate plan, when it's going to be published ? –  user43263 Jan 25 at 19:58
What you need is simply logical maturity. Perhaps this is best attained through a text which goes through many details, like Enderton's intro logic book. In the end, it is not necessary, and in my opinion actually very inefficient, for an author to constantly hew towards a formalist view. Casual platonism (which you can eventually read as noncommittal) is far more effective at communicating genuine mathematical ideas. Once you have attained logical maturity, you can read mathematics and interpret it according to whatever philosophical leanings you are drawn towards. –  Monroe Eskew Jan 26 at 5:30

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...

-

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.

-
I want to thank you very much - it felt as if you could read my mind with a part of what was bothering a set me straight! –  user43263 Jan 26 at 11:38
I'm puzzled about why this answer is getting votes. The difference is that in logic the subject matter is the formal systems themselves, so you can't just reason naively and say, for instance, "we know PA is consistent" and leave it at that. The consistency of PA is not provable in PA and this matters. The point is that the choice of metatheory is more relevant in logic than elsewhere, so I wouldn't be so quick to dismiss the OP's concerns. –  Nik Weaver Jan 26 at 16:28
@Nik: Everything you say is accurate. However, in my experience, students who say (in effect) that they are formalists and not platonists tend to be bothered by something more basic. They freeze up when they see talk of "truth" or "the standard natural numbers" and can't follow the reasoning. This really has nothing to do with formalism or even with technical concerns about the precise metatheoretical strength needed for specific arguments, although their complaints can sound like that. –  Timothy Chow Jan 26 at 21:56
(continued) Once students get over that hurdle, then there is, as you say, another hurdle later, when one needs to verify that specific arguments can be formalized in specific systems. Sometimes this is glossed over, and it is fair to ask for more details than are usually given. But again in my experience, people who have a clear understanding of the general setup and just want more technical details tend to phrase their request rather precisely, and in particular recognize that formalism vs platonism isn't the real issue. –  Timothy Chow Jan 26 at 22:02

(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.

-
I'm not sure if being a formalist necessarily means that the "details of formalizations and keeping proofs and arguments" have to look "closer to how they would 'formally'". If it's clear how to translate an informal argument into a formal one I don't see any objections to being informal. It seems to me that the difference lies rather in the fact that as a formalist one is more careful stating the setting in which one is working in the first place and avoiding "intuitively clear" arguments, whereas a platonist wouldn't be so much bothered by not being told, e.g., in which metatheory we [...] –  user43263 Jan 26 at 11:47
[...] work in, since he has some concept of "absolute truths" and can take that to be his metatheory - that would be a vague explanation of how I see the dichotomy (Timothy Chows answer explains this better). –  user43263 Jan 26 at 11:53
I don't think that comfort with "intuitively clear" arguments has much to do with platonism vs formalism. It has more to do with whether the author expects the reader to have enough experience to formalize the argument, or whether the author feels the need to spell out more details. It's true that some authors get lazy and fail to spell out formalization details even in situations where it's important to check that a particular argument can be formalized in a particular formal system. But this has more to do with expository skill than with philosophical prejudice. –  Timothy Chow Jan 26 at 22:17
Dear user43263, The following answer and question (mathoverflow.net/a/23096/33039) might seem irrelevant to your question at first sight, but I believe it is not. At its core, your question and concerns are really about the question in which formal system can we carry out logic. If you want to have a fixed metatheory and see formal details, just go and try to do it! For example, try to formalize "satisfaction" and "proves" relations in your favorite set theory. Once you see that these can be done, you will be no more disturbed by logicians' laziness to sweep these under the rug. –  Burak Jan 27 at 16:41
@Burak Thanks for the link, that was a good tip (as was your advice)! –  user43263 Jan 29 at 19:50

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.

-
@CarlMummert I think you misunderstood what I wrote there, or maybe I didn't say it as well as I could have, but I don't plan on getting into details here. Suffice it to say I had in mind different syntactic machinery. –  Todd Trimble Jan 25 at 19:26
Yes, it is clear there that you had a different syntax via Q sequences in mind. But I find that, in general, there is not a focus on syntax in categorical settings in the same way there is a focus on syntax in some (particularly older) presentations of first-order logic, and that is the spirit in which I hoped to quote you. Apologies for any misinterpretation. –  Carl Mummert Jan 25 at 19:39
@CarlMummert No problem! Actually I'm sorry you deleted your comment, because I think your suggestion about "plenitudinous Platonism" merits consideration, and wonder how this connects with the "multiverse conception" being developed by Hamkins et al. (I'm not too worried about where we might disagree regarding practice of category theorists.) –  Todd Trimble Jan 25 at 20:47
Thanks. The main point of the other comment was this: although categorical approaches such as ETCS seem to argue implicitly against various kinds of "unique platonism", I think it could be argued that they support forms of "plenitudinous platonism" (see plato.stanford.edu/entries/philosophy-mathematics/#PlePla for some discussion of that). Similarly, categorical approaches might be viewed as structuralist, and there is a close relationship between plenitudinous platonism and forms of structuralism. –  Carl Mummert Jan 25 at 21:00
Another relevant question is the difference between asking whether there is a single natural number structure $(\mathbb{N}, s)$ that is the "real" natural numbers with successor, versus whether there is a unique isomorphism class of such structures that determines the "real" isomorphism class of natural number structures. In many cases, the issue with the metatheory/object-theory distinction is not that they may disagree about what individual numbers "are", it's that they may disagree about the isomorphism type of the naturals (because the object theory may admit nonstandard numbers). –  Carl Mummert Jan 25 at 21:06