Search

This is an introductory paper to a series of results linking generic absoluteness results for second and third order number theory to the model theoretic notion of model companionship. Specifically we develop here a general framework linking Woodin's generic absoluteness results for second order number theory and the theory of universally Baire sets to model companionship and show that (with the required care in details) a Π 2 -property formalized in an appropriate language for second order number theory is forcible from some T ⊇ ZFC + large cardinals if and only if it is consistent with the universal fragment of T if and only if it is realized in the model companion of T. In particular we show that the first order theory of H ω 1 is the model companion of the first order theory of the universe of sets assuming the existence of class many Woodin cardinals, and working in a signature with predicates for Δ 0 -properties and for all universally Baire sets of reals. We will extend these results also to the theory of H ℵ 2 in a follow up of this paper. [ABSTRACT FROM AUTHOR]

In this paper we consider some fragments of IOpen (Robinson arithmetic Q with induction for quantifier-free formulas) proposed by Harvey Friedman and answer some questions he asked about these theories. We prove that I (lit) is equivalent to IOpen and is not finitely axiomatizable over Q , establish some inclusion relations between I (=) , I (≠) , I (⩽) and I (⩽̸) . We also prove that the set of diophantine equations solvable in models of I (=) is (algorithmically) decidable. [ABSTRACT FROM AUTHOR]

Realizability notions in mathematical logic have a long history, which can be traced back to the work of Stephen Kleene in the 1940s, aimed at exploring the foundations of intuitionistic logic. Kleene's initial realizability laid the ground for more sophisticated notions such as Kreisel's modified realizability and various modern approaches. In this context, our work aligns with the lineage of realizability strategies that emphasize the accumulation, rather than the propagation of precise witnesses. In this paper, we introduce a new notion of realizability, namely herbrandized modified realizability. This novel form of (cumulative) realizability, presented within the framework of semi-intuitionistic logic is based on a recently developed star combinatory calculus, which enables the gathering of witnesses into nonempty finite sets. We also show that the previous analysis can be extended from logic to (Heyting) arithmetic. [ABSTRACT FROM AUTHOR]

Akama et al. [1] introduced a hierarchical classification of first-order formulas for a hierarchical prenex normal form theorem in semi-classical arithmetic. In this paper, we give a justification for the hierarchical classification in a general context of first-order theories. To this end, we first formalize the standard transformation procedure for prenex normalization. Then we show that the classes E k and U k introduced in [1] are exactly the classes induced by Σ k and Π k respectively via the transformation procedure in any first-order theory. [ABSTRACT FROM AUTHOR]

In Arai (An ordinal analysis of a single stable ordinal, submitted) it is shown that an ordinal sup N < ω ψ Ω 1 (ε Ω S + N + 1) is an upper bound for the proof-theoretic ordinal of a set theory KP ℓ r + (M ≺ Σ 1 V) . In this paper we show that a second order arithmetic Σ 2 1 - - CA + Π 1 1 - CA 0 proves the wellfoundedness up to ψ Ω 1 (ε Ω S + N + 1 ) for each N. It is easy to interpret Σ 2 1 - - CA + Π 1 1 - CA 0 in KP ℓ r + (M ≺ Σ 1 V) . [ABSTRACT FROM AUTHOR]

Second-order arithmetic and class theory are second-order theories of mathematical subjects of foundational importance, namely, arithmetic and set theory. Despite the similarity in appearance, there turned out to be significant mathematical dissimilarities between them. The present paper studies various principles in class theory, from such a comparative perspective between second-order arithmetic and class theory, and presents a few new dissimilarities between them. [ABSTRACT FROM AUTHOR]

In this paper, we consider, for a set A of natural numbers, the following notions of finiteness There are a natural number l and a bijection f between { x ∈ N : x < l } and A ; There is an upper bound for A ; There is l such that ∀ B ⊆ A (| B | < l) ; It is not the case that ∀ y (∃ x > y) (x ∈ A) ; It is not the case that ∀ l ∃ B ⊆ A (| B | = l) , and infiniteness There are not a natural number l and a bijection f between { x ∈ N : x < l } and A ; There is no upper bound for A ; There is no l such that ∀ B ⊆ A (| B | < l) ; ∀ y (∃ x > y) (x ∈ A) ; ∀ l ∃ B ⊆ A (| B | = l) . In this paper, we systematically compare them in the method of constructive reverse mathematics. We show that the equivalence among them can be characterized by various combinations of induction axioms and non-constructive principles, including the axiom of bounded comprehension. [ABSTRACT FROM AUTHOR]

