Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Feferman Interpretability

Joost J. Joosten, Luka Mikec, Albert Visser

Abstract

We introduce a modal logic FIL for Feferman interpretability. In this logic both the provability modality and the interpretability modality can come with a label. This label indicates that in the arithmetical interpretation the axiom set of the underlying base theory is tweaked so as to mimic behaviour of finitely axiomatised theories. The theory with the tweaked axiom set will be extensionally the same as the original theory though this equality will in general not be provable. After providing the logic FIL and proving the arithmetical soundness, we set the logic to work to prove various interpretability principles to be sound in a large variety of (weak) arithmetical theories. In particular, we prove the two series of principles from [GJ20] to be arithmetically sound using FIL. Up to date, the arithmetical soundness of these series had only been proven using the techniques of definable cuts.

Feferman Interpretability

Abstract

We introduce a modal logic FIL for Feferman interpretability. In this logic both the provability modality and the interpretability modality can come with a label. This label indicates that in the arithmetical interpretation the axiom set of the underlying base theory is tweaked so as to mimic behaviour of finitely axiomatised theories. The theory with the tweaked axiom set will be extensionally the same as the original theory though this equality will in general not be provable. After providing the logic FIL and proving the arithmetical soundness, we set the logic to work to prove various interpretability principles to be sound in a large variety of (weak) arithmetical theories. In particular, we prove the two series of principles from [GJ20] to be arithmetically sound using FIL. Up to date, the arithmetical soundness of these series had only been proven using the techniques of definable cuts.

Paper Structure

This paper contains 23 sections, 22 theorems, 82 equations.

Table of Contents

  1. Arithmetic
  2. Interpretability
  3. Formalised provability and interpretability
  4. Modal interpretability logics
  5. Tweaking the axiom set
  6. The approximating theory defined
  7. A ${\sf {P}}\xspace$-like principle for the approximated theory
  8. Iterated approximations
  9. A modal logic for approximation
  10. The logic FIL
  11. Basic observations on FIL
  12. Arithmetical semantics
  13. A further modification of translations
  14. Arithmetical soundness
  15. On principles in $$ IL( All)
  16. ...and 8 more sections

Key Result

Theorem \oldthetheorem

We have the following.

Theorems & Definitions (50)

  • Definition \oldthetheorem: Buss1998
  • Definition \oldthetheorem: The polynomial induction schema Buss1998
  • Theorem \oldthetheorem: Buss:1986:BoundedArithmetic
  • Definition \oldthetheorem: $\Sigma_1$-collection
  • Theorem \oldthetheorem
  • Definition \oldthetheorem
  • Lemma \oldthetheorem
  • proof
  • Definition \oldthetheorem
  • Lemma \oldthetheorem
  • ...and 40 more