Provability logics for natural Turing progressions of arithmetical theories (Q804564): Difference between revisions

From MaRDI portal
Added link to MaRDI item.
Set OpenAlex properties.
 
(4 intermediate revisions by 3 users not shown)
Property / author
 
Property / author: Lev D. Beklemishev / rank
Normal rank
 
Property / author
 
Property / author: Lev D. Beklemishev / rank
 
Normal rank
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank
Property / cites work
 
Property / cites work: Modal logics with several operators and probability interpretations / rank
 
Normal rank
Property / cites work
 
Property / cites work: Transfinite recursive progressions of axiomatic theories / rank
 
Normal rank
Property / cites work
 
Property / cites work: Wie die Beweistheorie zu ihren Ordinalzahlen kam und kommt / rank
 
Normal rank
Property / cites work
 
Property / cites work: Provability in finite subtheories of PA and relative interpretability: a modal investigation / rank
 
Normal rank
Property / cites work
 
Property / cites work: Quantified modal logic and self-reference / rank
 
Normal rank
Property / cites work
 
Property / cites work: Provability interpretations of modal logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Resolution of singularities in bordism / rank
 
Normal rank
Property / full work available at URL
 
Property / full work available at URL: https://doi.org/10.1007/bf00370390 / rank
 
Normal rank
Property / OpenAlex ID
 
Property / OpenAlex ID: W1984643361 / rank
 
Normal rank

Latest revision as of 09:49, 30 July 2024

scientific article
Language Label Description Also known as
English
Provability logics for natural Turing progressions of arithmetical theories
scientific article

    Statements

    Provability logics for natural Turing progressions of arithmetical theories (English)
    0 references
    1991
    0 references
    In this paper Beklemishev defines a normal modal logic that has for each \(\xi < \varepsilon_0\) a modality \([\xi]\). The intended arithmetical interpretation of each modality \([\xi]\) will be a formalization in \(\mathbf{PA}\) of ``provable in the \(\xi\)-th Turing progression of some base theory \(T\)''. The logic \(\mathbf{TL}\varepsilon_0\) is presented. This logic is proven to be sound in that it generates modal principles \(\phi\) that are provable in \(\mathbf{PA}\) under any arithmetical interpretation \(\phi^{\ast}\) of \(\phi\). The base theory is chosen to be \(\mathbf{PA}\) so that transfinite induction up to any ordinal \(\lambda < \varepsilon_0\) is available. Next, modal semantics for \(\mathbf{TL}\varepsilon_0\) and certain fragments is given and modal completeness results are provided. These modal models can be embedded into arithmetic using a Solovay function to prove that \(\mathbf{TL}\varepsilon_0\) is arithmetically complete. By taking all theorems of \(\mathbf{TL}\varepsilon_0\) as axioms and adding reflexion to the logic one obtains after closing under modus ponens the logic \(\mathbf{TL}^{+}_{\varepsilon_0}\) that generates exactly the modal principles \(\phi\) that are true in the standard model under any arithmetical interpretation \(\phi^{\ast}\) of \(\phi\). It is shown that both \(\mathbf{TL}\varepsilon_0\) and \(\mathbf{TL}^{+}_{\varepsilon_0}\) are decidable.
    0 references
    provability logic
    0 references
    recursively enumerable theories
    0 references
    arithmetical interpretation
    0 references
    modal operators for progressions of theories
    0 references
    arithmetical completeness
    0 references
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references