Abstract

The purpose of this talk is to pose the question, “What are the Euclid’s postulates for syntactic metatheory?”

In the fourth century B.C.E., the Greek mathematician Euclid set down his famous postulates for plane geometry, explaining geometric shapes in terms of rules that govern their construction and incidence. The dialectical relationship between theories (axioms) and their models (coordinate systems) has been the driving force in the last two millennia of geometrical investigation.

In logic and computer science, workers in the “syntactic metatheory” investigate questions that lie on the fringe between a theory and its models — definability, normalization, decidability, conservativity, computational adequacy, parametricity, type safety, etc. Dominant methods attack these questions by means of explicit computations (e.g. Kripke logical relations) which practitioners have found to be both reliable and somewhat opaque. In this talk, I introduce Synthetic Tait computability — a new system of axioms that transforms these explicit computations into synthetic manipulations; classical Kripke logical relations can be seen as models or “coordinate systems” for the new geometry of syntax that is beginning to unfold.

Synthetic Tait computability has already been employed to positively resolve the normalization and decidability conjectures for cubical type theory, as well as a number of other recent results.