Feferman Interpretability

TL;DR

This paper introduces a modal logic FIL for Feferman interpretability, incorporating labeled modalities to model axiom set modifications in arithmetical theories, and proves its arithmetical soundness for various interpretability principles.

Contribution

It develops the logic FIL with labeled modalities for Feferman interpretability and establishes its arithmetical soundness, extending prior methods with a new logical framework.

Findings

Proves arithmetical soundness of interpretability principles using FIL

Models axiom set modifications via labeled modalities

Extends previous techniques beyond definable cuts

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.