Abstract Categorical Logic / Isabelle Bloch / LUW February 22

[jean-yves beziau]

The next session of the Logica Universalis Webinar will be Wednesday February 22 at 4pm CET (Paris-Geneva-Rome)

Speaker:  Isabelle Bloch, Sorbonne, Paris, France

Title of the talk: Abstract Categorical Logic

Abstract: We present in this talk  an abstract categorical logic based on an abstraction of quantifier. More precisely, the proposed logic is abstract because no structural constraints are imposed on models (semantics free). By contrast, formulas are inductively defined from an abstraction both of atomic formulas and of quantifiers. In this sense, the proposed approach differs from other works interested in formalizing the notion of abstract logic and of which the closest to our approach are the institutions, which in addition to be semantics free do not also impose any syntactic contingencies on the structure of formulas. To define the semantical framework in which formulas will be interpreted, we propose to follow the idea from categorical logic which defines the semantical interpretation of formulas from context and as subobjects of an object of a given category. In the spirit of Lawvere’s hyperdoctrines, we use a more abstract notion which generalizes the notion of subobject, standard in category theory: Pitt’s prop-categories. Always in the spirit of categorical logic, we propose a sequent calculus of which we show correctness and completeness for all semantical frameworks defined over any prop-categories. We then study some conditions which allow us to get this completeness result for particular classes of prop-categories.

https://link.springer.com/article/10.1007/s11787-022-00320-w

Associate Organization: GDR IA,  CNRS, presented by  Meghyn Bienvenu 

Chair: Andrei Rodin, Editorial Board LU

Everybody is welcome to join, register here:
https://www.springer.com/journal/11787/updates/23910922
Jean-Yves Beziau
Organizer of LUW and Editor-in-Chief of Logica Universalis
http://www.jyb-logic.org/