BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:Model Theory ex Proof-search - Alexander Gheorghiu
(University College London)
DTSTART:20220506T130000Z
DTEND:20220506T140000Z
UID:TALK4861AT
URL:/talk/index/4861
DESCRIPTION:*Zoom details*\n\n* Link: https://bham-ac-uk.zoom.
us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBam1IU
T09\n* Meeting ID: 818 7333 5084\n* Passcode: 217\
n\n*Abstract*\n\n\nWe consider a new approach to p
roving soundness and completeness that bypasses tr
uth-in-a-model to work directly with validity. Ess
entially\, one proves soundness and completeness f
or an (object-)logic by studying proof-search in a
meta-logic. The method proceeds through the persp
ective of reductive logic (as opposed to the more
traditional paradigm of deductive logic)\, using p
roof-search spaces as a medium for showing the beh
avioural equivalence of provability in the object-
logic's sequent calculus and provability in a calc
ulus of validity\, which is sound and complete wit
h respect to the models considered. The work cent
res around a particular case study: the logic of B
unched Implications -- the free combination of int
uitionistic propositional logic and multiplicative
intuitionistic linear logic. This logic is chosen
as its meta-theory is quite complex\, which has r
esulted in much consternation with regards to its
model theory\; for example\, the literature on BI
contains many similar but ultimately different alg
ebraic structures and satisfaction relations that
either capture only fragments of the logic (albeit
large ones) or have complex clauses for certain c
onnectives (e.g.\, Beth's clause for disjunction r
ather than Kripke's). Such complexities serve to e
xpose the merits and demerits of the proposed new
approach to model theory.
LOCATION:LG23\, SoCS and Zoom (see abstract for link)
CONTACT:Tom de Jong
END:VEVENT
END:VCALENDAR