nach oben

Erschienen in:

2015 | OriginalPaper | Buchkapitel

Kripke Models Built from Models of Arithmetic

verfasst von : Paula Henk

Erschienen in: Logic, Language, and Computation

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We introduce three relations between models of Peano Arithmetic (\(\mathsf {PA}\)), each of which is characterized as an arithmetical accessibility relation. A relation \(\mathrel {R}\) is said to be an arithmetical accessibility relation if for any model \(\mathcal {M}\) of \(\mathsf {PA}\), \(\mathcal {M}\vDash \mathsf {Pr}_{\pi }(\varphi )\) iff \(\mathcal {M}'\vDash \varphi \) for all \(\mathcal {M}'\) with \(\mathcal {M}\mathrel {R}\mathcal {M}'\), where \(\mathsf {Pr}_{\pi }(x)\) is an intensionally correct provability predicate of \(\mathsf {PA}\). The existence of arithmetical accessibility relations yields a new perspective on the arithmetical completeness of \(\mathsf {GL}\). We show that any finite Kripke model for the provability logic \(\mathsf {GL}\) is bisimilar to some “arithmetical” Kripke model whose domain consists of models of \(\mathsf {PA}\) and whose accessibility relation is an arithmetical accessibility relation. This yields a new interpretation of the modal operators in the context of \(\mathsf {PA}\): an arithmetical assertion \(\varphi \) is consistent (possible, \(\Diamond \varphi \)) if it holds in some arithmetically accessible model, and provable (necessary, \(\Box \varphi \)) if it holds in all arithmetically accessible models.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Towards a Suppositional Inquisitive Semantics

Nächstes Kapitel Positive Formulas in Intuitionistic and Minimal Logic

Here, \(\mathsf {PA}\) can be replaced by any recursively enumerable \(\varSigma _1\)-sound theory containing Elementary Arithmetic (\(\mathsf {EA}\)).

Our proof of Solovay’s Theorem is not “new”– the construction of the bisimulation makes crucial use of the most important ingredients of the original proof. Solovay’s Theorem will thus remain among the important theorems in mathematical logic which have “essentially” only one proof (see [3]).

The details of the algorithm are worked out in [10].

By this, we mean that the definitions of these relations and operations in \(\mathsf {PA}\) mimic the corresponding “informal” recursive definitions, and that the relevant recursion equations are provable in \(\mathsf {PA}\). In contrast, for a formula to be extensionally correct, it is only required to have the right extension in the standard model, or in other words to behave as intended with respect to the codes of standard sentences and terms. The concept of extensional correctness is found in the literature under various names, for example binumerability [2, 7] or representability [1]. There exist formulas which are extensionally correct with respect to a property but fail to express this property in an intensionally correct way – see p. 68 of [2] for an example.

To see how such ambiguities can arise, suppose (in \(\mathcal {M}\)) that \(17\) is in the extension of \(\delta _{j}\), but also that \(17\) is the code of the constant \(0\). Suppose also that we use sequences to code syntactical objects; for example the code of the sentence \(\mathsf {Z}c\) (where \(c\) is a constant) is the number \(\langle \ulcorner \mathsf {Z}\urcorner , \ulcorner c\urcorner \rangle \) (where \(\langle m, n\rangle \) is the code of the pair \((m,n)\)). The number \(\langle \mathsf {Z}, 17 \rangle \) can then either be parsed as coding the sentence \(\mathsf {Z}0\) of the language \(\varSigma \), or the sentence \(\mathsf {Z}c_{17}\) of the language \(\varSigma \cup \{c_{m}\mid m\in \mathcal {M}^{j}\}\).

The free variables are assumed to be bound by universal quantifiers.

Due to the availability of coding, allowing one parameter is as strong as allowing an arbitrary finite number of parameters.

For example, for 5 we require that \(\mathcal {M}\vDash \forall \varphi \in \mathsf {sent}\,(\pi (\varphi )\rightarrow \mathsf {tr}(\varphi , y))[m]\).

Remember that elements of the internal model are assumed to function simultaneously as codes of their own names.

For example, it should hold in \(\mathcal {M}^{+}\) that if \(\varphi \) is a sentence of the language \(\varSigma _{\delta }\), then \(\mathsf {tr}(\varphi )\) if and only if \(\forall \mathsf {a}\in \mathsf {as_{\delta }}\; \mathsf {tr}(\varphi [\mathsf {a}])\).

This was first noted in [12], and more carefully articulated in [2].

Cooper, S.B.: Computability Theory. CRC Mathematics Series. Chapman & Hall, London (2004)MATH

Feferman, S.: Arithmetization of metamathematics in a general setting. Fundam. Math. 49, 35–92 (1960)MATHMathSciNet

Foundations of Mathematics mailing list. http://cs.nyu.edu/pipermail/fom/2009-August/013996.html

Hamkins, J.D.: A simple maximality principle. J. Symb. Log. 68, 527–550 (2003)CrossRefMATHMathSciNet

Hamkins, J.D., Löwe, B.: The modal logic of forcing. Trans. Am. Math. Soc. 360, 1793–1817 (2008)CrossRefMATH

Kaye, R.: Models of Peano Arithmetic. Oxford Logic Guides. Oxford University Press, New York (1991)MATH

Lindström, P.: Aspects of Incompleteness. Lecture Notes in Logic. ASL/A K Peters, Natick, Massachusetts (2002)

Smoryński, C.: Nonstandard models and related developments. In: Harrington, L.A., Morley, M.D., Scedrov, A. (eds.) Harvey Friedman’s Research on the Foundations of Mathematics. Studies in logic and the foundations of mathematics, pp. 179–229. North-Holland, Amsterdam/New York/Oxford (1985)CrossRef

Solovay, R.M.: Provability interpretations of modal logic. Israel J. Math. 25, 287–304 (1976)CrossRefMATHMathSciNet

10.

Visser, A.: An inside view of \(\mathtt{{EXP}}\). J. Symb. Log. 57, 131–165 (1992)CrossRefMATHMathSciNet

11.

Visser, A.: An overview of interpretability logic. Adv. Modal Log. 1, 307–359 (1998)MathSciNet

12.

Wang, H.: A arithmetical models for formal systems. Methodos 3, 217–232 (1951)MathSciNet

Titel: Kripke Models Built from Models of Arithmetic
verfasst von: Paula Henk
Verlag: Springer Berlin Heidelberg
Buch: Logic, Language, and Computation
Print ISBN: 978-3-662-46905-7

Electronic ISBN: 978-3-662-46906-4

Copyright-Jahr: 2015
DOI: https://doi.org/10.1007/978-3-662-46906-4_10

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner