Solovay’s Completeness Without Fixed Points
| Autor: | Fedor Pakhomov |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
Discrete mathematics
Interpretation (logic) Semantics (computer science) 010102 general mathematics Provability logic 0102 computer and information sciences Fixed point 01 natural sciences TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Modal 010201 computation theory & mathematics Completeness (logic) Arithmetic function 0101 mathematics Mathematics |
| Zdroj: | Logic, Language, Information, and Computation ISBN: 9783662553855 WoLLIC |
| DOI: | 10.1007/978-3-662-55386-2_20 |
| Popis: | In this paper we present a new proof of Solovay’s theorem on arithmetical completeness of Godel-Lob provability logic \(\mathsf {GL}\). Originally, completeness of \(\mathsf {GL}\) with respect to interpretation of \(\Box \) as provability in \(\mathsf {PA}\) was proved by Solovay in 1976. The key part of Solovay’s proof was his construction of an arithmetical evaluation for a given modal formula that made the formula unprovable in \(\mathsf {PA}\) if it were unprovable in \(\mathsf {GL}\). The arithmetical sentences for the evaluations were constructed using certain arithmetical fixed points. The method developed by Solovay have been used for establishing similar semantics for many other logics. In our proof we develop new more explicit construction of required evaluations that doesn’t use any fixed points in their definitions. To our knowledge, it is the first alternative proof of the theorem that is essentially different from Solovay’s proof in this key part. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|