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

 HOME PROGRAMME CONTACT REGISTRATION