Formalism in the philosophy of mathematics has taken a variety of forms and has been advocated for widely divergent reasons. In Sects. 1 and 2, I briefly introduce the major formalist doctrines of the late nineteenth and early twentieth centuries. These are what I call empirico-semantic formalism (advocated by Heine), game formalism (advocated by Thomae) and instrumental formalism (advocated by Hilbert). After describing these views, I note some basic points of similarity and difference between them. In the remainder of the paper, I turn my attention to Hilbert's instrumental formalism. My primary aim there will be to develop its formalist elements more fully. These are, in the main, (i) its rejection of the axiom-centric focus of traditional model-construction approaches to consistency problems, (ii) its departure from the traditional understanding of the basic nature of proof and (iii) its distinctively descriptive or observational orientation with regard to the consistency problem for arithmetic. More specifically, I will highlight what I see as the salient points of connection between Hilbert's formalist attitude and his finitist standard for the consistency proof for arithmetic. I will also note what I see as a significant tension between Hilbert's observational approach to the consistency problem for arithmetic and his expressed hope that his solution of that problem would dispense with certain epistemological concerns regarding arithmetic once and for all. [ABSTRACT FROM AUTHOR]

In this paper, we prove results concerning the existence of proper end extensions of arbitrary models of fragments of Peano arithmetic (PA). In particular, we give alternative proofs that concern (a) a result of Clote (Fundam Math 127(2):163–170, 1986); (Fundam Math 158(3):301–302, 1998), on the end extendability of arbitrary models of Σ n -induction, for n ≥ 2 , and (b) the fact that every model of Σ 1 -induction has a proper end extension satisfying Δ 0 -induction; although this fact was not explicitly stated before, it follows by earlier results of Enayat and Wong (Ann Pure Appl Log 168:1247–1252, 2017) and Wong (Proc Am Math Soc 144:4021–4024, 2016). [ABSTRACT FROM AUTHOR]

We systematically study the interrelations between all possible variations of Δ 1 0 variants of the law of excluded middle and related principles in the context of intuitionistic arithmetic and analysis. [ABSTRACT FROM AUTHOR]

Abstract. This paper proves that the division operation [a/m] is provably total in the system S[sup 0, sub 2] of bounded arithmetic if and only if m is of the form 2 [sup n] for some n. [ABSTRACT FROM AUTHOR]

A major theme in the study of degree structures of all types has been the question of the decidability or undecidability of their first order theories. This is a natural and fundamental question that is an important goal in the analysis of these structures. In this paper, we study decidability for theories of upper semilattices that arise from the theory of numberings. We use the following approach: given a level of complexity, say Σα0, we consider the upper semilattice RΣα0 of all Σα0-computable numberings of all Σα0-computable families of subsets of N. We prove that the theory of the semilattice of all computable numberings is computably isomorphic to first order arithmetic. We show that the theory of the semilattice of all numberings is computably isomorphic to second order arithmetic. We also obtain a lower bound for the 1-degree of the theory of the semilattice of all Σα0-computable numberings, where α≥2 is a computable successor ordinal. Furthermore, it is shown that for any of the theories T mentioned above, the Π5-fragment of T is hereditarily undecidable. Similar results are obtained for the structure of all computably enumerable equivalence relations on N, equipped with composition. [ABSTRACT FROM AUTHOR]

