Abstract categorical logic (Q6043096): Difference between revisions

\textit{K. J. Barwise} [Ann. Math. Logic 7, 221--265 (1974; Zbl 0324.02034)] defined abstractly the notion of logic through two axioms stating that validity is stable under structure isomorphisms and language morphisms, from which mathematically useful extensions of first-order logic have been investigated. The theory of institutions [\textit{J. A. Goguen} and \textit{R. M. Burstall}, J. Assoc. Comput. Mach. 39, No. 1, 95--146 (1992; Zbl 0799.68134)] has been proposed as an extension of Barwise's abstract model theory. This paper proposes to define abstractly the notion of logic by supposing, as in institutions, no commitment to the internal structure of models, supposing in practice that formulas are inductively defined from propositional connectives and an abstraction both of atomic formulas and of quantifiers. The authors use the idea from categorical logic [\textit{P. T. Johnstone}, Sketches of an elephant. A topos theory compendium. I. Oxford: Clarendon Press (2002; Zbl 1071.18001)] to define the semantical interpretation of formulas from context and as subobjects of an object of a given category. The synopsis of the paper goes as follows. \begin{itemize} \item[\S 2] gives some preliminaries on \ prop-categories [\textit{S. Abramsky} (ed.) et al., Handbook of logic in computer science. Vol. 5: Logical and algebraic methods. Oxford: Oxford University Press (2000; Zbl 1035.03001), Chapter 2]. \item[\S 3] formulates the notions of semantical system and abstract quantifiers defining the semantical framework on which the abstract categorical logic is built. \item[\S 4] presents an internal logic whose semantical interpretation is done through semantical systems. The internal logic is defined as an extension of propositional logic by further considering an abstraction of both atomic formulas and quantifiers. The entailment calculus is formulated as a sequent calculus. \item[\S 5] is devoted to the proof of completeness of the entailment calculus. After a general completeness result, some conditions are studied to establish completeness for models restricted to particular classes of prop-categories. \end{itemize}