The Geometry of Interaction

Linear Logic, proposed by Jean-Yves Girard, remains one of the most important and startling developments in the study of logic and human cognition. I would have to place it within the same eschelon as Aristotle's and Frege's works. It is the first major, and successful, move to displace the concept of truth (preservation) and replace it with the notion of computational resources and their consumption in proof, reasoning, etc. This may not seem like much, but consider the practical implications to computer science, epistemology, quantum mechanics, and modeling of actual human cognition. Linear Logic combines some of the best aspects of constructivist approaches with a system that eschews the facile semantics often used to describe logic. The Stanford University site is an excellent resource. About the only thing even more interesting that this modified sequent logic (doing without weaking and contraction in proofs and emphasizing interaction and duality) is Girard's subsequent work on Ludics. More on that later.