ABSTRACT
Professor Roberto Magari is remembered for the depth and clarity of his lectures which impressed students and colleagues alike. Indeed he championed the deepening of logic through algebraic models and the clarification of algebra through explicit recognition of logic. In that spirit, I here model the basic construction of proof theory as the left bi-adjoint to the inclusion of Posets into Categories. That simple description has a rich history, some of which I here recall. Its specific content stems from the analysis, within such bicategories, of quantifiers and implications as cases of Kan’s notion of adjoint. The construction leads to some open algebraic problems concerning known classes of locally-cartesian-closed categories and their role as models for proof theory.
