The fibrational formulation of intuitionistic predicate logic I: Completeness according to Gödel, Kripke, and Läuchli, part 1

Abstract

Following thepattern of Lawvere’s notion of hyperdoctrine, we single out certain classes of fibrations and use them, in the present paper and its sequel, to give an algebraic framework for the proof theory of intuitionistic predicate calculus. The two papers are organized around representation theorems that correspond to and strengthen the completeness theorems of the title. The present first part deals with the fibrational analog of GodeFs completeness theorem and gives fibrational liftings of well-known categorical constructions. The present first part is a preparation for the main results to be given in the second part. © 1993, Duke University Press. All Rights Reserved.