linear logic, coq, cut-elimination
In proof theory, the cut-elimination theorem (or Hauptsatz, which means main result) is of paramount importance since it implies the consistency and the subformula property for the given system. This theorem states that for any sequent that has a proof using the cut rule, it is possible to find a cut-free proof for the same sequent. The proof of cut-elimination proceeds by induction on the lexicographical order (formula weight, cut height) and generates multiple cases, considering for instance, when the cut-formula is or not principal. In general, one must consider the last rule applied in the two premises immediately after applying the cut rule (seeing the proof bottom-up). This generates a considerable amount of cases and then, the demonstration of this theorem could be error prone if we use an informal proof. Linear Logic (LL) is one of the most significant substructural logics and it allows for cut-free sequent calculi. LL is a resource sensible logic and has been widely used in the specification and verification of computer systems. In view of this, it becomes relevant the study of this logic in this work. In this dissertation we formalize three sequent calculi for linear logic in Coq and prove all of them to be equivalent. Additionally, we formalize meta-theorems such as admissibility of cut, generalization of initial rule, bang and copy and invertibility of the rules for the connectives par, bottom, with and quest. Regarding the invertibility, we demonstrate this theorem in two different ways: a version by induction on the height of the derivation and by using the cut rule. This allows us to show how the cut rule greatly simplifies the proofs in the sequent calculus. In order to mitigate the number of several cases in the proofs, we develop several tactics in Coq that allows us to perform semi-automatic reasoning.