 Witness Theory
Notes on λcalculus and Logic
Adrian Rezuş
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. 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 proofcontext. The formalisms used to express witnesses and their equational behaviour are extensions of the pure `typed' λcalculus, considered as equational theories. Formally, a witness is generated from decorated  or `typed'  witness variables, representing assumptions, and witness operators, representing logical rules of inference. The equational specifications serve to define the witness operators. In general, this can be done by ignoring the `typing', i.e., the logic formulas themselves. Modeltheoretically, the witnesses are objects of an extensional Scott λmodel.
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 CurryHoward Correspondence, familiar from intuitionistic logic.
For the classical case, the decorations  oft called `types'  are classical logic formulas. At quantifierfree level, the equational theory of concern is the λcalculus with `surjective pairing' and some subsystens thereof, appropriately decorated. The extension to propositional, first and secondorder quantifiers is straightforward.
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. Among other things, it includes a survey of the origins of modern proof theory  Frege to Gentzen  from a witnesstheoretical point of view, as well as a characteristic application of witness theory to a practical logic problem concerning axiomatisability.
9781848903265
