My two main current research projects are as follows

**1. Induction, Abduction and Inference to the Best Explanation.**

I am interested in understanding the character of inductive inference, abductive inference, and inference to the best explanation. Although Bayesian approaches to these topics enjoy much popularity these days, I do not think such approaches offer the kind of insight into these forms of inference that one might hope. I instead prefer a more qualitative approach to understanding these forms of non-deductive inference. While skeptical about inference to the best explanation as it is usually formulated, I am nevertheless attracted to the idea that explanatory considerations play a central role in non-deductive inference. I am also inclined to think that many puzzles about induction stem from an unclear conception of how inductive inference works, and strive to produce a clearer account of inductive inference, in order to address the question of to what extent we need an account of its underpinnings.

**2. Type Theory and Logic.**

I am interested in understanding the way in which modern type theory, as developed over the past several decades in computer science, offers a new perspective on the nature of logic. A central question here is what the Curry-Howard Correspondence tells us about logic, and in what sense proofs can be viewed as programs. I am also interested in the idea that type theories (such as Martin-Löf Type Theory or Homotopy Type Theory) can be used as foundations for mathematical reasoning, and am interested in understanding what this tells us about the character of mathematics. A question of particular interest is whether in some sense intuitionistic logic has a privileged role to play in the foundations of mathematics.

I am in the process of writing a book on all this accessible to philosophers, mathematicians, and others who might not have much of a background in computer science. The book aims for a technically rigorous and decently complete introduction to this material without detouring through significant amounts of computer science. Right now, I am hoping that the book will consist of roughly ten chapters, beginning with an introduction to the lambda calculus, and ending with homotopy type theory. Here is a draft of the first two chapters. I hope to update it as more chapters become available or significant corrections are made. I am particularly welcoming of critical feedback and corrections. If you notice any problems or have any thoughts at all about the manuscript, please send me an email at kjdavey at uchicago.edu. (I plan on being generous when I finally write the acknowledgements section!)

Type Theory for Logic and Mathematics – Chapters 1, 2 (July 9, 2023)

**3. Other Interests
**

In addition to the above, I have further interests that I expect to continue to write about in the not too distant future. One topic of interest is the historical genesis of mathematical proof, in both the Western and Eastern traditions. Another is on formal theories of truth, and ways of avoiding the liar paradox. In this direction, I am currently exploring irreflexive logics as a way of reconciling reasonable principles of truth with systems of logic as close to classical logic as possible.