|Résumé||Proof theory is the study of proofs as mathematical objects in their own right. Infinite proofs (eg. infinite descent proofs) are pervasive in mathematics. A formal way of characterizing such proofs can be done by looking at fixed point logics (eg. mu calculus) from proof-theoretic lenses. Baelde et. al. have proposed an infinitary sequent calculus (i.e. infinitely deep, finitely wide proofs) for linear logic with fixed points (muMALL). In this talk, following a brief history of proof theory and infinite proofs, I will introduce muMALL. However, the sequent calculus of muMALL turns out to be ``too sequential". In order to achieve more liberal cut elimination, we have devised infinets which are proofs nets (à la Curien) for the multiplicative fragment (muMLL). The later part of the talk will focus on infinets and ongoing work on these nets.
Joint work with: Alexis Saurin, Luc Pellisier |