Logics of Statements in Context – First-Order Logic Files

Logics of Statements in Context have been 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”. Especially, it has been shown that we can define arbitrary first-order “open formulas” in arbitrary categories. At present, there are two deficiencies. In the general case only signatures with predicate symbols are considered and institutions of statements in context are only defined for single signatures. In this paper we elaborate the special case of traditional many-sorted First-Order Logic. We show that any many-sorted first-order signature Σ with predicate and (!) operation symbols gives rise to an institution FLΣ of Σ-statements in context, and that any signature morphism results in a comorphism between the corresponding institutions. We prove that we obtain a functor FL:Sig→coIns from the category of signatures into the category of institutions and comorphisms. We construct a corresponding Grothendieck institution FL♯ and prove that FL♯ is indeed an extension of the traditional institution of First-Order Logic which only comprises “closed formulas”. We also investigate substitutions in detail and discuss (elementary) diagrams in the sense of traditional First-Order Logic.