College Publications logo   College Publications title  
View Basket
Homepage Contact page
Academia Brasileira de Filosofia
Cadernos de Lógica e Computação
Cadernos de Lógica e Filosofia
Cahiers de Logique et d'Epistemologie
Communication, Mind and Language
Comptes Rendus de l'Academie Internationale de Philosophie des Sciences
Cuadernos de lógica, Epistemología y Lenguaje
Encyclopaedia of Logic
Historia Logicae
IfColog series in Computational Logic
Journal of Applied Logics - IfCoLog Journal
Logics for New-Generation AI
Logic and Law
Logic and Semiotics
Logic PhDs
Logic, Methodology and Philosophy of Science
The Logica Yearbook
Neural Computing and Artificial Intelligence
The SILFS series
Studies in Logic
History of Logic
Logic and cognitive systems
Mathematical logic and foundations
Studies in Logic and Argumentation
Logic and Bounded Rationality
Studies in Talmudic Logic
Student Publications
Texts in Logic and Reasoning
Texts in Mathematics
Digital Downloads
Information for authors
About us
Search for Books

Studies in Logic


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 proof-context. 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. Model-theoretically, 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 Curry-Howard Correspondence, familiar from intuitionistic logic.

For the classical case, the decorations - oft called `types' - are classical logic formulas. At quantifier-free level, the equational theory of concern is the λ-calculus with `surjective pairing' and some subsystens thereof, appropriately decorated. The extension to propositional, first- and second-order 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 witness-theoretical point of view, as well as a characteristic application of witness theory to a practical logic problem concerning axiomatisability.


© 2005–2024 College Publications / VFH webmaster