Solovay proved (Israel J Math 25(3-4):287-304, ) that the propositional provability logic of any ∑-sound recursively enumerable extension of PA is characterized by the propositional modal logic GL. By contrast, Montagna proved in (Notre Dame J Form Log 25(2):179-189, ) that predicate provability logics of Peano arithmetic and Bernays-Gödel set theory are different. Moreover, Artemov proved in (Doklady Akademii Nauk SSSR 290(6):1289-1292, ) that the predicate provability logic of a theory essentially depends on the choice of a binumeration of the theory which is used to construct the provability predicate. In this paper, we compare predicate provability logics of I∑'s. For a binumeration α( x) of a recursive theory T, let PL( T) be the predicate provability logic of T defined by α( x). We prove that for any natural numbers i, j such that 0 < i < j, there exists a ∑ binumeration α( x) of some recursive axiomatization of I∑ such that $${{\sf PL}_\alpha({\rm I \Sigma}_i) \nsupseteq \bigcap_{\beta(x)}{\sf PL}_\beta({\rm I \Sigma}_j)}$$ and $${{\sf PL}_\alpha({\rm I \Sigma}_i) \nsubseteq \bigcup_{\beta(x)}{\sf PL}_\beta({\rm I \Sigma}_j)}$$ , where β( x) ranges over all ∑ binumerations of recursive axiomatizations of I∑. [ABSTRACT FROM AUTHOR]

The topological arithmetical hierarchy is the effective version of the Borel hierarchy. Its class Δta 2 is just large enough to include several types of pointsets in Euclidean spaces ℝ k which are fundamental in computable analysis. As a crossbreed of Hausdorff's difference hierarchy in the Borel class ΔB of the arithmetical hierarchy, the Hausdorff-Ershov hierarchy introduced in this paper gives a powerful classification within Δ2 and Ershov's hierarchy in the class Δ0 2 of the arithmetical hierarchy, the Hausdorff-Ershov hierarchy introduced in this paper gives a powerful classification within Δta 2. This is based on suitable characterizations of the sets from Δta 2 which are obtained in a close analogy to those of the ΔB 2 sets as well as those of the Δ0 2 sets. A helpful tool in dealing with resolvable sets is contributed by the technique of depth analysis. On this basis, the hierarchy properties, in particular the strict inclusions between classes of different levels, can be shown by direct constructions of witness sets. The Hausdorff-Ershov hierarchy runs properly over all constructive ordinals, in contrast to Ershov's hierarchy whose denotation-independent version collapses at level ω 2. Also, some new characterizations of concepts of decidability for pointsets in Euclidean spaces are presented. [ABSTRACT FROM AUTHOR]

This paper is a sequel to my [7]. It focuses on the notion of natural number as introduced in section 1 I of that paper with regard to forms of induction and recursive definitions. One point is that this notion of natural number is somewhat weaker than the classical one in so far as it is defined in terms of a weak implication. The other point is the lack of even a weak form of extensionality. As a main result of the present paper it will turn out that the means provided in [7] are sufficient to account for an interpretation of primitive recursive arithmetic. [ABSTRACT FROM AUTHOR]

The paper establishes lower bounds on the provability of D = NP and the MRDP theorem in weak fragments of arithmetic. The theory I[sup 5] E[sub l] is shown to be unable to prove D = NP. This non-provability result is used to show that I[sup 5] E[sub 1] cannot prove the MRDP theorem. On the other hand it is shown that I¹ E[sub1] proves D contains all predicates of the form (∀i ≤ |b|) P(i, x) ο Q(i, x) where ο is =, <, or ≤, and I[sup 0] E[sub1] proves D contains all predicates of the form (∀i ≤ b) P(i, x) = Q(i, x). Here P and Q are polynomials. A conjecture is made that D contains NLOGTIME. However, it is shown that this conjecture would not be sufficient to imply D = NP. Weak reductions to equality are then considered as a way of showing D = NP. It is shown that the bit-wise less than predicate, ≤2, and quality are both co-NLOGTIME complete under FDLOGTIME reductions. This is used to show that if the FDLOGTIME functions are definable in D then D = NP. [ABSTRACT FROM AUTHOR]

This paper develops the philosophy and technology needed for adding a supremum operator to the interpretability logic $$\mathsf {ILM}$$ of Peano Arithmetic ( $$\mathsf {PA}$$ ). It is well-known that any theories extending $$\mathsf {PA}$$ have a supremum in the interpretability ordering. While provable in $$\mathsf {PA}$$ , this fact is not reflected in the theorems of the modal system $$\mathsf {ILM}$$ , due to limited expressive power. Our goal is to enrich the language of $$\mathsf {ILM}$$ by adding to it a new modality for the interpretability supremum. We explore different options for specifying the exact meaning of the new modality. Our final proposal involves a unary operator, the dual of which can be seen as a (nonstandard) provability predicate satisfying the axioms of the provability logic $$\mathsf {GL}$$ . [ABSTRACT FROM AUTHOR]

