arXiv subjects

Fedor Pakhomov

Publications and source records attributed to Fedor Pakhomov.

34 records · Page 2Linked to original sources

arXiv2021

The $Π^1_2$ Consequences of a Theory

We develop the abstract framework for a proof-theoretic analysis of theories with scope beyond ordinal numbers, resulting in an analog of Ordinal Analysis aimed at the study of theorems of complexity $Π^1_2$. This is done by replacing the use of ordinal numbers by particularly uniform, wellfoundedness preserving functors in the category of linear orders. Generalizing the notion of a proof-theoretic ordinal, we define the functorial $Π^1_2$ norm of a theory and prove its existence and uniqueness for $Π^1_2$-sound theories. From this, we further abstract a definition of the $Σ^1_2$- and $Π^1_2$-soundness ordinals of a theory; these quantify, respectively, the maximum strength of true $Σ^1_2$ theorems and minimum strength of false $Π^1_2$ theorems of a given theory. We study these ordinals, developing a proof-theoretic classification theory for recursively enumerable extensions of $\mathsf{ACA}_0$ Using techniques from infinitary and categorical proof theory, generalized recursion theory, constructibility, and forcing, we prove that an admissible ordinal is the $Π^1_2$-soundness ordinal of some recursively enumerable extension of $\mathsf{ACA}_0$ if and only if it is not parameter-free $Σ^1_1$-reflecting. We show that the $Σ^1_2$-soundness ordinal of $\mathsf{ACA}_0$ is $ω_1^{ck}$ and characterize the $Σ^1_2$-soundness ordinals of recursively enumerable, $Σ^1_2$-sound extensions of $Π^1_1{-}\mathsf{CA}_0$.

math.LO↗

arXiv2021

Finitely Axiomatized Theories Lack Self-Comprehension

In this paper we prove that no consistent finitely axiomatized theory one-dimensionally interprets its own extension with predicative comprehension. This constitutes a result with the flavor of the Second Incompleteness Theorem whose formulation is completely arithmetic-free. Probably the most important novel feature that distinguishes our result from the previous results of this kind is that it is applicable to arbitrary weak theories, rather than to extensions of some base theory. The methods used in the proof of the main result yield a new perspective on the notion of sequential theory, in the setting of forcing-interpretations.

math.LO↗

arXiv2020

Multi-Dimensional Interpretations of Presburger Arithmetic in Itself

Presburger Arithmetic is the true theory of natural numbers with addition. We study interpretations of Presburger Arithmetic in itself. The main result of this paper is that all self-interpretations are definably isomorphic to the trivial one. Here we consider interpretations that might be multi-dimensional. We note that this resolves a conjecture by A. Visser. In order to prove the result we show that all linear orderings that are interpretable in $(\mathbb{N};+)$ are scattered orderings with the finite Hausdorff rank and that the ranks are bounded in the terms of the dimensions of the respective interpretations.

math.LO↗

arXiv2020

Short Proofs for Slow Consistency

Let $\operatorname{Con}(\mathbf T)\!\restriction\!x$ denote the finite consistency statement "there are no proofs of contradiction in $\mathbf T$ with $\leq x$ symbols". For a large class of natural theories $\mathbf T$, Pudlák has shown that the lengths of the shortest proofs of $\operatorname{Con}(\mathbf T)\!\restriction\!n$ in the theory $\mathbf T$ itself are bounded by a polynomial in $n$. At the same time he conjectures that $\mathbf T$ does not have polynomial proofs of the finite consistency statements $\operatorname{Con}(\mathbf T+\operatorname{Con}(\mathbf T))\!\restriction\!n$. In contrast we show that Peano arithmetic ($\mathbf{PA}$) has polynomial proofs of $\operatorname{Con}(\mathbf{PA}+\operatorname{Con}^*(\mathbf{PA}))\!\restriction\!n$, where $\operatorname{Con}^*(\mathbf{PA})$ is the slow consistency statement for Peano arithmetic, introduced by S.-D. Friedman, Rathjen and Weiermann. We also obtain a new proof of the result that the usual consistency statement $\operatorname{Con}(\mathbf{PA})$ is equivalent to $\varepsilon_0$ iterations of slow consistency. Our argument is proof-theoretic, while previous investigations of slow consistency relied on non-standard models of arithmetic.

math.LO↗

arXiv2019

Reflection ranks and ordinal analysis

It is well-known that natural axiomatic theories are well-ordered by consistency strength. However, it is possible to construct descending chains of artificial theories with respect to consistency strength. We provide an explanation of this well-orderness phenomenon by studying a coarsening of the consistency strength order, namely, the $Π^1_1$ reflection strength order. We prove that there are no descending sequences of $Π^1_1$ sound extensions of $\mathsf{ACA}_0$ in this order. Accordingly, we can attach a rank in this order, which we call reflection rank, to any $Π^1_1$ sound extension of $\mathsf{ACA}_0$. We prove that for any $Π^1_1$ sound theory $T$ extending $\mathsf{ACA}_0^+$, the reflection rank of $T$ equals the proof-theoretic ordinal of $T$. We also prove that the proof-theoretic ordinal of $α$ iterated $Π^1_1$ reflection is $\varepsilon_α$. Finally, we use our results to provide straightforward well-foundedness proofs of ordinal notation systems based on reflection principles.

