Lev Beklemishev

We provide a variant of an axiomatization of elementary geometry based on logical axioms in the spirit of Huzita–Justin axioms for the origami constructions. We isolate the fragments corresponding to natural classes of origami constructions such as Pythagorean, Euclidean, and full origami constructions. The set of origami constructible points for each of the classes of constructions provides the minimal model of the corresponding set of logical axioms. Our axiomatizations are based on Wu’s axioms for orthogonal geometry and some modifications of Huzita–Justin axioms. We work out bi-interpretations between these logical theories and theories of fields as described in Makowsky (2018). Using a theorem of Ziegler (1982) which implies that the first order theory of Vieta fields is undecidable, we conclude that the first order theory of our axiomatization of origami is also undecidable.

We study the arithmetical schema asserting that every eventually decreasing elementary recursive function has a limit. Some other related principles are also formulated. We establish their relationship with restricted parameter-free induction schemata. We also prove that the same principle, formulated as an inference rule, provides an axiomatization of the Σ2-consequences of IΣ1.Using these results we show that ILM is the logic of Π1-conservativity of any reasonable extension of parameter-free Π1-induction schema. This result, however, cannot be much improved: by adapting a theorem of D. Zambella and G. Mints we show that the logic of Π1-conservativity of primitive recursive arithmetic properly extends ILM.In the third part of the paper we give an ordinal classification of -consequences of the standard fragments of Peano arithmetic in terms of reflection principles. This is interesting in view of the general program of ordinal analysis of theories, which in the most standard cases classifies Π-classes of sentences.

We establish a natural translation from word rewriting systems to strictly positive polymodal logics. Thereby, the latter can be considered as a generalization of the former. As a corollary we obtain examples of undecidable finitely axiomatizable strictly positive normal modal logics. The translation has its counterpart on the level of proofs: we formulate a natural deep inference proof system for strictly positive logics generalizing derivations in word rewriting systems. We also make some observations and formulate open questions related to the theory of modal companions of superintuitionistic logics that was initiated by L.L. Maksimova and V.V. Rybakov.

We study the fragment of Peano arithmetic formalizing the induction principle for the class of decidable predicates, $I\Delta_1$. We show that $I\Delta_1$ is independent from the set of all true arithmetical $\Pi_2-sentences$. Moreover, we establish the connections between this theory and some classes of oracle computable functions with restrictions on the allowed number of queries. We also obtain some conservation and independence results for parameter free and inference rule forms of $\Delta_1-induction$. An open problem formulated by J. Paris is whether $I\Delta_1$ proves the corresponding least element principle for decidable predicates, $L\Delta_1$ (or, equivalently. the $\Sigma_1-collection$ principle $B\Sigma_1$ ). We reduce this question to a purely computation-theoretic one.

A well-known polymodal provability logic inlMMLBox due to Japaridze is complete w.r.t. the arithmetical semantics where modalities correspond to reflection principles of restricted logical complexity in arithmetic. This system plays an important role in some recent applications of provability algebras in proof theory. However, an obstacle in the study of inlMMLBox is that it is incomplete w.r.t. any class of Kripke frames. In this paper we provide a complete Kripke semantics for inlMMLBox. First, we isolate a certain subsystem inlMMLBox of inlMMLBox that is sound and complete w.r.t. a nice class of finite frames. Second, appropriate models for inlMMLBox are defined as the limits of chains of finite expansions of models for inlMMLBox. The techniques involves unions of n -elementary chains and inverse limits of Kripke models. All the results are obtained by purely modal-logical methods formalizable in elementary arithmetic.

By a result of Paris and Friedman, the collection axiom schema for $\Sigma_{n+1}$ formulas, $B\Sigma_{n+1}$, is $\Pi_{n+2}$ conservative over $I\Sigma_n$. We give a new proof-theoretic proof of this theorem, which is based on a reduction of $B\Sigma_n$ to a version of collection rule and a subsequent analysis of this rule via Herbrand's theorem. A generalization of this method allows us to improve known results on reflection principles for $B\Sigma_n$ and to answer some technical questions left open by Sieg [23] and Hájek [9]. We also give a new proof of independence of $B\Sigma_{n+1}$ over $I\Sigma_n$ by a direct recursion-theoretic argument and answer an open problem formulated by Gaifman and Dimitracopoulos [8]

We investigate the bimodal logics sound and complete under the interpretation of modal operators as the provability predicates in certain natural pairs of arithmetical theories. Carlson characterized the provability logic for essentially reflexive extensions of theories, i.e. for pairs similar to. Here we study pairs of theories such that the gap between and is not so wide. In view of some general results concerning the problem of classification of the bimodal provability logics we are particularly interested in such pairs that is axiomatized over by ∏1-sentences only, and, for each n 1, proves the n-times iterated consistency of. A complete axiomatization, along with the appropriate Kripke semantics and decision procedures, is found for the two principal cases: finitely axiomatizable extensions of this sort, like e.g. ), ), etc., and reflexive extensions, like ¦n 1\s}), etc. We show that the first logic, ICP, is the minimal and the second one, RP, is the maximal within the class of the provability logics for such pairs of theories. We also show that there are some provability logics lying strictly between these two. As an application of the results of this paper, in the last section the polymodal provability logics for natural recursive progressions of theories based on iteration of consistency are characterized. We construct a system of ordinal notation, which gives exactly one notation to each constructive ordinal, such that the logic corresponding to any progression along coincides with that along natural Kalmar elementary well-orderings.

We suggest an algebraic approach to proof-theoretic analysis based on the notion of graded provability algebra, that is, Lindenbaum boolean algebra of a theory enriched by additional operators which allow for the structure to capture proof-theoretic information. We use this method to analyze Peano arithmetic and show how an ordinal notation system up to 0 can be recovered from the corresponding algebra in a canonical way. This method also establishes links between proof-theoretic ordinal analysis and the work which has been done in the last two decades on provability logic and reflection principles. Because of its abstract algebraic nature, we hope that it will also be of interest for non-prooftheorists.