A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs

George Tourlakis

Bulletin of the Section of Logic (2016)

  • Volume: 45, Issue: 1
  • ISSN: 0138-0680

Abstract

top
Reference [12] introduced a novel formula to formula translation tool (“formula-tors”) that enables syntactic metatheoretical investigations of first-order modallogics, bypassing a need to convert them first into Gentzen style logics in order torely on cut elimination and the subformula property. In fact, the formulator tool,as was already demonstrated in loc. cit., is applicable even to the metatheoreticalstudy of logics such as QGL, where cut elimination is (provably, [2]) unavailable. This paper applies the formulator approach to show the independence of the axiom schema ☐A → ☐∀ A of the logics M3and ML3 of [17, 18, 11, 13]. This leads to the conclusion that the two logics obtained by removing this axiom are incomplete, both with respect to their natural Kripke structures and to arithmetical interpretations.  In particular, the so modified ML3 is, similarly to QGL, an arithmetically incomplete first-order extension of GL, but, unlike QGL, all its theorems have cut free proofs. We also establish here, via formulators, a stronger version of the disjunction property for GL and QGL without going through Gentzen versions of these logics (compare with the more complexproofs in [2,8]).

How to cite

top

George Tourlakis. "A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs." Bulletin of the Section of Logic 45.1 (2016): null. <http://eudml.org/doc/295542>.

@article{GeorgeTourlakis2016,
abstract = {Reference [12] introduced a novel formula to formula translation tool (“formula-tors”) that enables syntactic metatheoretical investigations of first-order modallogics, bypassing a need to convert them first into Gentzen style logics in order torely on cut elimination and the subformula property. In fact, the formulator tool,as was already demonstrated in loc. cit., is applicable even to the metatheoreticalstudy of logics such as QGL, where cut elimination is (provably, [2]) unavailable. This paper applies the formulator approach to show the independence of the axiom schema ☐A → ☐∀ A of the logics M3and ML3 of [17, 18, 11, 13]. This leads to the conclusion that the two logics obtained by removing this axiom are incomplete, both with respect to their natural Kripke structures and to arithmetical interpretations.  In particular, the so modified ML3 is, similarly to QGL, an arithmetically incomplete first-order extension of GL, but, unlike QGL, all its theorems have cut free proofs. We also establish here, via formulators, a stronger version of the disjunction property for GL and QGL without going through Gentzen versions of these logics (compare with the more complexproofs in [2,8]).},
author = {George Tourlakis},
journal = {Bulletin of the Section of Logic},
keywords = {Modal logic; GL; first-order logic; proof theory; cut elimination; reflection property; disjunction property; quantified modal logic; QGL; arithmetical completeness},
language = {eng},
number = {1},
pages = {null},
title = {A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs},
url = {http://eudml.org/doc/295542},
volume = {45},
year = {2016},
}

TY - JOUR
AU - George Tourlakis
TI - A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs
JO - Bulletin of the Section of Logic
PY - 2016
VL - 45
IS - 1
SP - null
AB - Reference [12] introduced a novel formula to formula translation tool (“formula-tors”) that enables syntactic metatheoretical investigations of first-order modallogics, bypassing a need to convert them first into Gentzen style logics in order torely on cut elimination and the subformula property. In fact, the formulator tool,as was already demonstrated in loc. cit., is applicable even to the metatheoreticalstudy of logics such as QGL, where cut elimination is (provably, [2]) unavailable. This paper applies the formulator approach to show the independence of the axiom schema ☐A → ☐∀ A of the logics M3and ML3 of [17, 18, 11, 13]. This leads to the conclusion that the two logics obtained by removing this axiom are incomplete, both with respect to their natural Kripke structures and to arithmetical interpretations.  In particular, the so modified ML3 is, similarly to QGL, an arithmetically incomplete first-order extension of GL, but, unlike QGL, all its theorems have cut free proofs. We also establish here, via formulators, a stronger version of the disjunction property for GL and QGL without going through Gentzen versions of these logics (compare with the more complexproofs in [2,8]).
LA - eng
KW - Modal logic; GL; first-order logic; proof theory; cut elimination; reflection property; disjunction property; quantified modal logic; QGL; arithmetical completeness
UR - http://eudml.org/doc/295542
ER -

References

top
  1. [1] S. Artemov and G. Dzhaparidze, Finite Kripke Models and Predicate Logics of Provability, J. of Symb. Logic 55 (1990), no. 3, pp. 1090–1098. 
  2. [2] A. Avron, On modal systems having arithmetical interpretations, J. of Symb. Logic 49 (1984), no. 3, pp. 935–942. 
  3. [3] G. Boolos, The Logic of Provability, Cambridge University Press, Cambridge, 1993. 
  4. [4] N. Bourbaki, Éléments de Mathématique; Théorie des Ensembles, Hermann, Paris, 1966. 
  5. [5] H. B. Enderton, A mathematical introduction to logic, Academic Press, New York, 1972. 
  6. [6] F. Kibedi and G. Tourlakis, A modal extension of weak generalisation predicate logic, Logic Journal of the IGPL 14 (2006), no. 4, pp. 591–621. 
  7. [7] F. Montagna, The predicate modal logic of provability, Notre Dame J. of Formal Logic 25 (1984), pp. 179–189. 
  8. [8] G. Sambin and S. Valentini, A Modal Sequent Calculus for a Fragment of Arithmetic, Studia Logica 39 (1980), no. 2/3, pp. 245–256. 
  9. [9] G. Sambin and S. Valentini, The Modal Logic of Provability. The Sequential Approach, Journal of Philosophical Logic 11 (1982), no. 3, pp. 311–342. 
  10. [10] K. Schütte, Proof Theory, Springer-Verlag, New York, 1977. 
  11. [11] Y. Schwartz and G. Tourlakis, On the proof-theory of two formalisations of modal first-order logic, Studia Logica 96 (2010), no. 3, pp. 349–373. 
  12. [12] Y. Schwartz and G. Tourlakis, A Proof Theoretic Tool for First-Order Modal Logic, Bulletin of the Section of Logic 42 (2013), no. 3–4, pp. 93–110. 
  13. [13] Y. Schwartz and G. Tourlakis, On the Proof-Theory of a First-Order Version of GL, J. of Logic and Logical Philosophy 23 (2014), no. 3, pp. 329–363. 
  14. [14] J. R. Shoenfield, Mathematical Logic, Addison-Wesley, Reading, Massachusetts, 1967. 
  15. [15] C. Smoryński, Self-Reference and Modal Logic, Springer-Verlag, New York, 1985. 
  16. [16] G. Tourlakis, Lectures in Logic and Set Theory; Volume 1: Mathematical Logic, Cambridge University Press, Cambridge, 2003. 
  17. [17] G. Tourlakis and F. Kibedi, A modal extension of first order classical logic – Part I, Bulletin of the Section of Logic 32 (2003), no. 4, pp. 165–178. 
  18. [18] G. Tourlakis and F. Kibedi, A modal extension of first order classical logic – Part II, Bulletin of the Section of Logic 33 (2004), no. 1, pp. 1–10. 
  19. [19] V. A. Vardanyan, On the predicate logic of provability, “Cybernetics”, Academy of Sciences of the USSR (in Russian) (1985). 
  20. [20] R. E. Yavorsky, On arithmetical completeness of first-order logics, Advances in Modal Logic (F. Wolter H. Wansing M. de Rijke and M. Zakharyaschev, ed.), vol. 3, CSLI Publications, Stanford University, Stanford, USA, 2001, pp. 1–16. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.