The fibrational formulation of intuitionistic predicate logic. I: Completeness according to Gödel, Kripke, and Läuchli. Part 2 (Q1317969): Difference between revisions

[Reviewed together with the preceding paper.] These two papers formulate and prove some versions of completeness theorems for predicate logic. This is done entirely in the spirit of ``algebraic logic'', or ``functorial semantics'', where all syntactical constructs are replaced by certain algebraic objects. In the modern formulation, going back to \textit{W. Lawvere's} ``Equality in hyperdoctrines\dots'' [Applications of categorical algebra, Proc. Symp. Pure Math. 17, 1-14 (1970; Zbl 0234.18002)], these algebraic objects are fibered categories. The arrows of the base category are to be thought of as the terms of the theory in question, and the categories forming the fibres have as arrows entailments, or in the more sophisticated version, proofs of entailments. The Gödel- and Kripke-completeness theorems can now be formulated as embedding (or representation) results for fibered categories of the unsophisticated kind, meaning that the fibre categories are just partially ordered sets. The Läuchli-completeness result, on the other hand, allows for fibres which are genuine categories; this reflects the distinction between different proofs of the same entailment (which was part of the motivation in Läuchli's original work, where the idea of ``proof bundle'' was introduced [\textit{H. Läuchli}, Intuitionism and proof theory, Proc. Summer Conf. Buffalo N.Y. 1968, 227-234 (1970; Zbl 0216.005)]. The embedding is in this case into fibered categories deriving from the category of sets-equipped-with-a-permutation. It is only asserted that ``free'' Heyting-fibrations may be so represented, and it is stated that these are ``exactly the ones that one obtains from an arbitrary theory in intuitionistic predicate logic as the structure of proofs''. The detailed explication of this point is promised to appear in the author's (still unpublished) paper: ``The fibrational formulation of intuitionistic predicate logic. II: The algebra of proofs''.