National Autonomous University of Mexico (UNAM)
Abstract: In this talk, I will present the ongoing work to relate different deduction systems for constructive logic S4. Continuing our previous work, an equivalence between axiomatic and natural deduction, we study the equivalence between them with a dual-context sequent calculus. Sequent system GS4 uses sequents with two contexts to capture the notions of global and local truths without resorting to any formal semantics. Moreover, the dual-context approach allows us to manipulate modal formulas in the contexts by considering them as pure (non-modal) propositions and vice versa. This feature considerably simplifies the actual construction of proofs and sometimes allows us to replace modal reasoning with a simpler propositional one.
Joint work with Favio Miranda and Selene Linares.
Horário: 11:00 (UTC-3)