Witness Theory

<p>This book is concerned with the mathematical analysis of the concept of formal proof in classical logic and records - in substance - a longer exercise in applied λ-calculus.<br />Following colloquialisms going back to L. E. J. Brouwer the objects of study in this enterprise are called witnesses. A witness is meant to represent the logical proof of a classically valid formula in a given proof-context. The formalisms used to express witnesses and their equational behaviour are extensions of the pure `typed' λ-calculus considered as equational theories.<br />Formally a witness is generated from decorated - or `typed' - witness variables representing assumptions and witness operators representing logical rules of inference.<br />The equational specifications serve to define the witness operators.<br />In general this can be done by ignoring the `typing' i.e. the logic formulas themselves.<br />Model-theoretically the witnesses are objects of an extensional Scott λ-model.<br /><br />The approach - called generically `witness theory' - is inspired from work of N. G. de Bruijn on a mathematical theory of proving done during the late 1960s and the early 1970s at the University of Eindhoven (The Netherlands) and is similar to the approach behind the Curry-Howard Correspondence familiar from intuitionistic logic.<br /><br />For the classical case the decorations - oft called `types' - are classical logic formulas.<br />At quantifier-free level the equational theory of concern is the λ-calculus with `surjective pairing' and some subsystens thereof appropriately decorated.<br />The extension to propositional first- and second-order quantifiers is straightforward.<br /><br /><br />The book consists of a collection of notes and papers written and circulated during the last ten years as a continuation of previous research done by the author during the nineteen eighties.<br />Among other things it includes a survey of the origins of modern proof theory - Frege to Gentzen - from a witness-theoretical point of view as well as a characteristic application of witness theory to a practical logic problem concerning axiomatisability.</p>