math.LO↗

arXiv2019

A weak set theory that proves its own consistency

In the paper we introduce a weak set theory $\mathsf{H}_{<ω}$ . A formalization of arithmetic on finite von Neumann ordinals gives an embedding of arithmetical language into this theory. We show that $\mathsf{H}_{<ω}$ proves a natural arithmetization of its own Hilbert-style consistency. Unlike some previous examples of theories proving their own consistency, $\mathsf{H}_{<ω}$ appears to be sufficiently natural. The theory $\mathsf{H}_{<ω}$ is infinitely axiomatizable and proves existence of all individual hereditarily finite sets, but at the same time all its finite subtheories have finite models. Therefore, our example avoids the strong version of Gödel second incompleteness theorem (due to Pudlák) that asserts that no consistent a theory interpreting Robinson's arithmetic $\mathsf{Q}$ proves its own consistency. To show that $\mathsf{H}_{<ω}$ proves its own consistency we establish a conservation result connecting Kalmar elementary arithmetic $\mathsf{EA}$ and $\mathsf{H}_{<ω}$. We also consider the version of $\mathsf{H}_{<ω}$ over higher order logic denoted $\mathsf{H}^ω_{<ω}$. It has the same non-Gödelian property as $\mathsf{H}_{<ω}$ but happens to be more attractive from a technical point of view. In particular, we show that $\mathsf{H}^ω_{<ω}$ proves a $Π_1$ sentence $φ$ of the predicate-only version of arithmetical language iff $\mathsf{EA}$ proves that $φ$ holds on the superexponential cut.

math.LO↗

arXiv2018

Truth, Disjunction, and Induction

By a well-known result of Kotlarski, Krajewski, and Lachlan (1981), first-order Peano arithmetic $PA$ can be conservatively extended to the theory $CT^{-}[PA]$ of a truth predicate satisfying compositional axioms, i.e., axioms stating that the truth predicate is correct on atomic formulae and commutes with all the propositional connectives and quantifiers. This results motivates the general question of determining natural axioms concerning the truth predicate that can be added to $CT^{-}[PA]$ while maintaining conservativity over $PA$. Our main result shows that conservativity fails even for the extension of $CT^{-}[PA]$ obtained by the seemingly weak axiom of disjunctive correctness $DC$ that asserts that the truth predicate commutes with disjunctions of arbitrary finite size. In particular, $CT^{-}[PA] + DC$ implies $Con(PA)$. Our main result states that the theory $CT^{-}[PA] + DC$ coincides with the theory $CT_0[PA]$ obtained by adding $Δ_0$-induction in the language with the truth predicate. This result strengthens earlier work by Kotlarski (1986) and Cieśliński (2010). For our proof we develop a new general form of Visser's theorem on non-existence of infinite descending chains of truth definitions and prove it by reduction to (Löb's version of) Gödel's second incompleteness theorem, rather than by using the Visser-Yablo paradox, as in Visser's original proof (1989).

math.LO↗

arXiv2018

Complexity of the interpretability logic IL

We show that the decision problem for the basic system of interpretability logic IL is PSPACE-complete. For this purpose we present an algorithm which uses polynomial space with respect to the complexity of a given formula. The existence of such algorithm, together with the previously known PSPACE hardness of the closed fragment of IL, implies PSPACE-completeness.

math.LO↗

arXiv2018

Interpretations of Presburger Arithmetic in Itself

Presburger arithmetic PrA is the true theory of natural numbers with addition. We study interpretations of PrA in itself. We prove that all one-dimensional self-interpretations are definably isomorphic to the identity self-interpretation. In order to prove the results we show that all linear orders that are interpretable in (N,+) are scattered orders with the finite Hausdorff rank and that the ranks are bounded in terms of the dimension of the respective interpretations. From our result about self-interpretations of PrA it follows that PrA isn't one-dimensionally interpretable in any of its finite subtheories. We note that the latter was conjectured by A. Visser.

math.LO↗

arXiv2017

On a question of Krajewski's

In this paper we provide a (negative) solution to a problem posed by Stanisław Krajewski. Consider a recursively enumerable theory U and a finite expansion of the signature of U that contains at least one predicate symbol of arity $\ge$ 2. We show that, for any finite extension $α$ of U in the expanded language that is conservative over U, there is a conservative extension $β$ of U in the expanded language, such that $α\vdashβ$ and $β\nvdashα$. The result is preserved when we consider either extensions or model-conservative extensions of U in stead of conservative extensions. Moreover, the result is preserved when we replace $\vdash$ as ordering on the finitely axiomatized extensions in the expanded language by a special kind of interpretability, to wit interpretability that identically translates the symbols of the U-language. We show that the result fails when we consider an expansion with only unary predicate symbols for conservative extensions of U ordered by interpretability that preserves the symbols of U.

