[Settfa] Tuesday 10 Dec, Amir Tabatabai

[David Bradley-Williams]

Tuesday, 10 December 2024 - 10:00 to 11:30
Place: IM, Žitná 25, konírna

Speaker: Amir Tabatabai, IM CAS
Title: Categorical Proof Theory: An Introduction

Abstract
Proofs are, unfortunately, often regarded as second-class citizens in 
logic—even within their own domain of proof theory. They are typically 
examined to address questions of provability or, more frequently, the 
unprovability of statements within a given theory. Consequently, 
foundational issues such as defining proofs beyond their somewhat 
artificial and syntactic representations, understanding the equality of 
proofs, and characterizing the equivalence of propositions have remained 
largely underexplored.
Categorical proof theory offers a highly successful framework for 
studying proofs in an abstract form, providing the tools to address 
these foundational problems rigorously. Its core idea is to interpret 
proof systems as structured categories, where objects represent 
propositions, and morphisms correspond to proofs.
In this talk, we will begin by revisiting bicartesian closed categories 
(BCCs). We will argue that the bicartesian closed structure is exactly 
the structure of the intuitionistic propositional proofs. Using BCCs as 
the categorical semantics for intuitionistic propositional proofs, we 
will investigate three central problems: the existence of proofs, the 
equality of proofs, and the equivalence of propositions. Additionally, 
we will present concrete completeness results for these problems. If 
time permits, we will also explore classical proof systems and examine 
the BHK interpretation as an alternative perspective.

For more information see the seminar web page at
https://www.math.cas.cz/index.php/events/seminar/6


-- 
David Bradley-Williams PhD
Department of Abstract Analysis
Institute of Mathematics, Czech Academy of Sciences
Žitná 25
115 67 Praha 1
Czech Republic

Tel: +420-222 090 743

Url: http://davidbw.sdf.org/