Friday, 21 March 2014

Logical foundations for mathematics? The first-order vs. second-order ‘dichotomy’? (Part IV of 'Axiomatizations of arithmetic...')

(It took me much longer than I had anticipated to get back to this paper, but here is the final part of my paper on axiomatizations of arithmetic and the first-order/second-order divide. Part I is here; Part II is here; Part III is here. As always, comments are welcome!)

3. Logical foundations for mathematics? The first-order vs. second-order ‘dichotomy’?

Given the (apparent) impossibility of tackling the descriptive and deductive projects at once with one and the same underlying logical system – what Tennant (2000) describes as ‘the impossibility of monomathematics’ – what should we conclude about the general project of using logic to investigate the foundations of mathematics? And what should we conclude about the first-order vs. second-order divide? I will discuss each of these two questions in turn.

If the picture sketched in the previous sections is one of partial failure, it can equally well be seen as a picture of partial success. Indeed, a number of first-order mathematical theories can be made to be categorical with suitable second-order extensions (Read 1997). And thus, as argued by Read, there is a sense in which the completeness project of the early days of formal axiomatics has been achieved (despite Gödel’s results), namely in the descriptive sense countenanced by Dedekind and others.  

Moreover, categoricity failure must not be viewed as a complete disaster, if one bears in mind Shapiro’s (1997) useful distinction between algebraic and nonalgebraic theories:
Roughly, non-algebraic theories are theories which appear at first sight to be about a unique model: the intended model of the theory. We have seen examples of such theories: arithmetic, mathematical analysis… Algebraic theories, in contrast, do not carry a prima facie claim to be about a unique model. Examples are group theory, topology, graph theory… (Horsten 2012, section 4.2)
In this vein, proofs of (non-)categoricity can be viewed as a means of classifying algebraic and non-algebraic theories (Meadows 2013). This means that the descriptive (non-algebraic) project of picking out a previously chosen mathematical structure and describing it in logical terms has developed into the more general descriptive project of studying theories and groups of theories not only insofar as they instantiate unique structures (i.e. non-algebraic as well as algebraic versions of the descriptive project).

On the deductive side, things may seem less rosy at first sight. In a sense, first-order logic is not only descriptively inadequate: it is also deductively inadequate, given the impossibility of a deductively complete first-order theory of the natural numbers, and the fact that first-order logic itself is undecidable (though complete). It does have a better behaved underlying notion of logical consequence when compared to second-order logic, but it still falls short of delivering the deductive power that e.g. Frege or Hilbert would have hoped for. In short, first-order logic might be described as being ‘neither here nor there’.

However, if one looks beyond the confines of first-order or second-order logic, developments in automated theorem proving suggest that the deductive use as described by Hintikka is still alive and kicking. Sure enough, there is always the question of whether a given mathematical theorem, formulated in ‘ordinary’ mathematical language, is properly ‘translated’ into the language used by the theorem-proving program. But automated theorem proving is in many senses a compelling instantiation of Frege’s idea of putting chains of reasoning to test.

Recently, the new research program of homotopy type-theory promises to bring in a whole new perspective to the foundations of mathematics. In particular, its base logic, Martin-Löf’s constructive type-theory, is known to enjoy very favorable computational properties, and the focus on homotopy theory brings in a clear descriptive component. It is too early to tell whether homotopy type-theory will indeed change the terms of the game (as its proponents claim), but it does seem to offer new prospects for the possibility of unifying the descriptive perspective and the deductive perspective.

In sum, what we observe currently is not a complete demise of the original descriptive and deductive projects of pioneers such Frege and Dedekind, but rather a transformation of these projects into more encompassing, more general projects.

As for the first-order vs. second-order divide, it may be instructive to look in more detail into the idea of second-order extensions of first-order theories, specifically with respect to arithmetic. Some of these proposals can be described as ‘optimization projects’ that seek to incorporate the least amount of second-order vocabulary so as to ensure categoricity, while producing a deductively well-behaved theory. In other words, the goal of an optimal tradeoff between expressiveness and tractability may not be entirely unreasonable after all.

