Geometrisation of first-order logic

Roy Dyckhoff, Sara Negri

Research output: Contribution to journalArticlepeer-review

25 Citations (Scopus)


That every first-order theory has a coherent conservative extension is regarded by some as obvious, even trivial, and by others as not at all obvious, but instead remarkable and valuable; the result is in any case neither sufficiently well-known nor easily found in the literature. Various approaches to the result are presented and discussed in detail, including one inspired by a problem in the proof theory of intermediate logics that led us to the proof of the present paper. It can be seen as a modification of Skolem’s argument from 1920 for his “Normal Form” theorem. “Geometric” being the infinitary version of “coherent”, it is further shown that every infinitary first-order theory, suitably restricted, has a geometric conservative extension, hence the title. The results are applied to simplify methods used in reasoning in and about modal and intermediate logics. We include also a new algorithm to generate special coherent implications from an axiom, designed to preserve the structure of formulae with relatively little use of normal forms.
Original languageEnglish
Pages (from-to)123–163
Number of pages41
JournalBulletin of Symbolic Logic
Issue number2
Early online date4 Jun 2015
Publication statusPublished - Jun 2015


  • Coherent implication
  • Coherent logic
  • Geometric logic
  • Weakly positive formula


Dive into the research topics of 'Geometrisation of first-order logic'. Together they form a unique fingerprint.

Cite this