In earlier work we introduced two systems for nonstandard analysis, one based on classical and one based on intuitionistic logic; these systems were conservative extensions of first-order Peano and Heyting arithmetic, respectively. In this paper we study how adding the principle of countable saturation to these systems affects their proof-theoretic strength. We will show that adding countable saturation to our intuitionistic system does not increase its proof-theoretic strength, while adding it to the classical system increases the strength from first- to full second-order arithmetic. [ABSTRACT FROM AUTHOR]

Abstract. In this paper a new method, elimination of Skolem functions for monotone formulas, is developed which makes it possible to determine precisely the arithmetical strength of instances of various non-constructive function existence principles. This is achieved by reducing the use of such instances in a given proof to instances of certain arithmetical principles. Our framework are systems F[sup w] := G[sub n]A[sup w] +AC-qf + change, where (G[sub n]A[sup w])[sub n is an element of N] is a hierarchy of (weak) subsystems of arithmetic in all finite types (introduced in [14]), AC-qf is the schema of quantifier-flee choice in all types and A is a set of certain analytical principles which e.g. includes the binary Konig's lemma. We apply this method to show that the arithmetical closures of single instances of/JO-comprehension and -choice contribute to the growth of extractable bounds from proofs relative to F[sup w] only by a primitive recursive functional in the sense of Kleene. In subsequent papers these results are widely generalized and the method is used to determine the arithmetical content of single sequences of instances of the Bolzano-Weierstrag principle for bounded sequences in R[sup d], the Ascoli-lemma and others. [ABSTRACT FROM AUTHOR]

Abstract. In the first part of this paper we investigate the intuitionistic version iI SIGMA[sub 1] of I SIGMA[sub 1] (in the language of PRA), using Kleene's recursive realizability techniques. Our treatment closely parallels the usual one for HA and establishes a number of nice properties for iI SIGMA[sub 1], e.g. existence of primitive recursive choice functions (this is established by different means also in [D94]). We then sharpen an unpublished theorem of Visser's to the effect that quantifier alternation alone is much less powerful intuitionistically than classically: iI SIGMA[sub 1] together with induction over arbitrary prenex formulas is PI[sub 2]-conservative over iI PI[sub 2]. In the second part of the article we study the relation of iI SIGMA[sub 1] to iI PI[sub 1] (in the usual arithmetical language). The situation here is markedly different from the classical case in that iI PI[sub 1] and iI SIGMA[sub 1] are mutually incomparable, while iI SIGMA[sub 1] is significantly stronger than iI PI[sub 1] as far as provably recursive functions are concerned: All primitive recursive functions can be proved total in iI SIGMA[sub 1] whereas the provably recursive functions of iI PI[sub 1] are all majorized by polynomials over N. iI PI[sub 1] is unusual also in that it lacks closure under Markov's Rule MR[sub PR]. [ABSTRACT FROM AUTHOR]

In Cieśliński (J Philos Logic 39:325–337, 2010), Cieśliński asked whether compositional truth theory with the additional axiom that all propositional tautologies are true is conservative over Peano Arithmetic. We provide a partial answer to this question, showing that if we additionally assume that truth predicate agrees with arithmetical truth on quantifier-free sentences, the resulting theory is as strong as Δ 0 -induction for the compositional truth predicate, hence non-conservative. On the other hand, it can be shown with a routine argument that the principle of quantifier-free correctness is itself conservative. [ABSTRACT FROM AUTHOR]

This paper investigates the status of the fragments of Peano Arithmetic obtained by restricting induction, collection and least number axiom schemes to formulas which are $${\Delta_1}$$ provably in an arithmetic theory T. In particular, we determine the provably total computable functions of this kind of theories. As an application, we obtain a reduction of the problem whether $${I\Delta_0 + \neg \mathit{exp}}$$ implies $${B\Sigma_1}$$ to a purely recursion-theoretic question. [ABSTRACT FROM AUTHOR]

