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. |
Year | DOI | Venue |
---|---|---|
2015 | 10.1017/bsl.2015.7 | BULLETIN OF SYMBOLIC LOGIC |
Keywords | Field | DocType |
coherent implication,coherent logic,geometric logic,conservative extension,weakly positive formula | Discrete mathematics,Computational logic,Axiom,Multimodal logic,Proof theory,Theoretical computer science,First-order logic,Conservative extension,Mathematics,Modal,Calculus,Dynamic logic (modal logic) | Journal |
Volume | Issue | ISSN |
21 | 2 | 1079-8986 |
Citations | PageRank | References |
9 | 0.53 | 14 |
Authors | ||
2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Roy Dyckhoff | 1 | 452 | 49.09 |
Sara Negri | 2 | 280 | 24.76 |