Por Matteo Manighetti (Inria Saclay & LIX, École Polytechnique, Palaiseau, France).
Linear Logic uncovered many hidden structures in the proof theory of classical and intuitionistic logic. An important property of Linear Logic, that was later also found in classical and intuitionistic logic, is the availability of focused proof systems: these are sequent calculi that drastically restrict the non-determinism associated with usual sequent calculi. The fact that they remain a sequent calculus at the core, while gaining stronger normal forms, provided a good setting for several results in computer science. Some focused proof systems have been proposed for systems of arithmetic, aiming at applications in theorem proving and model checking. However, this is also a setting where some classical results of the metatheory of arithmetic can be studied. In this talk, I will present a focused proof system for the theory of inductive definitions in Multiplicative-Additive Linear Logic (a linear logic without weakening and contraction) due to D. Baelde, as well as some early applications to the metatheory of arithmetic.
Zoom Meeting | ID da reunião: 890 8479 3299 - senha de acesso: 409604
