David Corfield
Type Theory and Philosophy

Contents

Idea of the workshop

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)

Type theory

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.)

Several converging paths

  • Philosophical logic
  • Natural language
  • Constructive mathematics
  • Computer science
  • Category theory

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

  • Groups, groupoids and higher groupoids
  • Univalence
  • Higher inductive types

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 universal quantification corresponding to a dependent type, e.g., ‘All men are mortal’, that is, x:ManMortal(x)\prod_{x:Man} Mortal(x) from x:ManMortal(x):Propositionx:Man \vdash Mortal(x): Proposition.
  • The invariants of a group action, that is *:BGV(*)\prod_{\ast:\mathbf{B} G} V(\ast) from *:BGV(*):Type\ast:\mathbf{B} G \vdash V(\ast):Type.

The boundary between logic and mathematics is blurred with the two manifestations of a common construction, here dependent product.

Ways forward

  • Modalities
  • Continuity and smoothness

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

The workshop will consist of tutorials and talks.

9 June

  • Welcome and coffee, 11.30-11.50

  • Introductory remarks, 11.50-12.00

Tutorials

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

  • Tutorial 4: 16.30-17.30 David Corfield (Kent), Homotopy type theory (slides).

19.30 Workshop dinner (Venue The Dolphin pub)

10 June

Talks

  • 09.30-10.20 Andrei Rodin (Moscow), Geometric Characteristics as an early form of typing

COFFEE BREAK

  • 10.40-11.30 Laura Crosilla (Leeds), Poincaré and Weyl on predicativity and the concept of set in Martin-Löf type theory
  • 11.40-12.30 Luke Burke (UCL), TAG glue semantics

LUNCH (Gulbenkian or elsewhere)

  • 14.00-14.50 Anthony Durity (Cork), The Unity of Form and Content
  • 14.55-15.45 Giuseppe Primiero (Middlesex), (Versions of) Modal Type Theory, (slides)

END

Possible topics

  • Natural language
  • Types and metaphysics
  • Structuralism
  • Identity
  • Modality
  • Constructivity
  • Invariance

Participants

  • Simon Thompson
  • Zhaohui Luo
  • David Corfield
  • Anthony Durity
  • Andrei Rodin
  • Laura Crosilla
  • Luke Burke
  • Ansten Klev
  • Atoosa Kasirzadeh
  • Giuseppe Primiero
  • Joshua Black
  • Wendy Hammache

Contact

Sorry but there is no more funding for this event. For any enquiries contact me at d.corfield@kent.ac.uk.

Revised on June 20, 2016 12:17:45 by David Corfield (129.12.18.218)