Two series of formalized interpretability principles for weak systems of arithmetic

A new principle in the interpretability logic of all reasonable arithmetical theories

The interpretability logic of a mathematical theory describes the structural behavior of interpretations over that theory. Different theories have different logics. This paper from 2011 revolves around the question what logic describes the behavior that is present in all theories with a minimum amount of arithmetic; the intersection over all such theories so to say. We denote this target logic by ${\textbf{IL}}({\rm All})$. In this paper we present a new principle $\sf R$ in ${\textbf{IL}}({\rm All})$. We show that $\sf R$ does not follow from the logic ${\textbf{IL}}{\sf P_0W^*}$ that contain…

Mutual Interpretability of Weak Essentially Undecidable Theories

Kristiansen and Murwanashyaka recently proved that Robinson arithmetic Q is interpretable in an elementary theory of full binary trees, T. We prove that, conversely, T is interpretable in Q by producing a formal interpretation of T in an elementary concatenation theory, thereby also establishing mutual interpretability of T with several well-known weak essentially undecidable theories of numbers, strings and sets. We also in introduce a "hybrid" elementary theory of strings and trees and establish its mutual interpretability with Robinson's weak arithmetic R, the weak theory of binary trees WT…

Provability and interpretability logics with restricted realizations

The provability logic of a theory T is the set of modal formulas, which under any arithmetical realization are provable in T . We slightly modify this notion by requiring the arithmetical realizations to come from a specified set $Γ$. We make an analogous modification for interpretability logics. This is a paper from 2012. We first studied provability logics with restricted realizations, and show that for various natural candidates of theory T and restriction set $Γ$, where each sentence in $Γ$ has a well understood (meta)-mathematical content in T, the result is the logic of linear frames. Ho…

Interpretability in PRA

In this paper from 2009 we study IL(PRA), the interpretability logic of PRA. As PRA is neither an essentially reflexive theory nor finitely axiomatizable, the two known arithmetical completeness results do not apply to PRA: IL(PRA) is not ILM or ILP. IL(PRA) does of course contain all the principles known to be part of IL(All), the interpretability logic of the principles common to all reasonable arithmetical theories. In this paper, we take two arithmetical properties of PRA and see what their consequences in the modal logic IL(PRA) are. These properties are reflected in the so-called Beklemi…

Proof Schemata for Theories equivalent to $PA$: on the Benefit of Conservative Reflection Principles

Induction is typically formalized as a rule or axiom extension of the LK-calculus. While this extension of the sequent calculus is simple and elegant, proof transformation and analysis can be quite difficult. Theories with an induction rule, for example Peano arithmetic do not have a {\em Herbrand} theorem. In this work we extend an existing meta-theoretic formalism, so called proof schemata, a recursive formulation of induction particularly suited for proof analysis, to Peano arithmetic. This relationship provides a meaningful conservative reflection principle between \PA and an alternative p…

Arithmetic with Limited Exponentiation

We present and analyze a natural hierarchy of weak theories, develop analysis in them, and show that they are interpretable in bounded quantifier arithmetic $\text{I}Δ_0$ (and hence in Robinson arithmetic Q). The strongest theories include computation corresponding to k-fold exponential (fixed k) time, Weak König's Lemma, and an arbitrary but fixed number of higher level function types with extensionality, recursive comprehension, and quantifier-free axiom of choice. We also explain why interpretability in $\text{I}Δ_0$ is so rich, and how to get below it.

Solovay's Relative Consistency Proof for FIM and BI

In 2002 Robert Solovay proved that a subsystem BI of classical second order arithmetic, with bar induction and arithmetical countable choice, can be negatively interpreted in the neutral subsystem BSK of Kleene's intuitionistic analysis FIM using Markov's Principle MP. Combining this result with Kleene's formalized recursive realizability, he established (in primitive recursive arithmetic PRA) that FIM + MP and BI have the same consistency strength. This historical note includes Solovay's original proof, with his permission, and the additional observation that Markov's Principle can be weakene…

Comparing Hume's Principle, Basic Law V and Peano Arithmetic

This paper presents new constructions of models of Hume's Principle and Basic Law V with restricted amounts of comprehension. The techniques used in these constructions are drawn from hyperarithmetic theory and the model theory of fields, and formalizing these techniques within various subsystems of second-order Peano arithmetic allows one to put upper and lower bounds on the interpretability strength of these theories and hence to compare these theories to the canonical subsystems of second-order arithmetic. The main results of this paper are: (i) there is a consistent extension of the hypera…

弱可解释性逻辑上的持续性原则

The persistence principle over weak interpretability logic

本文研究在弱可解释性逻辑中加入持续性原则所得逻辑，证明其弱不动点性质、切消与 Craig 插值、有限标架性质及算术语义下的可靠完全性。

Veltman语义的超滤扩展

Ultrafilter Extensions for Veltman Semantics

本文提出可解释性逻辑的一阶框架条件，证明其不可模态定义，但适用于ILM和ILP框架，并为此发展超滤扩展的代数工具。

可证性模型

Provability Models

本文提出名为可证性模型的经典模态逻辑新型克里普克式语义，证明了多类模态逻辑、解释性逻辑ILM对该类模型的可靠性与完全性，并将其改进为谓词可判定版本。

遗传有限多重集的弱本质不可判定理论

Weak essentially undecidable theories of hereditarily finite multisets

该研究引入遗传有限多重集的一阶理论WF⁻和F⁻，证明WF⁻与R、F⁻与Q相互可解释，F⁻本质不可判定。克服多重集恢复有序对障碍，展示顺序与多重性的关系，还证明公理独立性及应用于斯宾塞 - 布朗形式，定位本质不可判定边界。