Model Theory ex Proof-search

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

• Alexander Gheorghiu (University College London)
• Friday 06 May 2022, 14:00-15:00
• LG23, SoCS and Zoom (see abstract for link).

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

Zoom details

• Link: https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBam1IUT09
• Meeting ID: 818 7333 5084
• Passcode: 217

Abstract

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.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• LG23, SoCS and Zoom (see abstract for link)
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.