Geometrisation of First-Order Logic

Bulletin of Symbolic Logic 21 (2):123-163 (2015)
  Copy   BIBTEX


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.



    Upload a copy of this work     Papers currently archived: 93,296

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Geometrisation of first-order logic.Roy Dyckhoff And Sara Negri - 2015 - Bulletin of Symbolic Logic 21 (2):123-163.
Geometric Rules in Infinitary Logic.Sara Negri - 2021 - In Ofer Arieli & Anna Zamansky (eds.), Arnon Avron on Semantics and Proof Theory of Non-Classical Logics. Springer Verlag. pp. 265-293.
Classifying toposes for first-order theories.Carsten Butz & Peter Johnstone - 1998 - Annals of Pure and Applied Logic 91 (1):33-58.
Generalising canonical extension to the categorical setting.Dion Coumans - 2012 - Annals of Pure and Applied Logic 163 (12):1940-1961.
Proof Theory for Functional Modal Logic.Shawn Standefer - 2018 - Studia Logica 106 (1):49-84.
A characterization theorem for geometric logic.Olivia Caramello - 2011 - Annals of Pure and Applied Logic 162 (4):318-321.
Strongly Millian Second-Order Modal Logics.Bruno Jacinto - 2017 - Review of Symbolic Logic 10 (3):397-454.


Added to PP

65 (#256,004)

6 months
24 (#121,857)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Proof analysis for Lewis counterfactuals.Sara Negri & Giorgio Sbardolini - 2016 - Review of Symbolic Logic 9 (1):44-75.
From Display to Labelled Proofs for Tense Logics.Agata Ciabattoni, Tim Lyon & Revantha Ramanayake - 2018 - In Anil Nerode & Sergei Artemov (eds.), Logical Foundations of Computer Science. Springer International Publishing. pp. 120 - 139.
The Apperception Engine.Richard Evans - 2022 - In Hyeongjoo Kim & Dieter Schönecker (eds.), Kant and Artificial Intelligence. De Gruyter. pp. 39-104.
Proof theory for quantified monotone modal logics.Sara Negri & Eugenio Orlandelli - 2019 - Logic Journal of the IGPL 27 (4):478-506.

View all 14 citations / Add more citations