General proof theory addresses the question "What is a proof?" by dealing with questions related to normal forms of proofs, and in particular with the question of identity criteria for proofs. It deals with the structure of proofs, as exhibited, for example, with the help of the typed lambda calculus in the Curry-Howard correspondence, and not with their strength measured by ordinals, which is what one finds in proof theory that arose out of Hilbert's programme.

Much of general proof theory is the field of categorial proof theory. Fundamental notions of category theory like the notion of adjoint functor, and very important structures like cartesian closed categories, came to be of central concern for logic in that field. Through results of categorial proof theory called coherence results, which provide a model theory for equality of proofs, logic finds new ties with geometry, topology and algebra.

In general proof theory one looks for an algebra of proofs, and for that one concentrates on the operations of this algebra, which come with the inference rules. As an equational theory, the algebra of proofs involves the question of identity criteria for proofs, the central question of general proof theory. (This question may be found, at least implicitly, in Hilbert's 24th problem; see: https://www.mi.sanu.ac.rs/~kosta/Dosen_General%20Proof%20Theory%20nov2011.pdf). This is still a young branch of logic, to whose development contributions were made in the Belgrade school.

The seminar started in the autumn of 2011, and its chairman is Kosta Dosen. It is not expected to meet more than once a month during the academic year.

GALLERY