Skip to content

Research at St Andrews

Geometrisation of first-order logic

Research output: Contribution to journalArticle

DOI

Open Access permissions

Open

Abstract

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.
Close

Details

Original languageEnglish
Pages (from-to)123–163
Number of pages41
JournalBulletin of Symbolic Logic
Volume21
Issue number2
Early online date4 Jun 2015
DOIs
StatePublished - Jun 2015

    Research areas

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

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Contraction-free sequent calculi in intuitionistic logic: a correction

    Dyckhoff, R. Dec 2018 In : Journal of Symbolic Logic. 83, 4, p. 1680-1682 3 p.

    Research output: Contribution to journalArticle

  2. Indefinite proof and inversions of syllogisms

    Dyckhoff, R. 14 Jul 2018 (Accepted/In press) In : Bulletin of Symbolic Logic. 13 p.

    Research output: Contribution to journalArticle

  3. Analyticity, balance and non-admissibility of Cut in Stoic Logic

    Bobzien, S. & Dyckhoff, R. 20 Apr 2018 In : Studia Logica. First Online, 23 p.

    Research output: Contribution to journalArticle

  4. Intuitionistic decision procedures since Gentzen

    Dyckhoff, R. 5 May 2016 Advances in Proof Theory. Kahle, R., Strahm, T. & Studer, T. (eds.). Birkhäuser Basel, p. 245-267 (Progress in Computer Science and Applied Logic; vol. 28)

    Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

Related by journal

  1. Indefinite proof and inversions of syllogisms

    Dyckhoff, R. 14 Jul 2018 (Accepted/In press) In : Bulletin of Symbolic Logic. 13 p.

    Research output: Contribution to journalArticle

ID: 181704500