One such example is the framework of ‘ancestral logic’ (Avron 2003, Cohen 2010). Smith (2008) argues on plausible conceptual grounds that our basic intuitive grasp of arithmetic surely does not require the whole second-order conceptual apparatus, but only the concept of the ancestral of a relation, or the idea of transitive closure under iterable operations (my parents had parents, who in turn had parents, who themselves had parents, and so on). Another way to arrive at a similar conclusion is to appreciate that what is needed to establish categoricity by extending a first-order theory is nothing more than the expressive power required to formulate the induction schema, or equivalently the last, second-order axiom in the Dedekind/Peano axiomatization (the one needed to exclude ‘alien intruders’). Here again, the concept of the ancestral of a relation is a plausible candidate (Smith 2008, section 3; Cohen 2010, section 5.3).

Extensions of first-order logic with the concept of the ancestral yield a number of interesting systems (Smith 2008, section 4; Cohen 2010, chapter 5). These systems, while not being fully axiomatizable (Smith 2008, section 4), enjoy a number of favorable proof-theoretical properties (Cohen 2010, chapter 5). Indeed, they are vastly ‘better behaved’ from a deductive point of view than full-blown second-order logic – and of course, they are categorical.

Significant for our purposes is the status of the notion of the ancestral, straddled between first-order and second-order logic. Smith argues that the fact that this notion can be defined in second-order terms does not necessarily mean that it is an essentially higher-order notion:

In sum, the claim is that the child who moves from a grasp of a relation to a grasp of the ancestral of that relation need not thereby manifest an understanding of second-order quantification interpreted as quantification over arbitrary sets. It seems, rather, that she has attained a distinct conceptual level here, something whose grasp requires going beyond a grasp of the fundamental logical constructions regimented in first-order logic, but which doesn’t takes as far as an understanding of full second-order quantification. (Smith 2008)

What this suggests is that the first-order vs. second-order divide itself may be too coarse to describe adequately the conceptual building blocks of arithmetic. It is clear that purely first-order vocabulary will not yield categoricity, but it would be misguided to view the move to full-blown second-order logic as the next ‘natural’ step. In effect, as argued by Smith, the concept of the ancestral of a relation is essentially neither first-order nor second-order, properly speaking. So maybe the problem lies precisely in the coarse first-order vs. second-order dichotomy when it comes to the key concepts at the foundations of arithmetic (such as the concept of the ancestral, or Dedekind’s notion of chains). We may need different, intermediate categories to classify and analyze these concepts more accurately.


4. Conclusions

My starting point was the observation that first-order Peano Arithmetic is non-categorical but deductively well-behaved, while second-order Peano Arithmetic is categorical but deductively ill-behaved. I then turned to Hintikka’s distinction between descriptive and deductive approaches for the foundations of mathematics. Both approaches were represented in the early days of formal axiomatics at the end of the 19th century, but the descriptive approach was undoubtedly the predominant one; Frege was then the sole representative of the deductive approach.

Given the (apparent?) impossibility of combining both approaches in virtue of the orthogonal desiderata of expressiveness and tractability, one might conclude (as Tennant (2000) seems to argue) that the project of providing logical foundations for mathematics itself is misguided from the start. But I have argued that a story of partial failure is also a story of partial success, and that both projects (descriptive and deductive) remain fruitful and vibrant. I have also argued that an investigation of the conceptual foundations of arithmetic seems to suggest that the first-order vs. second-order dichotomy is in fact too coarse, as some key concepts (such as the concept of the ancestral of a relation) seem to inhabit a ‘limbo’ between the two realms.

One of the main conclusions I wish to draw from these observations is that there is no such thing as a unique project for the foundations of mathematics. Here we focused on two distinct projects, descriptive and deductive, but there may well be others. While it may seem that these two perspectives are incompatible, there is both the possibility of ‘optimization projects’, i.e. the search for the best trade-off between expressive and deductive power (e.g. ancestral arithmetic), and the possibility that an entirely new approach (maybe homotopy type-theory?) may even dissolve the apparent impossibility of fully engaging in both projects at once. It is perhaps due to an excessive focus on the first-order vs. second-order divide that we came to think that the two projects are incompatible.

