Hostname: page-component-586b7cd67f-2plfb Total loading time: 0 Render date: 2024-11-25T02:25:06.906Z Has data issue: false hasContentIssue false
  • English
  • Français

On modal systems having arithmetical interpretations

Published online by Cambridge University Press:  12 March 2014

Arnon Avron
Arnon Avron*
Affiliation:
Tel-Aviv University, Ramat-Aviv, Tel-Aviv, Israel
Get access Rights & Permissions [Opens in a new window]

Extract

We deal here with two modal logics, GL and Grz, that are known to have interesting arithmetical interpretations connected with the notion of provability. GL is the extensiom of K (or K4) by the schema □(□ A → A) → □ A, and Grz is the extension of S4 by □(□(A → □A) →A) → □A. GL is also known to be sound and complete with respect to the class of all Kripke models that are transitive, irreflexive and well founded. Grz bears the same relation to the corresponding reflexive models. We refer the reader to [1] for a full exposition of the subject. (See also [4], [2], [6].)

In §I we develop a sequential calculus for both GL and Grz and give a semantical proof that both systems admit cut-elimination. (Incidentally, this provides an easy proof of the semantical completeness of the two systems.) With respect to GL this yields a correction of an error in [2].

In §II we show that cut-elimination fails for QGL (the extension of GL to a language with quantifiers). We further show that, despite this failure, QGL still has some of GL's interesting properties (e.g., the disjunction property). We also show, using fixed-point techniques, that similar properties obtain if we take as semantics for QGL the arithmetical interpretation extended in the obvious way.

We want to thank Professor H. Gaifman for his help while working on the subject.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 49 , Issue 3 , September 1984 , pp. 935 - 942
Copyright
Copyright © Association for Symbolic Logic 1984

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

[1]Boolos, G., The unprovability of consistency, Cambridge University Press, Cambridge, 1979.Google Scholar
[2]Leviant, D., On the proof theory of the modal logic for arithmetic provability, this Journal, vol. 46 (1981), pp. 531–537.Google Scholar
[3]Smoryński, C., Fifty years of self-reference in arithmetic, Notre Dame Journal of Formal Logic, vol. 22 (1981), pp. 357–374.CrossRefGoogle Scholar
[4]Solovay, R., Provability interpretations of modal logics, Israel Journal of Mathematics, vol. 25 (1976), pp. 287–304.CrossRefGoogle Scholar
[5]Takeuti, G., Proof theory, North-Holland, Amsterdam, 1978.Google Scholar
[6]Sambin, G. and Valentini, S., A modal sequent calculus for a fragment of arithmetic, Studia Logica, vol. 39 (1980), pp. 245–256.CrossRefGoogle Scholar
[7]Boolos, G., Extremely undecidable sentences, this Journal, vol. 47 (1982), pp. 191–196.Google Scholar
[8]Artémov, S. N., Arithmetically complete modal theories, Sémiotika i Informatika, vyp. 14 (1980), pp. 115–133. (Russian)Google Scholar
[9]Montagna, F., On the diagonalizable algebra of Peano arithmetic, Unione Matematica Italiana: Bolletino B, ser. 5, vol. 16 (1979), pp. 795–812.Google Scholar
[10]Visser, A., On the provability logic of any recursive enumerable extension of Peano arithmetic or another look at Solovay proof (to appear).Google Scholar