Hostname: page-component-cd9895bd7-dzt6s Total loading time: 0 Render date: 2024-12-23T00:48:26.125Z Has data issue: false hasContentIssue false
  • English
  • Français

GEOMETRISATION OF FIRST-ORDER LOGIC

Published online by Cambridge University Press:  04 June 2015

ROY DYCKHOFF  and
SARA NEGRI
ROY DYCKHOFF
Affiliation:
SCHOOL OF COMPUTER SCIENCE JACK COLE BUILDING, NORTH HAUGH UNIVERSITY OF ST ANDREWS ST ANDREWS, FIFE, KY 16 9SX, UKE-mail: [email protected]
SARA NEGRI
Affiliation:
DEPARTMENT OF PHILOSOPHY P.O. BOX 24 (UNIONINKATU 40 A), 00014 UNIVERSITY OF HELSINKI, FINLANDE-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

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.

Keywords

coherent implicationcoherent logicgeometric logicconservative extensionweakly positive formula
Type
Articles
Information
Bulletin of Symbolic Logic , Volume 21 , Issue 2 , June 2015 , pp. 123 - 163
Copyright
Copyright © The Association for Symbolic Logic 2015 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Antonius, W., Théories cohérentes et prétopos. Thèse de Maitrise ès Sciences (Mathématiques), Université de Montréal, Montreal, 1975.Google Scholar
Avigad, J., Dean, E., and Mumma, J., A formal system for Euclid’s elements. Review of Symbolic Logic, vol. 2 (2009), pp. 700–767.CrossRefGoogle Scholar
Avron, A., Gentzen-type systems, resolution and tableaux. Journal of Automated Reasoning, vol. 10 (1993), pp. 265–281.CrossRefGoogle Scholar
Barr, M., Toposes without points. Journal of Pure and Applied Algebra, vol. 5 (1974), pp. 265–280.CrossRefGoogle Scholar
Bezem, M., Final Report: Automating Coherent Logic—ACL. http://www.ii.uib.no/acl/acl-report-final.pdf, 2013.Google Scholar
Bezem, M. and Coquand, T., Automating Coherent Logic, Proceedings of LPAR 2005, LNCS 3835, Springer, Berlin, 2005, pp. 246–260.Google Scholar
Bezem, M., Coquand, T., and Waaler, A., Research Proposal: Automating Coherent Logic. http://www.ii.uib.no/acl/description.pdf, 2006.Google Scholar
Bezem, M. and Hendricks, T., On the mechanization of the proof of Hessenberg’s theorem in coherent logic. Journal of Automated Reasoning, vol. 40 (2008), pp. 61–85.CrossRefGoogle Scholar
Blass, A., Topoi and computation. Bulletin of the EATCS, vol. 36 (1988), pp. 57–65.Google Scholar
Blass, A., Does Quantifier-Elimination Imply Decidability?http://math.stackexchange.com/questions/260293/, 2012.Google Scholar
Castellini, C. and Smaill, A., A systematic presentation of quantified modal logics. Logic Journal of the IGPL, vol. 10 (2002), pp. 571–599.CrossRefGoogle Scholar
Chagrov, A. and Zakharyaschev, M., Modal logic, Oxford University Press, Oxford, 1997.CrossRefGoogle Scholar
Ciabattoni, A., Maffezioli, P., and Spandier, L., Hypersequent and Labelled Calculi for Intermediate Logics, In Tableaux 2013 Proceedings, LNCS 8123, Springer, Heidelberg, 2013, pp. 81–96.Google Scholar
van Dalen, D, Logic and Structure, third ed., Springer, Berlin, 1997.Google Scholar
Dyckhoff, R., Contraction-free calculi for intuitionistic logic, this Journal, vol. 57 (1992), pp. 795–807.Google Scholar
Dyckhoff, R., Implementations of Coherentisations of First-order Logic, http://rd.host.cs.st-andrews.ac.uk/logic/nonmac/, School of Computer Science, University of St Andrews, 2014.Google Scholar
Dyckhoff, R. and Lengrand, S., LJQ: A Strongly Focused Calculus For Intuitionistic Logic, In CiE 2006 Proceedings, LNCS 3988, Springer, 2006, pp. 173–185.Google Scholar
Dyckhoff, R. and Negri, S., Proof analysis in intermediate logics. Archive for Mathematical Logic, vol. 51 (2012), pp. 71–92.CrossRefGoogle Scholar
Dyckhoff, R. and Negri, S., An idempotent coherentisation algorithm. MS. In preparation, 2015.Google Scholar
Fisher, J., CoFOL Report and User Guide, www.csupomona.edu/∼jrfisher/colog2012/reports/coFOL.pdf, 20 April 2012.Google Scholar
Fisher, J. and Bezem, M., Query Completeness of Skolem Machine Computations, Machines, Computations and Universality, 2007 Proceedings, LNCS 4664, Springer, 2007, pp. 182–192.Google Scholar
Fisher, J. and Bezem, M., Skolem machines, Fundamenta Informaticae, vol. 91 (2009), pp. 79–103.CrossRefGoogle Scholar
Freyd, P., Aspects of topoi. Bulletin of the Australian Mathematical Society, vol. 7 (1972), pp. 1–76.CrossRefGoogle Scholar
Harrison, J., Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, New York, NY, 2009.CrossRefGoogle Scholar
van Heijenoort, J, From Frege to Gödel, Harvard University Press, Cambridge, MA, 1967.Google Scholar
Hilbert, D. and Bernays, P., Foundations of mathematics I, Translated from German “Grundlagen der Mathematik I”, second ed., (1968) (C.-P. Wirth, editor), College Publications, London, 2011.Google Scholar
Hodges, W., Model Theory, Cambridge University Press, Cambridge, 1993.CrossRefGoogle Scholar
Holen, B., Hovland, D., and Giese, M., Efficient Rule-Matching for Hyper-Tableaux, 9th International Workshop on Implementation of Logics Proceedings, EasyChair Proceedings in Computing Series, vol. 22, EasyChair, 2013, pp. 4–17.Google Scholar
Jervell, H., Thoralf Skolem: Pioneer of computational logic. Nordic Journal of Philosophical Logic, vol. 1 (1996), pp. 107–117.Google Scholar
Johnstone, P., Stone Spaces, Cambridge University Press, Cambridge, 1982.Google Scholar
Johnstone, P., Sketches of an Elephant: A Topos Theory Companion, I and II, Oxford Logic Guides, vol. 43, 44, Oxford University Press, Oxford, 2002.Google Scholar
López-Escobar, E. G. K., An interpolation theorem for denumerably long formulae. Fundamenta Mathematicae, vol. 57 (1965), pp. 253–272.CrossRefGoogle Scholar
Mac Lane, S. and Moerdijk, I., Sheaves in Geometry and Logic: A First Introduction to Topos Theory, Springer, New York, 1992.Google Scholar
Maffezioli, P., Naibo, A., and Negri, S., The Church-Fitch knowability paradox in the light of structural proof theory. Synthese, vol. 190 (2013), pp. 2677–2716.CrossRefGoogle Scholar
Makkai, M. and Reyes, G. E., First-Order Categorical Logic, Lecture Notes in Mathematics, vol. 611, Springer, Berlin, 1977.CrossRefGoogle Scholar
Marquis, J. P. and Reyes, G. E., The History of Categorical Logic: 1963–1977, Handbook of the History of Logic, vol. 6 (Sets and Extensions in the Twentieth Century), 2012, pp. 689–800.Google Scholar
Minker, J., Overview of disjunctive logic programming. Annals of Mathematics and Artificial Intelligence, vol. 12 (1994), pp. 1–24.CrossRefGoogle Scholar
Mints, G., Classical and Intuitionistic Geometric Logic. Talk at Conference on Philosophy, Mathematics, Linguistics: Aspects of Interaction 2012, http://science-visits.mccme.ru/doc/mints_talk_2012-05-22.pdf, 2012.Google Scholar
Negri, S., Contraction-free sequent calculi for geometric theories, with an application to Barr’s theorem. Archive for Mathematical Logic, vol. 42 (2003), pp. 389–401.CrossRefGoogle Scholar
Negri, S., Proof analysis in modal logic. Journal of Philosophical Logic, vol. 34 (2005), pp. 507–544.CrossRefGoogle Scholar
Negri, S., Proof analysis beyond geometric theories: from rule systems to systems of rules. Journal of Logic and Computation, http://logcom.oxfordjournals.org/content/early/2014/06/13/logcom.exu037, 2014.Google Scholar
Negri, S., Proofs and countermodels in non-classical logics. Logica Universalis, vol. 8 (2014), pp. 25–60.CrossRefGoogle Scholar
Negri, S. and von Plato, J., Structural Proof Theory, Cambridge University Press, Cambridge, 2001.CrossRefGoogle Scholar
Negri, S. and von Plato, J., Proof Analysis, Cambridge University Press, Cambridge, 2011.CrossRefGoogle Scholar
de Nivelle, H and Meng, J., Geometric Resolution: a Proof Procedure Based on Finite Model Search, Proceedings of IJCAR 2006, LNAI 4130, Springer, 2006, pp. 303–317.Google Scholar
OCaml: An industrial strength programming language supporting functional, imperative and object-oriented styles, https://ocaml.org/.Google Scholar
Orevkov, V. P., Glivenko’s Sequence Classes, Logical and logico-mathematical calculi 1, Proceedings of the Steklov Institute of Mathematics, vol. 98 (pp. 131–154 in Russian original), 1968, pp. 147–173.Google Scholar
Palmgren, E., An intuitionistic axiomatisation of real closed fields. Mathematical Logic Quarterly, vol. 48 (2002), pp. 297–299.3.0.CO;2-G>CrossRefGoogle Scholar
von Plato, J, In the shadows of the Löwenheim-Skolem theorem: Early combinatorial analyses of mathematical proofs. Bulletin of Symbolic Logic, vol. 13 (2005), pp. 189–225.CrossRefGoogle Scholar
Polonsky, A., Proofs, types and lambda calculus. PhD thesis, University of Bergen, Bergen, 2011.Google Scholar
Rathjen, M., Notes on proof theory, Leeds University, Leeds, 2014. Unpublished MS.Google Scholar
Reyes, G. E., Sheaves and concepts: a model-theoretic interpretation of Grothendieck topoi. Cahiers de Topologie et Géométrie Différentielle Catégoriques, vol. 18 (1977), pp. 105–137.Google Scholar
Rothmaler, P., Introduction to Model Theory, Taylor and Francis, New York, 2000.Google Scholar
Sacks, G., Saturated Model Theory, W. A. Benjamin Inc, Reading MA, 1972 (Second ed., World Scientific, Singapore, 2009).Google Scholar
Simpson, A., The proof theory and semantics of intuitionistic modal logic. PhD thesis, Edinburgh University, Edinburgh, 1994.Google Scholar
Skolem, T., Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit und Beweisbarkeit mathematischen Sätze nebst einem Theoreme über dichte Mengen, Skrifter I, vol. 4, Det Norske Videnskaps-Akademi, 1920, pp. 1–36. Also in [57, pp. 103–136]. Also (so far as §1 is concerned) in translation in [25, pp. 254–263].Google Scholar
Skolem, T., Selected Works in Logic (Fenstad, J. E., editor), Universitetsforlaget, Oslo, 1970.Google Scholar
Smullyan, R. M., First-Order Logic. Corrected reprint of 1968 original. Dover Pubs. Inc., New York, 1995.Google Scholar
Stojanović, S., Pavlović, V., and Janic̆ić, P., A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs, Proceedings of Automated Deduction in Geometry 2010, LNAI 6877, Springer, Heidelberg, 2011, pp. 201–220.Google Scholar
Troelstra, A. S. and Schwichtenberg, H., Basic Proof Theory, second ed., Cambridge University Press, Cambridge, 2001.Google Scholar
Wraith, G., Generic Galois Theory of Local Rings, Proceedings of Applications of Sheaves, Durham 1977, LNM 753, Springer, New York, 1979, pp 739–767.Google Scholar
Wraith, G., Intuitionistic Algebra: Some Recent Developments in Topos Theory, Proceedings of International Congress of Mathematics, Helsinki, 1978, pp. 331–337.Google Scholar