At any rate, the choice of formalism/logical framework will depend on the exact goals of the formalization/axiomatization. Here, the focus has been on the expressiveness-tractability axis, but there may well be other relevant parameters. Now, if we acknowledge that there may be more than one legitimate theoretical goal when approaching mathematics with logical tools (and here we discussed two, prima facie equally legitimate approaches: descriptive and deductive), then there is no reason why there should be a unique, most appropriate logical framework for the foundations of mathematics. The picture that emerges is of a multifaceted, pluralistic enterprise, not of a uniquely defined project, and thus one allowing for multiple, equally legitimate perspectives and underlying theoretical frameworks. A plurality of goals suggests a form of logical pluralism, and thus, perhaps there is no real ‘dispute’ between first-order and second-order logic in this domain.


6 comments:

  1. I really enjoyed this paper, I had not looked at these issues in this way before. My one small criticism is that you could maybe spend a bit more time on ancestral arithmetic and HoTT in relation to the deductive/descriptive `divide,' especially as paper will appeal/ be accessible to people without a lot of background in the formal foundations of mathematics.

    ReplyDelete
    Replies
    1. Thanks for your comment! I agree that as it stands, the paper basically presupposes that the reader knows more or less what ancestral arithmetic and HoTT are all about. My hesitation is that if I start elaborating further on them, then I'll have to tell a much longer story, and the balance of the paper might be disrupted. For ancestral arithmetic in any case, Smith's paper has everything I might want to say :)

      Delete
  2. I really enjoyed all four parts of this article! It is nice to see such a balanced account of the deductive/descriptive divide with a positive outlook.

    I have also been following the development of HoTT, mostly from the sidelines, but with great interest in what this fresh point of view might bring to foundations of mathematics. It is interesting to see that the deductive/descriptive clash is happening within HoTT itself. On the one hand, some seem to support the view that homotopy type theory is the language of higher topos theory. On the other hand, some seem to support the view that homotopy type theory is a better way to understand mathematical reality. A few months ago, I asked on MathOverflow whether HoTT had an intended model and Andrej Bauer explained that points of view are mixed in the HoTT community: http://mathoverflow.net/a/136369 (See also this recent exchange between Voevodsky and Shulman on the HoTT newsgroup to see how the two perspectives interact.)

    Interestingly, there appears to be a third point of view which is relatively unaffected by the divide. Some who arrived at HoTT from the type-theoretic side seem to focus on the computational interpretation of homotopy type theory. Rather than being interested in describing mathematical objects, proponents of this perspective are more interested in describing mathematical activity. I find this point of view very refreshing and I am very curious to see what kind of impact this perspective will have on the development of HoTT.




    ReplyDelete
    Replies
    1. Thanks for the comments, Francois (somehow I'm not able to 'reply' to your comment directly). It's very interesting to hear that within the HoTT community itself there is some disagreement as to what the whole project is about, so to speak. I'd say that the third point of view which you describe is basically a 'deductive' point of view, in the sense that it aims at describing mathematical activity, as you put it. At any rate, while it is still too early to say, I do think that HoTT may fundamentally change how we think about the deductive/descriptive divide, even if there are differences in emphasis among the HoTT community itself.

      Delete
  3. Hi Catarina,
    Thanks for the interesting account of the description/deductive divide. I think it may be possible to avoid the difficulties of the divide by relaxing the requirement on the descriptive side from categoricity to completeness. I develop this idea in my paper: Completeness and Categoricity (in power):
    Formalization without Foundationalism
    which has appeared in BSL and is online at
    http://homepages.math.uic.edu/~jbaldwin/pub/catcomnovbib2013.pdf



    John Baldwin

    ReplyDelete
  4. I read your article and its great help us and great information about logical foundation of math and the treatment technique is not as a matter of course that is done on a coordinated session. Bunch treatment has additionally been known not extremely powerful thanks for sharing internal medicine personal statement .

    ReplyDelete