![]() |
![]() |
University of Birmingham > Talks@bham > Theoretical computer science seminar > Model Theory ex Proof-search
Model Theory ex Proof-searchAdd 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
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:
Note that ex-directory lists are not shown. |
Other listsType the title of a new list here Test Physics and Astronomy ColloquiaOther talksLet there be light: Illuminating neutron star mergers with radiative transfer simulations TBA Counting cycles in planar graphs Ultrafast Spectroscopy and Microscopy as probes of Energy Materials Topological interfaces, phase transitions, and point-group symmetries – spinor Bose-Einstein condensates as topological-defect laboratories Width parameters and the maximum independent set problem |