University of Birmingham > Talks@bham > Theoretical computer science seminar > Model Theory ex Proof-search

Model Theory ex Proof-search

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Tom de Jong.

Zoom details


We consider a new approach to proving soundness and completeness that bypasses truth-in-a-model to work directly with validity. Essentially, one proves soundness and completeness for an (object-)logic by studying proof-search in a meta-logic. The method proceeds through the perspective of reductive logic (as opposed to the more traditional paradigm of deductive logic), using proof-search spaces as a medium for showing the behavioural equivalence of provability in the object-logic’s sequent calculus and provability in a calculus of validity, which is sound and complete with respect to the models considered. The work centres around a particular case study: the logic of Bunched Implications—the free combination of intuitionistic propositional logic and multiplicative intuitionistic linear logic. This logic is chosen as its meta-theory is quite complex, which has resulted in much consternation with regards to its model theory; for example, the literature on BI contains many similar but ultimately different algebraic structures and satisfaction relations that either capture only fragments of the logic (albeit large ones) or have complex clauses for certain connectives (e.g., Beth’s clause for disjunction rather than Kripke’s). Such complexities serve to expose the merits and demerits of the proposed new approach to model theory.

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.