Logics of Statements in Context – The Case of Many-Sorted First-Order Logic

Logics of Statements in Context have been recently proposed as a general framework to describe and relate, in a uniform and unifying way, a broad spectrum of logics and specification formalisms which also comprise “open formulas”. The concept of “statement in context” is our novel proposal to formalize, in an adequate way, the rather informal concept of “open formula”. In the talk we address the special case of traditional Many-Sorted First-Order Logic. We discuss that any many-sorted first-order signature Sigma with predicate and (!) operation symbols gives rise to an institution FL(Sigma) of Sigma-statements in context. As a methodological side-effect, we provide some evidence that we are not fatefully doomed to formalize variables by means of signature extensions when we do “abstract model theory”! At the end of the talk, we intend to outline the following constructions and results: Assigning to each many-sorted first-order signature Sigma the institution FL(Sigma) defines a functor from the category of many-sorted signatures into the category of institutions and comorphisms. We can construct a corresponding Grothendieck institution FL# which turns out to be indeed a conservative extension of the traditional institution of Many-Sorted First-Order Logic only comprising “closed formulas”.
Uwe Wolter
Last modified: Tue Jun 10 2025