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 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.

We introduce the logics GLP Λ, a generalization of Japaridze’s polymodal provability logic GLP ω where Λ is any linearly ordered set representing a hierarchy of provability operators of increasing strength. We shall provide a reduction of these logics to GLP ω yielding among other things a finitary proof of the normal form theorem for the variable-free fragment of GLP Λ and the decidability of GLP Λ for recursive orderings Λ. Further, we give a restricted axiomatization of the variable-free fragment of GLP Λ.

For “natural enough” systems of ordinal notation we show that α times iterated local reflection schema over a sufficiently strong arithmetic T proves the same Π 1 0 -sentences as ω α times iterated consistency. A corollary is that the two hierarchies catch up modulo relative interpretability exactly at ε-numbers. We also derive the following more general “mixed” formulas estimating the consistency strength of iterated local reflection: for all ordinals α ⩾ 1 and all β, β ≡ Π 1 0 T ω α ·, α ≡ Π 1 0 T β + ω α. Here T α stands for α times iterated local reflection over T, T β stands for β times iterated consistency, and ≡ Π 1 0 denotes mutual Π 1 0 -conservativity. In an appendix to this paper we develop our notion of “natural enough” system of ordinal notation and show that such systems do exist for every recursive ordinal.