Date(s) : 04/12/2014 iCal
15 h 30 min - 16 h 30 min
Hypersequent calculus, introduced by Arnon Avron, is an extension of the ordinary sequent calculus that deals with disjunctions of sequents. Historically it has been a tool for studying intermediate logics and many-valued logics (so-called fuzzy logics), but it is interesting in its own right as a proof system with a well-behaved cut-elimination procedure.
In this talk, I will discuss some aspects of hypersequents, that could be hopefully meaningful to those who are not interested in fuzzy logics at all. The topics include:
• Brouwer’s fixed point theorem and cut-elimination: a potential link.
• Algebraic cut-elimination a la Maehara and Okada: success and failure.
• Takeuti-Titani’s density rule: elimination and algebraic interpretation.
[http://www.kurims.kyoto-u.ac.jp/~terui/]
Catégories Pas de Catégories