math.LO↗

arXiv2017

Solovay's completeness without fixed points

In this paper we present a new proof of Solovay's theorem on arithmetical completeness of Gödel-Löb provability logic GL. Originally, completeness of GL with respect to interpretation of $\Box$ as provability in PA was proved by R. 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 PA if it were unprovable in 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.

math.LO↗

arXiv2016

Slow and Ordinary Provability for Peano Arithmetic

The notion of slow provability for Peano Arithmetic ($\mathsf{PA}$) was introduced by S.D. Friedman, M. Rathjen, and A. Weiermann. They studied the slow consistency statement $\mathrm{Con}_{\mathsf{s}}$ that asserts that a contradiction is not slow provable in $\mathsf{PA}$. They showed that the logical strength of $\mathsf{PA}+\mathrm{Con}_{\mathsf{s}}$ lies strictly between that of $\mathsf{PA}$ and $\mathsf{PA}$ together with its ordinary consistency: $\mathsf{PA}\subsetneq \mathsf{PA}+\mathrm{Con}_{\mathsf{s}}\subsetneq \mathsf{PA}+\mathrm{Con}$. This paper is a further investigation into slow provability and its interplay with ordinary provability in $\mathsf{PA}$. We study three variants of slow provability. The associated consistency statement of each of these yields a theory that lies strictly between $\mathsf{PA}$ and $\mathsf{PA}+\mathrm{Con}$ in terms of logical strength. We investigate Turing-Feferman progressions based on these variants of slow provability. We show that for our three notions, the Turing-Feferman progression reaches $\mathsf{PA}+\mathrm{Con}$ in a different numbers of steps, namely $\varepsilon_0$, $ω$, and $2$. For each of the three slow provability predicates, we also determine its joint provability logic with ordinary $\mathsf{PA}$-provability.

math.LO↗

arXiv2015

Ordinal Notations in Caucal Hierarchy

Caucal hierarchy is a well-known class of graphs with decidable monadic theories. It were proved by L. Braud and A. Carayol that well-orderings in the hierarchy are the well-orderings with order types less than $\varepsilon_0$. Naturally, every well-ordering from the hierarchy could be considered as a constructive system of ordinal notations. In proof theory constructive systems of ordinal notations with fixed systems of cofinal sequences are used for the purposes of classification of provable recursive functions of theories. We show that any well-ordering from the hierarchy could be extended by a monadically definable system of cofinal sequences with Bachmann property. We show that the growth speed of functions from fast-growing hierarchy based on constructive ordinal notations from Caucal hierarchy may be only slightly influenced by the choice of monadically definable systems of cofinal sequences. We show that for ordinals less than $ω^ω$ a fast-growing hierarchy based on any system of ordinal notations from Caucal hierarchy coincides with Löb-Wainer hierarchy.

math.LO↗

arXiv2014

On Elementary Theories of GLP-Algebras

There is a polymodal provability logic $GLP$. We consider generalizations of this logic: the logics $GLP_α$, where $α$ ranges over linear ordered sets and play the role of the set of indexes of modalities. We consider the varieties of modal algebras that corresponds to the polymodal logics. We prove that the elementary theories of the free $\emptyset$-generated $GLP_{n}$ -algebras are decidable for all finite ordinals $n$.

math.LO↗

arXiv2013

On Elementary Theories of Ordinal Notation Systems based on Reflection Principles

We consider the constructive ordinal notation system for the ordinal ${ε_0}$ that were introduced by L.D. Beklemishev. There are fragments of this system that are ordinal notation systems for the smaller ordinals ${ω_n}$ (towers of $ω$-exponentiations of the height $n$). This systems are based on Japaridze's provability logic $\mathbf{GLP}$. They are closely related with the technique of ordinal analysis of $\mathbf{PA}$ and fragments of $\mathbf{PA}$ based on iterated reflection principles. We consider this notation system and it's fragments as structures with the signatures selected in a natural way. We prove that the full notation system and it's fragments, for ordinals ${\geω_4}$, have undecidable elementary theories. We also prove that the fragments of the full system, for ordinals ${\leω_3}$, have decidable elementary theories. We obtain some results about decidability of elementary theory, for the ordinal notation systems with weaker signatures.

math.LO↗

arXiv2013

On the complexity of the closed fragment of Japaridze's provability logic

We consider well-known provability logic GLP. We prove that the GLP-provability problem for variable-free polymodal formulas is PSPACE-complete. For a number n, let L^n_0 denote the class of all polymodal variable-free formulas without modalities , ,... . We show that, for every number n, the GLP-provability problem for formulas from L^n_0 is in PTIME.

math.LO↗