We introduce sequent calculus, its structural rules and the logical rules for the logical connective $\land$. We then limit the sequent calculus to linear logic nad split $\land$ into two connectives. We further introduce all other connectives in linear logic and explain their interpretations, then we introduce the cut rule. We formulate the cut elimination theorem then ascribe a numeric value, called degree, to each cut and prove the theorem using double induction, the outer induction on the number of cuts in the proof tree, the inner induction on the degree of the cut. Within the induction we split cases based on the type of cut and the formula being cut. We define the principal cut and lower its degree it for each connective seperately. We define the generalised cut rule for the exponentials and lower its degree. We lower the degree of the non-principal cut rule (and the non-principal generalised cut rule) and then proceed to the induction base, with which we finish the proof.
|
