Formalising the Institution for First-Order Logic in an
Interactive Proof Assistant
This talk will focus on a formalisation of a fragment of the theory of
institutions in the Coq proof assistant, specifically on the
formalisation of the institution for first-order logic with equality
and the proof of its satisfaction condition. I will talk about
formalisation: its role in mathematics in general and institution
theory in particular. I will include some details about how the
mathematical objects of institution theory are represented -
especially first-order quantifiers - and how they differ from their
set-theoretic counterparts, with a focus on accuracy of representation
and threats to validity, rather than getting mired in the technical
merits and demerits of particular modelling choices. Time permitting,
I will also describe some very preliminary attempts to do
institution-independent model theory in Coq.
Conor Reynolds
Last modified: Wed June 19 2024