Type Theory and Philosophy is a workshop to be held at the University of Kent on 9-10 June 2016 which explores how type theory might play the kinds of role in philosophy taken at present by standard calculi such as first-order logic, set theory and modal logic. The event will consist of tutorials and talks and is open to anyone who would like to find out more about type theory.
VENUE: W1-SR6 (Woolf Building)
By ‘type theory’, I have in mind especially the dependent type theory of Per Martin-Löf and its developments, right up to homotopy type theory and beyond. Since homotopy type theory contains within it a typed first-order logic and a form of structural set theory (see here), it is at the very least plausible that it will offer useful new tools for philosophy. (See slides, 10 and after from a recent talk in Brussels.)
Martin-Löf drew on the writings of philosophers such as Brentano, Frege and Husserl. There is a strongly constructive flavour to his ideas. (See Martin-Löf’s works, and also Göran Sundholm ‘Proof Theory and Meaning’ (pdf).)
Aarne Ranta’s ‘Type-Theoretic Grammar’ (Clarendon 1994) already contains a wealth of possible routes to explore, in particular in his treatment of natural language phenomena, such as anaphora. Clearly something like types are written into our language: ‘when’ questions expect a time, ‘who’ a person, ‘where’ a place.
Plenty of research continues in this direction, see, e.g., the work of Zhaohui Luo, a computer scientist referring to Strawson, Geach, Dummett, Brandom and Davidson, on topics such as coercion. (See the article with Chatzikyriakidis, Natural Language Inference in Coq.)
Type theories have been embraced by computer science, and a strong association with category theory has been observed. These relations have been dubbed computational trinitarianism by Robert Harper which is “the central organizing principle of a theory of computation that integrates, unifies, and enriches the language of logic, programming, and mathematics.”
Homotopy type theory is a variety of intensional type theory, with univalence and higher inductive types. The identity of two elements of a type is now not just a yes/no question, but may be represented by a higher groupoid.
A common interpretation of homotopy type theory treats sets and propositions as two kinds of types, suggesting uniform treatment where possible. So, for example, when ‘the’ as used in a definite description has been rendered type theoretically, it makes sense to apply ‘the’ to all types, not only sets. In this way we may explain the use of generalized the in mathematics. (See Expressing ‘The Structure of’ in Homotopy Type Theory.)
Treating propositions as only some types, along with the possibility of considering more structured types, allows common type-theoretic constructions to find unexpected manifestations. For example, working in the context of (the delooping of) a group, we can carry out constructions in representation theory, and treat the invariance of the Erlangen program.
From the perspective of homotopy type theory, the same construction extracts
The boundary between logic and mathematics is blurred with the two manifestations of a common construction, here dependent product.
Research into type-theoretic treatments of modal logic continues.
Some highly structured modalities have been shown to capture continuity and smoothness (cohesive and differential homotopy type theory). In the latter, working in the context of infinitesimal neighbourhoods allows constructions of partial differential equations. More elaborate contexts allow the expression of prequantum field theory.
For quantum physics we need the linear variant of homotopy type theory.
Now a great deal of physics may be written out, see Differential cohomology in a cohesive ∞-topos. General covariance is neatly expressed in type theory.
Non-reversible processes may also require a directed version.
The workshop will consist of tutorials and talks.
Welcome and coffee, 11.30-11.50
Introductory remarks, 11.50-12.00
LUNCH (provided in situ)
Tutorial 2: 14.00-15.00 Ansten Klev (Prague), Constructive type theory
Tutorial 3: 15.05-16.05 Zhaohui Luo (Royal Holloway), MTT-semantics is both model-theoretic and proof-theoretic (slides)
COFFEE BREAK
19.30 Workshop dinner (Venue The Dolphin pub)
COFFEE BREAK
LUNCH (Gulbenkian or elsewhere)
END
Sorry but there is no more funding for this event. For any enquiries contact me at d.corfield@kent.ac.uk.