This paper gives a Gentzen-style proof of the consistency of Heyting arithmetic in an intuitionistic sequent calculus with explicit rules of weakening, contraction and cut. The reductions of the proof, which transform derivations of a contradiction into less complex derivations, are based on a method for direct cut-elimination without the use of multicut. This method treats contractions by tracing up from contracted cut formulas to the places in the derivation where each occurrence was first introduced. Thereby, Gentzen's heightline argument, which introduces additional cuts on contracted compound cut formulas, is avoided. To show termination of the reduction procedure an ordinal assignment based on techniques of Howard for Gödel's T is used. [ABSTRACT FROM AUTHOR]

In this paper we prove conservation theorems for theories of classical first-order arithmetic over their intuitionistic version. We also prove generalized conservation results for intuitionistic theories when certain weak forms of the principle of excluded middle are added to them. Members of two families of subsystems of Heyting arithmetic and Buss-Harnik’s theories of intuitionistic bounded arithmetic are the intuitionistic theories we consider. For the first group, we use a method described by Leivant based on the negative translation combined with a variant of Friedman’s translation. For the second group, we use Avigad’s forcing method. [ABSTRACT FROM AUTHOR]

Leo Harrington showed that the second-order theory of arithmetic WKL 0 is $${\Pi^1_1}$$ -conservative over the theory RCA 0. Harrington’s proof is model-theoretic, making use of a forcing argument. A purely proof-theoretic proof, avoiding forcing, has been eluding the efforts of researchers. In this short paper, we present a proof of Harrington’s result using a cut-elimination argument. [ABSTRACT FROM AUTHOR]

In this paper we naturally define when a theory has bounded quantifier elimination, or is bounded model complete. We give several equivalent conditions for a theory to have each of these properties. These results provide simple proofs for some known results in the model theory of the bounded arithmetic theories like CPV and PV1. We use the mentioned results to obtain some independence results in the context of intuitionistic bounded arithmetic. We show that, if the intuitionistic theory of polynomial induction on strict $$\Pi_2^{b}$$ formulas proves decidability of $$\Sigma_1^b$$ formulas, then P=NP. We also prove that, if the mentioned intuitionistic theory proves $${\rm LMIN}(\Sigma_{1}^{b})$$ , then P=NP. [ABSTRACT FROM AUTHOR]

We prove that PTC N( n) (the polynomial time closure of the nonstandard natural number n in the model N of S2.) cannot be a model of U12. This implies that there exists a first order sentence of bounded arithmetic which is provable in U12 but does not hold in PTC N( n). [ABSTRACT FROM AUTHOR]

In this paper, we first prove several general theorems about strongness, supercompactness, and indestructibility, along the way giving some new applications of Hamkins’ lottery preparation forcing to indestructibility. We then show that it is consistent, relative to the existence of cardinals κ<λ so that κ is λ supercompact and λ is inaccessible, for the least strongly compact cardinal κ to be the least strong cardinal and to have its strongness, but not its strong compactness, indestructible under κ-strategically closed forcing. [ABSTRACT FROM AUTHOR]

