What are the major research programmes in contemporary logic?

Question

As an interested outsider who is prone to reading about different formulations of logic, I've become interested in better understanding the big picture of what people are trying to accomplish as they are researching logic, or merely talking about logic as a proper subject of philosophy.

For instance: in the course of the extended commentary in my earlier question on the motivations of Dialetheism, it occurred to me that I might be misinterpreting some of the answers. While I think I correctly understand what people are saying about models of logic in themselves, I may be badly misinterpreting the relationship which they are drawing between logical statements, and states of affairs — there are claims that this logic, or that logic, are useful for certain situations; and as someone raised in a very solidly formal classical tradition, I would end up responding something along the lines of "things don't really work that way", or "I can see why you might call this a logic but I would describe it some other way". But perhaps these reactions miss the point?

Fact — There exist several logics. When philosophers investigate them, what is their intent? Obviously this will depend on the philosopher. But I can envision two different sorts of research programme concerning logic, whose names I will invent ad hoc without reference to anything in particular:

• Empirical logic: explore logic with the intent of determining what manner of logic best describes the world at large. Without making too many assumptions about the world, but responding to it in a more-or-less empirical fashion (taking data from the world around you, but not necessarily in a strictly scientific manner: all personal experiences are grist for the mill), what sort of logic provides the best modus operandum?

• Abstract logic: explore logic without any particular concern for whether one's subject of study has direct application, and certainly without insisting that it be particularly useful in all practical circumstances. Observe when the reasoning in other philosophers' work (on the subjects of ontology, epistemology, ethics, etc.) can be described by some particular logical system, when these do not seem to be simple "classical" logic. Also: devise models of logic merely to explore what curious or desirable properties or achievements might be possible in a logical system.

The distinction that I imagine between the two is parallel to that of physics versus pure mathematics: one is concerned with devising the right model to capture the whole world (or at least provide a united framework for a sizeable and more-or-less well-defined chunk of it), while the other is more concerned with devising models for the sake of exploring what models one can devise, and exploring the properties of the models they devise. A distinction between inventing tools and finding the right tools; a modal distinction in their goals, between determining what logics you could imagine and determining what logics you should use.

Of course, the above are only two concievable (and very broad!) research programmes; they might not be exhaustive, or mutually exclusive. They also may not be particularly useful for drawing distinctions between the different objectives of people working in logic: maybe there are better (or less trivial) distinctions than what I've guessed at above.

Bearing this in mind: what are the major research programmes in modern logic? In each branch, what are the most prominent schools of thought, and who are the most prominent thinkers/authors?

Answer 1

Categorical logic is of contemporary interest . An (elementary) topos is a generalisation of set theory (without choice), and its internal logic is higher-order intuitionistic logic.

It also has a geometric character: A sheaf of sets, is a topos, and is equivalently (which reveals it geometric character more clearly) an etale (projection is locally homeomorphic) bundle.

Interestingly, Cohens forcing construction can then be given a geometric description. Also, if (the axiom of ) Choice is enforced, then it forces the logic to become classical.

Smooth toposes model synthetic differential geometry, where the fact that the law of the excluded middle fails is neccessary to define the infinitesimal line.

homotopy type theory is a new interpretation of martin-lofs intensional constructive type theory. As the natural logic of homotopy, constructive type theory is also related to the notion of a higher topos.

Whereas category theory has been mooted as an alternative foundation to matehematics ala ZFC by Lawvere, Vladimir Voevodsky has proposed a new program for a comprehensive, computational foundation for mathematics based on the homotopical interpretation of type theory.

Answer 2

A few qualifications. My domain knowledge comes mainly from continental work and engagements with mathematical logic; I would presume there is an awful lot of new research going on in analytic circles, but unfortunately none are really on my radar at this time, so we'll have to wait for someone more knowledgeable about philosophy of logic in general to comment more broadly on this. These are then really touchpoints in the contemporary philosophy of mathematics than research strands in logic per se. There is some valid criticism in the comments questioning some of the suggestions below.

