Quantifier-complete categories (Q1238805): Difference between revisions

lt is well known (for good exposition cf. \textit{C. R. Mann} [Proc. Lond. math. Soc., III. Ser. 31, 289-310 (1975; Zbl 0317.02036)]) that the intuitionistic propositional calculus in the language \(\&,\supset,T\)(ruth) is turned into a cartesian closed category by taking formulas as objects, \(\&,\supset,T\) as product, exponent and terminal object respectively and derivations \(f:A\to B\) as morphisms. More precisely, morphisms are the equivalence classes of derivations modulo equivalence \(f\equiv g:f, g\) are interconvertible using conversions employed in normalization (cutelimination). Moreover, this category is free (the smallest in a natural class). This observation was extended to the language containing \(\vee,\perp\) but the detailed proofs seem to be never published. In the paper under review the author extends the observation to intuitionistic propositional calculus with infinitary conjunction and disjunction. For many details the reader is referred either to previous publications by the author or to proof-theoretic literature or to the author's paper [Notre Dame J. formal Logic 18, 441-457 (1977; Zbl 0258.02038)]. Finitary quantifiers are interpreted in the familiar way by infinitary conjunctions and disjunctions, hence the name quantifier-complete. Infinitary derivations obtained via this translation from finitary derivations of formulas containing quantifiers are called finitary constructible. The equivalence of finitary constructible derivations is said to be decided via certain normal form defined using more than 20 kinds of reductions with additional conditions. The proof depends on the Church-Rosser theorem and is not given, but it should contain more than \(20^2\) cases (with subcases according to interrelations of additional conditions). This is the price of using antecedent-succedent rules instead of natural deduction formulation where no additional reduction is needed after cutelimination. Familiar results concerning intuitionistic underivability of sequents like \(\forall x(p\vee Fx)\to p\vee\forall xFx\) are used to prove that certain limits cannot be interchanged. Some remarks and definitions seem to be in need of clarification. The relation \(\equiv^*\) (top p. 101) is defined via replacement only of outermost quantifiers and is neither a congruence nor transitive. The congruence relation \(\equiv_0\) identifies the obvious derivation of \(\forall xPx\to\forall yPy\) with 1, which is not the rase for familiar equivalence of derivations. It is not quite clear what is understood by ``proof-theoretical possibility'' in the definition of a normal derivation (bottom p. 107) and by equivalence of two notions of normality at the end of \S6 (cf. \textit{J. Zucker} [Ann. math. Logic 7, 1-112 (1974; Zbl 0298.02023), \S1]).