Date: Thu, 18 Mar 1999 16:00:03 -0700 From: Randall Holmes Subject: FOM: second-order logic is a myth -- also, informal versus formal reasoning In this note, I discuss Simpson's claim that "mathematics can be formalized in ZFC" This is a very common claim; I often make it myself (more often I claim that mathematics can be formalized in strong extensions of NFU, a claim to which the same strictures apply that I apply below to the commoner claim about ZFC). It is true in a certain practical sense. But I think that there are also good grounds (which most of us know about, though I will tiresomely summarize them below) for the contrary claim that "arithmetic (and so most of mathematics) cannot be formalized at all". This is relevant to the thread about second-order logic because I think that the use of "naive" and "informal" by Simpson in contexts where Black (apparently) and I (certainly) would say that second-order logic is being used are indicative of the contrasting viewpoints at work. The informal view of arithmetic is "second-order" from my standpoint and involves an appeal to "naive theory of sets" from Simpson's. In any event, from either standpoint, one can arrive at the conclusion that the axioms and rules of inference of first-order PA are correct for reasoning about the natural numbers. We now encode terms and proofs of first-order PA by natural numbers, so that we can (apparently) talk about formal proofs in PA inside PA itself. We can refer to open sentences with one natural number parameter as "formal predicates of a natural number" and enumerate these. We can define a formal predicate which ostensibly expresses: "the nth formal predicate of natural numbers cannot be proved to hold of n" This is the mth formal predicate for some natural number. We can then express the G\"odel sentence as (roughly): "the mth formal predicate of natural numbers holds of m" >From an informal standpoint, we can see that this is true; it says (informally) that it itself cannot be proved. If it could be proved, then (informally) we would be able to prove a false sentence in PA, which we know from our informal standpoint is not the case. However, since it can't be proved, there are models of PA in which it is false. In these models, there are "natural numbers" which encode "proofs" of the G\"odel sentence. These must be nonstandard natural numbers, since there aren't actually any such "proofs". It is usually said that the G\"odel sentence is self-referential. I claim that this is not what is really happening. The reason that logical disaster (paradox) is averted here is precisely that self-reference cannot be achieved: the axioms of PA do not succeed in specifying the natural numbers exactly, and so do not succeed in specifying the notion of "formal proof in PA" precisely either; the only reason that we see self-reference is that we informally accept the notions formalized in PA at "face value" as equivalent to the corresponding informal notions. In true second-order arithmetic, it is possible to define such notions as "formal proof in first order PA" exactly; in fact, "formal proof in T", where T is any formal system, can be defined precisely in second-order arithmetic. The argument given above can be adapted in the true second-order context to prove that there can be no such notion as "formal proof in second-order arithmetic". This applies to the formal system usually called "second-order arithmetic" as well; certain principles which I accept because I accept true second-order arithmetic are formalized in this first-order two-sorted theory. But at the informal level I accept even stronger statements as true which are not provable in this formal system: for example, I informally accept the truth of the G\"odel sentence of the formalized "second-order arithmetic" or even stronger systems (such as ZFC). My claim here is that the informal standpoint cannot be eliminated. I can extract formal principles of reasoning which I regard as correct from my informal standpoint and work inside such a formal system, but such a formal system never exhausts the mathematical principles that I accept as correct. For any such system T, since I accept T as valid, I accept Con(T) as valid as well (for example; this sort of thing is presumably not restricted to the G\"odel phenomenon!). It may be that my informal standpoint can be completely formalized, but if so it cannot be formalized by me; I will not accept this hypothetical formalization even if it is presented to me (I presumably won't understand it). I do accept PA (and ZFC) so these theories cannot be formalizations of mathematics as I understand it. Since Simpson accepts these systems, they can't formalize mathematics as he understands it, either :-) I think that this issue of the relationship between our informal understanding of mathematics and our formalizations is a crucially important one for the topic of this list. It also may help to clarify the sense in which I (and perhaps others) regard second order logic as indispensible and distinct from the "second-order theories" which can be formalized. Note: I don't regard second-order principles (which are necessarily informal, though partially formalizable) as exhausting informal principles of reasoning, or even as exhausting the informal principles needed for the discussion above. disclaimer: I don't profess that anything in this posting is original with me (except of course any errors or infelicities). And God posted an angel with a flaming sword at | Sincerely, M. Randall Holmes the gates of Cantor's paradise, that the | Boise State U. (disavows all) slow-witted and the deliberately obtuse might | holmes@math.idbsu.edu not glimpse the wonders therein. | http://math.idbsu.edu/~holmes ------------------------------ Date: Thu, 18 Mar 1999 16:25:52 -0700 From: Randall Holmes Subject: FOM: informal versus formal reasoning I must hasten to add that I regard formal proof as completely indispensible in mathematics; I would hate to be accused of being a postmodernist. First-order logic does capture a (nearly) universal standard of formalized proof. I also regard exact formal definition of what we are talking about as being completely indispensible in mathematics; thus the need for the expressive power of second-order logic. Formal proofs (using generally accepted principles such as those of first-order logic) allow us to see that the conclusions we draw follow from our axioms. They also allow us to identify the axioms we are using, which themselves may require "informal" justification. If you do not share my conviction that a certain axiom is true, this allows you to express your objections to my proof precisely; you can separate objections on a formal level from objections on an informal or "intuitive" level. (If you are a constructivist, you can examine the formal principles of reasoning I accept and express your possibly stronger objections to my proof precisely as well). As long as we confine ourselves to what can be proved within a strong formal system such as ZFC which most of us are willing to accept as safe, the need for informal justifications of axioms can be kept to a minimum (even to zero) allowing some of us to be convinced (mostly harmlessly) that the formal system in question "formalizes mathematics". And God posted an angel with a flaming sword at | Sincerely, M. Randall Holmes the gates of Cantor's paradise, that the | Boise State U. (disavows all) slow-witted and the deliberately obtuse might | holmes@math.idbsu.edu not glimpse the wonders therein. | http://math.idbsu.edu/~holmes