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]

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]

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]

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]

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]

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]

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]

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]

Every function over the natural numbers has an infinite subdomain on which the function is non-decreasing. Motivated by a question of Dzhafarov and Schweber, we study the reverse mathematics of variants of this statement. It turns out that this statement restricted to computably bounded functions is computationally weak and does not imply the existence of the halting set. On the other hand, we prove that it is not a consequence of Ramsey's theorem for pairs. This statement can therefore be seen as an arguably natural principle between the arithmetic comprehension axiom and stable Ramsey's theorem for pairs. [ABSTRACT FROM AUTHOR]

In this article we provide an intrinsic characterization of the famous Howard-Bachmann ordinal in terms of a natural well-partial-ordering by showing that this ordinal can be realized as a maximal order type of a class of generalized trees with respect to a homeomorphic embeddability relation. We use our calculations to draw some conclusions about some corresponding subsystems of second order arithmetic. All these subsystems deal with versions of light-face $$\varPi ^1_1$$ -comprehension. [ABSTRACT FROM AUTHOR]

For any sufficiently strong theory of arithmetic, the set of Diophantine equations provably unsolvable in the theory is algorithmically undecidable, as a consequence of the MRDP theorem. In contrast, we show decidability of Diophantine equations provably unsolvable in Robinson's arithmetic Q. The argument hinges on an analysis of a particular class of equations, hitherto unexplored in Diophantine literature. We also axiomatize the universal fragment of Q in the process. [ABSTRACT FROM AUTHOR]

We present two constructions of models of bounded arithmetic, both in the form of a generalization of the ultrapower construction, that yield nonelementary extensions but do not introduce new lengths. As an application we show, assuming the existence of a one-way permutation g hard against polynomial-size circuits, that $$\textit{strict}R^1_2(g)$$ is weaker than $$R^1_2(g)$$ . In particular, if such a permutation can be defined by a term in the language of $$R^1_2$$ , then $$\textit{strict}R^1_2$$ is weaker than $$R^1_2$$ . [ABSTRACT FROM AUTHOR]

A proof of normalization for a classical system of Peano Arithmetic formulated in natural deduction is given. The classical rule of the system is the rule for indirect proof restricted to atomic formulas. This rule does not, due to the restriction, interfere with the standard detour conversions. The convertible detours, numerical inductions and instances of indirect proof concluding falsity are reduced in a way that decreases a vector assigned to the derivation. By interpreting the expressions of the vectors as ordinals each derivation is assigned an ordinal less than ɛ. The vector assignment, which proves termination of the procedure, originates in a normalization proof for Gödel's T by Howard (Intuitionism and proof theory. North-Holland, Amsterdam, ). [ABSTRACT FROM AUTHOR]

The elementary arithmetic operations $${+,\cdot,\le}$$ on integers are well-known to be computable in the weak complexity class TC, and it is a basic question what properties of these operations can be proved using only TC-computable objects, i.e., in a theory of bounded arithmetic corresponding to TC. We will show that the theory VTC extended with an axiom postulating the totality of iterated multiplication (which is computable in TC) proves induction for quantifier-free formulas in the language $${\langle{+,\cdot,\le}\rangle}$$ ( IOpen), and more generally, minimization for $${\Sigma_{0}^{b}}$$ formulas in the language of Buss's S. [ABSTRACT FROM AUTHOR]

Elementary patterns of resemblance notate ordinals up to the ordinal of $${\Pi^1_1 - CA_0}$$ . We provide ordinal multiplication and exponentiation algorithms using these notations. [ABSTRACT FROM AUTHOR]

We describe a method of forcing against weak theories of arithmetic and its applications in propositional proof complexity. [ABSTRACT FROM AUTHOR]

We prove that Basic Arithmetic, BA, has the de Jongh property, i.e., for any propositional formula A( p,..., p) built up of atoms p,..., p, BPC $${\vdash}$$ A( p,..., p) if and only if for all arithmetical sentences B,..., B, BA $${\vdash}$$ A( B,..., B). The technique used in our proof can easily be applied to some known extensions of BA. [ABSTRACT FROM AUTHOR]