To be really clear: the suggestion below are mostly aimed to acquaint you very generally with philosophers who are deeply curious and attentive to mathematics. They do not represent active threads of research in contemporary logic, but may help provide some of the properly philosophical motivation for the philosophical study of mathematics and provide concepts helpful for understanding the process of mathematical research/invention/discovery.

Alain Badiou might merit some investigation. In particular, I might recommend Number and Numbers for an introduction to his philosophy of mathematics; note that it also provides a very thorough if strongly-opinionated review (and to some degree perhaps synthesis) of the work and thought of some of the most important figures for contemporary philosophy of mathematics -- I believe Cantor, Frege and Dedekind are each covered in some depth. The introduction to this review of that book provides some good examples of other ways contemporary philosophers have used mathematical logic to advance their philosophical research:

Donald Davidson used Tarski's theory of truth for formal languages to ground his approach to natural language semantics. Modal logic is frequently used to discuss problems of necessity, time, or belief. W. V. O. Quine made the reduction of mathematics to set theory a paradigm of "ontological commitment," such that an idealized formalization of physical science identified the entities needed to ensure the theory as fundamentally "real."

Gilles Deleuze wrote a beautiful little book called The Logic of Sense, which may be of some interest -- it is perhaps surpisingly a very fun and engaging work, packed full of many wonderful 'paradoxes' of the sort you were asking about in a previous question. In another book of his Difference and Repetition Deleuze deals with the philosophical foundations of the calculus, though I fear that may be even further afield. At any rate, good luck with your reading (and thank you for this good and interesting question!)

---

A few more touchpoints might be worth mentioning here today. In particular a text that might be valuable to review would be the the recently published translation of Albert Lautman's Mathematics, Ideas and the Physical Real, as well as another work (which might be understood as a spiritual successor) Zalamea's Synthetic Philosophy of Contemporary Mathematics. Both of these authors have a profound interest in pursuing the threads of mathematical research very carefully on its own terms. Zalamea's work in particular might itself be considered something of a review of certain contemporary threads of mathematical research with an emphasis on "higher" mathematics and in particular devoting a lot of time to figures like Grothendieck.

Answer 3

Your distinction between empirical and abstract logic is important. Mathematicians who worked on the conception of a method of logic in the 19th century, Frege in particular, were essentially and explicitly motivated by the idea that a proper method of formal logic would help improve the rigour of mathematical proofs, a particular concern at the time, between the two extremes of Abel and Weierstrass. This suggests a view of logic as essentially not arbitrary and therefore as essentially empirical.

And in effect, mathematicians working on a method of logic at the time had to rely on the only empirical evidence available to them, i.e. Aristotle's syllogistic theory, plus what other people since had said on the subject, including other mathematicians, as well as their own personal intuition, as to what formulas could be accepted as logical truths, this in order to work out a method of logical calculus they could use to improve rigour of proof.

Today, on the surface, we seem to have a very different perspective, whereby logic is more often understood as essentially a mathematical object, like the set of Real numbers is, so that logic is thought of as being the methods of logic themselves that mathematicians have contrived since Frege. In this perspective, logic is no longer seen as an essentially empirical science, but as the motley collection of theories, seen as arbitrary at least in principle, that mathematicians are working on as objects of study rather than as methods they could use to improve the rigour of proofs.

Meanwhile, mathematicians themselves still essentially use and effectively rely on their own, intuitive, sense of logic to prove theorems, producing what can be described in effect as semi-formal proofs.

The few examples of formal logic being used to prove theorems today all rely on some variation of Gentzen's "natural" method of proof (conceived between 1929 and 1935), which is essentially a modern generalisation of Aristotle, a method which effectively relies on the crucial use of so-called rules of inference, which are formulas all essentially taken from the set of formulas long recognised as logical truths in the Aristotelian tradition, save a few exceptions.

So, in effect, all current practice of mathematical proof, be it intuitive or making use of theorem provers, like Isabel in Germany and Coq in France, still literally relies ultimately on the empirical evidence available to mathematicians that some logical truths are evidently true. Yet, the fundamentally empirical nature of the logic practised by mathematicians themselves, today as always since Euclid, is somewhat airbrushed out of the picture in favour of a more abstract notion of it.