Logic	LINEAR LOGIC AND PROOF THEORY
Advanced course	HAROLD SCHELLINX Department of Mathematics, Utrecht University
Second week	schellin@math.ruu.nl
Course description	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'.)
Prerequisites	None
Literature	No specific recommendation