Department of Mathematics, Utrecht University After a thorough introduction to the ideas and techniques of linear
logic, with a strong emphasis on proof nets for MELL (multiplicative
exponential linear logic), we will, in the second half of this
course, show how the embedding of derivations in standard sequent
calculi for classical (second) order logic into these proof nets,
enables the definition of a proper (deterministic) normalization
procedure for classical sequent calculus: the $tq$-normalization.
This notion of reduction is shown to be strongly normalizing and
confluent (hence it guarantees unique normal forms of classical
derivations). By subsequently narrowing the space of possible
proofs of a given sequent, we eventually end up with an `optimal'
quotient of classical sequent calculus ({\bf LK}$^{\eta}_p$),
in which all standard boolean equivalences (commutativity, associativity
of conjunction, disjunction; involutivity of negation, de Morgan
laws, etc.) are in fact {\em computational isomorphisms}. We will show how the linear approach to the proof theory of (second
order) logic gives us a quite general framework, in which several,
at first sight seemingly unrelated, attempts at the `constructivization'
of classical logic, can be understood. (This, by the way, retrospectively
justifies linear logic's claim at being the `logic behind logic'.)

**Logic**
**L**INEAR **L**OGIC AND **P**ROOF **T**HEORY
**Advanced course**
**Second week**
schellin@math.ruu.nl
**Course description**
**Prerequisites**
None
**Literature**
No specific recommendation