Cartesian logic (Q1605480)

In 1976, \textit{Michel Coste} introduced a formal syntax for the logic intrepretable in cartesian (that is, finitely complete) categories. (His work, which refined and improved on earlier ideas of J. R. Isbell, O. Keane and H. Volger, was published in Coste's paper ``Localisation, spectra and sheaf representation'' [in: M. P. Fourman et al. (eds.), Applications of sheaves, Lect. Notes Math. 753, 212-238 (1979; Zbl 0422.18007)]. For a modern account of it, see chapter D1 of the reviewer's book [Sketches of an elephant: a topos theory compendium, Oxford University Press (2002; Zbl 1071.18001)].) One feature of Coste's syntax is that the formulae and the theorems of a cartesian theory must be defined by a simultaneous recursion: until you know what you can prove in a theory, you cannot tell which instances of existential quantification are permitted. In the present paper (which, typically for its author, contains no reference to Coste or to anyone else who has worked in this area), the author develops a new syntax for cartesian logic, which is very similar to Coste's, but has the feature that its primitive assertions (`unique existential entailments') are defined `once for all'; the price which one pays for this is a set of rules of inference which are considerably more complicated than those of Coste's logic. Nevertheless, the author proves the completeness of his logic, in the sense that every cartesian theory has a conservative universal model in a cartesian category, and that every (small) cartesian category contains the universal model of some cartesian theory. (At least, he claims completeness: the section of the paper which should contain the proof of universality is in effect left as an exercise for the reader, with the comment: `The proof that this is so is a task worth doing. It is to be hoped that someone actually does it'.) In the final section of the paper, the author introduces what he calls `alternating logic', which is a similar reworking of the `disjunctive logic' introduced by the reviewer in ``A syntactic approach to Diers' localizable categories'' [Lect. Notes Math. 753, 466-478 (1979; Zbl 0421.03050)].