Cartesian logic
type: Item
instance of: scholarly article
title: Cartesian logic
zbMATH Open document ID: 1004.03052
DOI: 10.1016/S0304-3975(00)00328-5
published in: Theoretical Computer Science
publication date: 2002-07-18T00:00:00Z
review text: 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 `disju…
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 18A30
Mathematics Subject Classification ID: 18C50
Mathematics Subject Classification ID: 18D15
zbMATH DE Number: 1768737
zbMATH Keywords: cartesian theory
zbMATH Keywords: syntax
zbMATH Keywords: cartesian logic
zbMATH Keywords: completeness
zbMATH Keywords: conservative universal model
zbMATH Keywords: cartesian category
zbMATH Keywords: alternating logic
zbMATH Keywords: disjunctive logic
author: Peter J. Freyd
reviewed by: Peter Johnstone
MaRDI profile type: Publication
Recommended article: On essentially algebraic theories and their generalizations
Recommended article: Q3693527
Recommended article: Q3142163
Recommended article: Q3768900
Recommended article: Q5215784
Recommended article: Locally cartesian closed categories and type theory
Recommended article: Q3825226
Recommended article: Q4856547
Recommended article: Q3461939
Recommended article: On conceptual completeness of syntactic-semantical systems
description: scientific article; zbMATH DE number 1768737