The ŁΠ and ŁΠ1/2 logics were introduced by Godo, Esteva and Montagna. These logics extend many other known propositional and predicate logics, including the three mainly investigated ones (Gödel, product and Lukasiewicz logic). The aim of this paper is to show some advances in this field. We will see further reduction of the axiomatic systems for both logics. Then we will see many other logics contained in the ŁΠ family of logics (namely logics induced by the continuous finitely constructed t-norms and Takeuti and Titani's fuzzy predicate logic). [ABSTRACT FROM AUTHOR]

Dynamic ordinal analysis is ordinal analysis for weak arithmetics like fragments of bounded arithmetic. In this paper we will define dynamic ordinals – they will be sets of number theoretic functions measuring the amount of sΠ[sup b] [sub 1] (X) order induction available in a theory. We will compare order induction to successor induction over weak theories. We will compute dynamic ordinals of the bounded arithmetic theories sΣ[sup b] [sub n] (X)-L[sup m] IND for m=n and m=n+1, n≥0. Different dynamic ordinals lead to separation. In this way we will obtain several separation results between these relativized theories. We will generalize our results to further languages extending the language of bounded arithmetic. [ABSTRACT FROM AUTHOR]

In the language { 0 , 1 , ∘ , ⪯ } , where 0 and 1 are constant symbols, ∘ is a binary function symbol and ⪯ is a binary relation symbol, we formulate two theories, WD and D , that are mutually interpretable with the theory of arithmetic R and Robinson arithmetic Q , respectively. The intended model of WD and D is the free semigroup generated by { 0 , 1 } under string concatenation extended with the prefix relation. The theories WD and D are purely universally axiomatised, in contrast to Q which has the Π 2 -axiom ∀ x [ x = 0 ∨ ∃ y [ x = S y ] ] . [ABSTRACT FROM AUTHOR]

We compute that the index set of PAC-learnable concept classes is m-complete $${\Sigma^{0}_{3}}$$ within the set of indices for all concept classes of a reasonable form. All concept classes considered are computable enumerations of computable $${\Pi^{0}_{1}}$$ classes, in a sense made precise here. This family of concept classes is sufficient to cover all standard examples, and also has the property that PAC learnability is equivalent to finite VC dimension. [ABSTRACT FROM AUTHOR]

We prove that all extensions of Heyting Arithmetic with a logic that has the finite frame property possess the de Jongh property. [ABSTRACT FROM AUTHOR]

We introduce the simpler and shorter proof of Hajek’s theorem that the mathematical induction on ω implies a contradiction in the set theory with the comprehension principle within Łukasiewicz predicate logic Ł $${\forall}$$ (Hajek Arch Math Logic 44(6):763–782, 2005) by extending the proof in (Yatabe Arch Math Logic, accepted) so as to be effective in any linearly ordered MV-algebra. [ABSTRACT FROM AUTHOR]

In this article we find some sufficient and some necessary $${\Sigma^1_1}$$ -conditions with oracles for a model to be resplendent or chronically resplendent. The main tool of our proofs is internal arguments, that is analogues of classical theorems and model-theoretic constructions conducted inside a model of first-order Peano Arithmetic: arithmetised back-and-forth constructions and versions of the arithmetised completeness theorem, namely constructions of recursively saturated and resplendent models from the point of view of a model of arithmetic. These internal arguments are used in conjunction with Pabion’s theorem that ensures that certain oracles are coded in a sufficiently saturated model of arithmetic. Examples of applications are provided for the theories of dense linear orders and of discrete linear orders. These results are then generalised to other ω-categorical theories and theories with a unique countable recursively saturated model. [ABSTRACT FROM AUTHOR]

We study the Lindenbaum algebra $${\fancyscript{A}}$$ ( WKL o, RCA o) of sentences in the language of second-order arithmetic that imply RCA o and are provable from WKL o. We explore the relationship between $${\Sigma^1_1}$$ sentences in $${\fancyscript{A}}$$ ( WKL o, RCA o) and $${\Pi^0_1}$$ classes of subsets of ω. By applying a result of Binns and Simpson ( Arch. Math. Logic 43(3), 399–414, 2004) about $${\Pi^0_1}$$ classes, we give a specific embedding of the free distributive lattice with countably many generators into $${\fancyscript{A}}$$ ( WKL o, RCA o). [ABSTRACT FROM AUTHOR]

We answer a question of Jockusch by constructing a hyperimmune-free minimal degree below a 1-generic one. To do this we introduce a new forcing notion called arithmetical Sacks forcing. Some other applications are presented. [ABSTRACT FROM AUTHOR]

Progressions of iterated reflection principles can be used as a tool for the ordinal analysis of formal systems. We discuss various notions of proof-theoretic ordinals and compare the information obtained by means of the reflection principles with the results obtained by the more usual proof-theoretic techniques. In some cases we obtain sharper results, e.g., we define proof-theoretic ordinals relevant to logical complexity Π[sup0][sub1] and, similarly, for any class Π[sup0][subn]. We provide a more general version of the fine structure relationships for iterated reflection principles (due to U. Schmerl [25]). This allows us, in a uniform manner, to analyze main fragments of arithmetic axiomatized by restricted forms of induction, including I∑[subn], I∑[subn], IΠ[subn] and their combinations. We also obtain new conservation results relating the hierarchies of uniform and local reflection principles. In particular, we show that (for a sufficiently broad class of theories T the uniform ∑[sub1]-reflection principle for T is ∑[sub2]-conservative over the corresponding local reflection principle. This bears some corollaries on the hierarchies of restricted induction schemata in arithmetic and provides a key tool for our generalization of Schmerl's theorem. [ABSTRACT FROM AUTHOR]

Abstract. We investigate the problem how to lift the non -- Universal quantifier SIGMA[sup b, sub 1] (alpha) -- conservativity of T[sup 2, sub 2] (alpha) over S[sup 2, sub 2] (alpha) to the expected non -- Universal quantifier SIGMA[sup b, sub i] (alpha) -- conservativity of T[sup i+1, sub 2](alpha) over S[sup i+1, sub 2] (alpha), for i > 1. We give a non-trivial refinement of the "lifting method" developed in [4, 8], and we prove a sufficient condition on a Universal quantifier SIGMA[sup b, sub 1] (f)-consequence of T[sub 2] (f) to yield the non-conservation result. Further we prove that Ramsey's theorem, a Universal quantifier SIGMA[sup b, sub 1](alpha) -- formula, is not provable in T[sup 1, sub 2] (alpha), and that Universal quantifier SIGMA[sup b, sub 1] (alpha)- conservativity of T[sup i +1, sub 2] (alpha) over T[sup i, sub 2] (alpha) implies Universal quantifier SIGMa[sup b, sub j](alpha) -- conservativity of the whole T[sub 2](alpha) over T[sup i, sub 2](alpha), for any j is greater than or equal to 2. [ABSTRACT FROM AUTHOR]

The present work determines the arithmetic complexity of the index sets of u.c.e. families which are learnable according to various criteria of algorithmic learning. Specifically, we prove that the index set of codes for families that are TxtFex b a -learnable is Σ 4 0 -complete and that the index set of TxtFex ∗ ∗ -learnable and the index set of TxtFext ∗ ∗ -learnable families are both Σ 5 0 -complete. [ABSTRACT FROM AUTHOR]

This paper contains a corrected proof that the statement “every non-empty closed subset of a compact complete separable metric space is separably closed” implies the arithmetical comprehension axiom of reverse mathematics. [ABSTRACT FROM AUTHOR]

Answering a question raised by Shavrukov and Visser (Notre Dame J Form Log 55(4):569–582, 2014), we show that the lattice of ∃ Σ 1 b -sentences (in the language of Buss' weak arithmetical system S 2 1 ) over any computable enumerable consistent extension T of S 2 1 is uniformly dense (in the sense of Definition 2). We also show that for every C ∈ { Φ n : n ≥ 3 } ∪ { Θ n : n ≥ 2 } (where Φ and Θ refer to the known hierarchies of arithmetical formulas introduced by Burr for intuitionistic arithmetic) the lattices of C -sentences over any c.e. consistent extension T of the intuitionistic version of Robinson Arithmetic R are uniformly dense. As an immediate consequence of the proof, all these lattices are also locally universal (in the sense of Definition 3). [ABSTRACT FROM AUTHOR]

Schur's Lemma says that the endomorphism ring of a simple left R-module is a division ring. It plays a fundamental role to prove classical ring structure theorems like the Jacobson Density Theorem and the Wedderburn–Artin Theorem. We first define the endomorphism ring of simple left R-modules by their Π 1 0 subsets and show that Schur's Lemma is provable in R C A 0 . A ring R is left primitive if there is a faithful simple left R-module and left semisimple if the left regular module R R is semisimple. The Jacobson Density Theorem and the Wedderburn-Artin Theorem characterize left primitive ring and left semisimple ring, respectively. We then study such theorems from the standpoint of reverse mathematics. [ABSTRACT FROM AUTHOR]

Tanaka (Ann Pure Appl Log 84:41–49, 1997) proved a powerful generalization of Friedman's self-embedding theorem that states that given a countable nonstandard model (M , A) of the subsystem WKL 0 of second order arithmetic, and any element m of M , there is a self-embedding j of (M , A) onto a proper initial segment of itself such that j fixes every predecessor of m. Here we extend Tanaka's work by establishing the following results for a countable nonstandard model (M , A) of WKL 0 and a proper cut I of M : Theorem A. The following conditions are equivalent: (a) I is closed under exponentiation. (b) There is a self-embeddingjof (M , A) onto a proper initial segment of itselfsuch thatIis the longest initial segment of fixed points ofj. Theorem B. The following conditions are equivalent: (a) I is a strong cut of M and I ≺ Σ 1 M. (b) There is a self-embeddingj of (M , A) onto a proper initial segment of itself such that I is the set of all fixed points ofj. [ABSTRACT FROM AUTHOR]

We show, assuming weak large cardinals, that in the context of games of length ω with moves coming from a proper class, clopen determinacy is strictly weaker than open determinacy. The proof amounts to an analysis of a certain level of L that exists under large cardinal assumptions weaker than an inaccessible. Our argument is sufficiently general to give a family of determinacy separation results applying in any setting where the universal class is sufficiently closed; e.g., in third, seventh, or (ω + 2) th order arithmetic. We also prove bounds on the strength of Borel determinacy for proper class games. These results answer questions of Gitman and Hamkins. [ABSTRACT FROM AUTHOR]

Working in subsystems of second order arithmetic, we formulate several representations for hypergraphs. We then prove the equivalence of various vertex coloring theorems to WKL 0 , ACA 0 , and Π 1 1 - CA 0 . [ABSTRACT FROM AUTHOR]

Let Γ be a class of formulas. We say that a theory T in classical logic has the Γ-disjunction property if for any Γ sentences φ and ψ, either T⊢φ or T⊢ψ whenever T⊢φ∨ψ. First, we characterize the Γ-disjunction property in terms of the notion of partial conservativity. Secondly, we prove a model theoretic characterization result for Σn-disjunction property. Thirdly, we investigate relationships between partial disjunction properties and several other properties of theories containing Peano arithmetic. Finally, we investigate unprovability of formalized partial disjunction properties. [ABSTRACT FROM AUTHOR]

Consistency with the formal Church’s thesis, for short CT, and the axiom of choice, for short AC, was one of the requirements asked to be satisfied by the intensional level of a two-level foundation for constructive mathematics as proposed by Maietti and Sambin (in Crosilla, Schuster (eds) From sets and types to topology and analysis: practicable foundations for constructive mathematics, Oxford University Press, Oxford, 2005). Here we show that this is the case for the intensional level of the two-level Minimalist Foundation, for short MF, completed in 2009 by the second author. The intensional level of MF consists of an intensional type theory à la Martin-Löf, called mTT. The consistency of mTT with CT and AC is obtained by showing the consistency with the formal Church’s thesis of a fragment of intensional Martin-Löf’s type theory, called MLtt1, where mTT can be easily interpreted. Then to show the consistency of MLtt1 with CT we interpret it within Feferman’s predicative theory of non-iterative fixpoints ID1^ by extending the well known Kleene’s realizability semantics of intuitionistic arithmetics so that CT is trivially validated. More in detail the fragment MLtt1 we interpret consists of first order intensional Martin-Löf’s type theory with one universe and with explicit substitution rules in place of usual equality rules preserving type constructors (hence without the so called ξ-rule which is not valid in our realizability semantics). A key difficulty encountered in our interpretation was to use the right interpretation of lambda abstraction in the applicative structure of natural numbers in order to model all the equality rules of MLtt1 correctly. In particular the universe of MLtt1 is modelled by means of ID1^-fixpoints following a technique due first to Aczel and used by Feferman and Beeson. [ABSTRACT FROM AUTHOR]

Generalizing Cooper’s method of quantifier elimination for Presburger arithmetic, we give a new proof that all parametric Presburger families {St:t∈N} [as defined by Woods (Electron J Comb 21:P21, 2014)] are definable by formulas with polynomially bounded quantifiers in an expanded language with predicates for divisibility by f(t) for every polynomial f∈Z[t]. In fact, this quantifier bounding method works more generally in expansions of Presburger arithmetic by multiplication by scalars {α(t):α∈R,t∈X} where R is any ring of functions from X into Z. [ABSTRACT FROM AUTHOR]

The ϵ-substitution method is a technique for giving consistency proofs for theories of arithmetic. We use this technique to give a proof of the consistency of the impredicative theory ID1 using a variant of the cut-elimination formalism introduced by Mints. [ABSTRACT FROM AUTHOR]