Skip to main content
Source Link
Timothy Chow
  • 82.7k
  • 26
  • 363
  • 587

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.

Post Made Community Wiki by Timothy Chow