Dr. Roy Dyckhoff will give a talk titled, “Geometrisation of first-order logic”.

Abstract:

We show that every first-order theory T has a conservative extension G_T that is a geometric theory. Reasoning problems in T can therefore be replaced by problems in G_T, where the methods of geometric (aka ‘coherent’) logic are applicable. We discuss related work by Skolem (1920), Antonius (1975), Bezem and Coquand (2005), Fisher (2007–..), Polonsky (2011) and Mints (2012).

(A formula is **positive** iff built from atoms using \exists, \land and \lor. A **geometric implication** is the universal quantification of a formula C -> D where C and D are positive. A theory is **geometric** iff axiomatised by geometric implications. Lots of mathematical theories are geometric. Reasoning in a geometric theory usually avoids the unnatural conversions of resolution-based theorem proving, and produces intuitionistically sound proofs)

Joint work with Sara Negri (Helsinki).