Type Theory, Constructive Mathematics and Geometric Logic / Théorie des types, mathématiques constructives et logique géométrique

Collection Type Theory, Constructive Mathematics and Geometric Logic / Théorie des types, mathématiques constructives et logique géométrique

Organizer(s) Coquand, Thierry ; Negri, Sara ; Rathjen, Michael ; Schuster, Peter

Date(s) 01/05/2023 - 05/05/2023

linked URL https://conferences.cirm-math.fr/2319.html

00:00:00 / 00:00:00

5 5

From axioms to synthetic inference rules via focusing

Gentzen's sequent calculus can be given additional structure via focusing. We illustrate how that additional structure can be used to construct synthetic inference rules. In particular, bipolar formulas (a slight generalization of geometric formulas) can be converted to such synthetic rules once polarity is assigned to the atomic formulas and some logical connectives. Since there is some flexibility in the assignment of polarity, a given formula might yield several different synthetic rules. It is also the case that cut-elimination immediately holds for these new inference rules. Such conversion of bipolar axioms to inference rules can be done in classical and intuitionistic logics. This talk is based in part on a paper in the Annals of Pure and Applied Logic co-authored with Sonia Marin, Elaine Pimentel, and Marco Volpe (2022).

Information about the video

Date of recording 04/05/2023
Date of publication 15/05/2023
Institution CIRM
Licence CC BY NC ND
Language English
Audience Researchers, Graduate Students
Director(s) Guillaume Hennenfent
Format MP4

Citation data

DOI 10.24350/CIRM.V.20040703
Cite this video Miller, Dale (04/05/2023). From axioms to synthetic inference rules via focusing. CIRM. Audiovisual resource. DOI: 10.24350/CIRM.V.20040703
URL https://dx.doi.org/10.24350/CIRM.V.20040703

Domain(s)

Logic in Computer Science

Bibliography

MARIN, Sonia, MILLER, Dale, PIMENTEL, Elaine, et al. From axioms to synthetic inference rules via focusing. Annals of Pure and Applied Logic, 2022, vol. 173, no 5, p. 103091. - https://doi.org/10.1016/j.apal.2022.103091

MSC codes

Last related questions on MathOverflow

You have to connect your Carmin.tv account with mathoverflow to add question

Ask a question on MathOverflow

All the collection videos

52:12

published on May 15, 2023

On a decomposition of WKL!!

By Takako Nemoto

55:38

published on May 15, 2023

New modal operators for constructive mathematics

By Ingo Blechschmidt

58:06

published on May 15, 2023

Recursive inequalities in applied proof theory

By Thomas Powell

58:27

published on May 15, 2023

Compact ordinals in HoTT/UF

By Martin Escardó

46:40

published on May 15, 2023

From axioms to synthetic inference rules via focusing

By Dale Miller

Copyright Carmin.tv 2024

Give feedback