Based on the paper [4] we show that true second‐order arithmetic is interpretable over the real‐algebraic structure of models of intuitionistic analysis built upon a certain class of complete Heyting algebras.

We introduce a herbrandized functional interpretation of a first-order semi-intuitionistic extension of Heyting Arithmetic and study its main properties. We then extend the interpretation to a certain system of second-order arithmetic which includes a (classically false) formulation of the FAN principle and weak König's lemma. It is shown that any first-order formula provable in this system is classically true. It is perhaps worthy of note that, in our interpretation, second-order variables are (...) interpreted by finite sets of natural numbers. (shrink)

We obtain a nonasymptotic lower time bound for deciding sentences of bounded second-order arithmetic with respect to a form of the random access machine with stored programs. More precisely, let P be an arbitrary program for the model under consideration which recognized true formulas with a given range of parameters. Let p be the length of P and let N be an arbitrary natural number. We show how to construct a formula G with one free variable (...) with length not more than 400 symbols and a value f of x such that the time required by P to decide the truth of G is at least N+1 steps. Furthermore, the G constructed does not depend on P and the length of f is less than p+400. (shrink)

It is often remarked that first-order Peano Arithmetic is non-categorical but deductively well-behaved, while second-order Peano Arithmetic is categorical but deductively ill-behaved. This suggests that, when it comes to axiomatizations of mathematical theories, expressive power and deductive power may be orthogonal, mutually exclusive desiderata. In this paper, I turn to Hintikka’s :69–90, 1989) distinction between descriptive and deductive approaches in the foundations of mathematics to discuss the implications of this observation for the first-order logic (...) versus second-order logic divide. The descriptive approach is illustrated by Dedekind’s ‘discovery’ of the need for second-order concepts to ensure categoricity in his axiomatization of arithmetic; the deductive approach is illustrated by Frege’s Begriffsschrift project. I argue that, rather than suggesting that any use of logic in the foundations of mathematics is doomed to failure given the impossibility of combining the descriptive approach with the deductive approach, what this apparent predicament in fact indicates is that the first-order versus second-order divide may be too crude to investigate what an adequate axiomatization of arithmetic should look like. I also conclude that, insofar as there are different, equally legitimate projects one may engage in when working on the foundations of mathematics, there is no such thing as the One True Logic for this purpose; different logical systems may be adequate for different projects. (shrink)

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 $$\Pi _2$$ -property formalized in an appropriate language for second (...) order number theory is forcible from some $$T\supseteq \mathsf {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_{\omega _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 $$\Delta _0$$ -properties and for all universally Baire sets of reals. We will extend these results also to the theory of $$H_{\aleph _2}$$ in a follow up of this paper. (shrink)

In this paper, we introduce systems of nonstandard second-order arithmetic which are conservative extensions of systems of second-order arithmetic. Within these systems, we do reverse mathematics for nonstandard analysis, and we can import techniques of nonstandard analysis into analysis in weak systems of second-order arithmetic. Then, we apply nonstandard techniques to a version of Riemannʼs mapping theorem, and show several different versions of Riemannʼs mapping theorem.

This paper examines the ontological commitments of the second-order language of arithmetic and argues that they do not extend beyond the first-order language. Then, building on an argument by George Boolos, we develop a Tarski-style definition of a truth predicate for the second-order language of arithmetic that does not involve the assignment of sets to second-order variables but rather uses the same class of assignments standardly used in a definition for the (...) first-order language. (shrink)

We prove that the first-order theory of the Medvedev degrees, the first-order theory of the Muchnik degrees, and the third-order theory of true arithmetic are pairwise recursively isomorphic (obtained independently by Lewis, Nies, and Sorbi [7]). We then restrict our attention to the degrees of closed sets and prove that the following theories are pairwise recursively isomorphic: the first-order theory of the closed Medvedev degrees, the first-order theory of the compact Medvedev degrees, the (...) first-order theory of the closed Muchnik degrees, the first-order theory of the compact Muchnik degrees, and the second-order theory of true arithmetic. Our coding methods also prove that neither the closed Medvedev degrees nor the compact Medvedev degrees are elementarily equivalent to either the closed Muchnik degrees or the compact Muchnik degrees. (shrink)

Constructive ZF + full separation is shown to be equiconsistent with Second Order Arithmetic.

We show that there is a [Formula: see text]-model of second-order arithmetic in which the choice scheme holds, but the dependent choice scheme fails for a [Formula: see text]-assertion, confirming a conjecture of Stephen Simpson. We obtain as a corollary that the Reflection Principle, stating that every formula reflects to a transitive set, can fail in models of [Formula: see text]. This work is a rediscovery by the first two authors of a result obtained by the third (...) author in [V. G. Kanovei, On descriptive forms of the countable axiom of choice, Investigations on nonclassical logics and set theory, Work Collect., Moscow, 3-136 ]. (shrink)

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). (shrink)

In this paper, we discuss uniform versions of some axioms of second order arithmetic in the context of higher order arithmetic. We prove that uniform versions of weak weak König's lemma WWKL and Σ01 separation are equivalent to over a suitable base theory of higher order arithmetic, where is the assertion that there exists Φ2 such that Φf1 = 0 if and only if ∃x0 for all f. We also prove that uniform versions (...) of some well-known theorems are equivalent to or the axiom of the existence of the Suslin operator. (shrink)

This paper describes axiomatic theories SA and SAR, which are versions of second order arithmetic with countably many sorts for sets of natural numbers. The theories are intended to be applied in reverse mathematics because their multi-sorted language allows to express some mathematical statements in more natural form than in the standard second order arithmetic. We study metamathematical properties of the theories SA, SAR and their fragments. We show that SA is mutually interpretable with (...) the theory of arithmetical truth PATr obtained from the Peano arithmetic by adding infinitely many truth predicates. Corresponding fragments of SA and PATr are also mutually interpretable. We compare the proof-theoretical strengths of the fragments; in particular, we show that each fragment SAs with sorts <=s is weaker than next fragment SAs+1. (shrink)

We introduce a notion of syntactical truth predicate (s.t.p.) for the second order arithmetic PA 2 . An s.t.p. is a set T of closed formulas such that: (i) T(t = u) if and only if the closed first order terms t and u are convertible, i.e., have the same value in the standard interpretation (ii) T(A → B) if and only if (T(A) $\Longrightarrow$ T(B)) (iii) T(∀ x A) if and only if (T(A[x ← t]) (...) for any closed first order term t) (iv) T(∀ X A) if and only if (T(A[X ←▵]) for any closed set definition $\triangle = \{x \mid D(x)\}$ ). S.t.p.'s can be seen as a counterpart to Tarski's notion of (model-theoretical) validity and have main model properties. In particular, their existence is equivalent to the existence of an ω-model of PA 2 , this fact being provable in PA 2 with arithmetical comprehension only. (shrink)

This research is motivated by the program of Reverse Mathematics. We investigate basic part of complex analysis within some weak subsystems of second order arithmetic, in order to determine what kind of set existence axioms are needed to prove theorems of basic analysis. We are especially concerned with Cauchy’s integral theorem. We show that a weak version of Cauchy’s integral theorem is proved in RCAo. Using this, we can prove that holomorphic functions are analytic in RCAo. (...) On the other hand, we show that a full version of Cauchy’s integral theorem cannot be proved in RCAo but is equivalent to weak König’s lemma over RCAo. (shrink)

This paper presents a systematic study of the prehistory of the traditional subsystems of second-order arithmetic that feature prominently in the reverse mathematics program of Friedman and Simpson. We look in particular at: (i) the long arc from Poincar\'e to Feferman as concerns arithmetic definability and provability, (ii) the interplay between finitism and the formalization of analysis in the lecture notes and publications of Hilbert and Bernays, (iii) the uncertainty as to the constructive status of principles (...) equivalent to Weak K\"onig's Lemma, and (iv) the large-scale intellectual backdrop to arithmetical transfinite recursion in descriptive set theory and its effectivization by Borel, Lusin, Addison, and others. (shrink)

This paper addresses the structures and ), whereMis a nonstandard model of PA andωis the standard cut. It is known that ) is interpretable in. Our main technical result is that there is an reverse interpretation of in ) which is ‘local’ in the sense of Visser [11]. We also relate the model theory of to the study of transplendent models of PA [2].This yields a number of model theoretic results concerning theω-models and their standard systems SSy, including the following.•$\left (...) \prec \left$if and only if$M \prec K$and$\left} \right) \prec \left} \right)$.•$\left} \right) \prec \left} \right)$if and only if$\left \prec \left$for someω-saturatedM*.•$M{ \prec _{\rm{e}}}K$implies SSy = SSy, but cofinal extensions do not necessarily preserve standard system in this sense.• SSy=SSy if and only if ) satisfies the full comprehension scheme.• If SSy is uniformly defined by a single formula, then ) satisfies the full comprehension scheme; and there are modelsMfor which SSy is not uniformly defined in this sense. (shrink)

By RCA 0 , we denote a subsystem of second order arithmetic based on Δ0 1 comprehension and Δ0 1 induction. We show within this system that the real number system R satisfies all the theorems (possibly with non-standard length) of the theory of real closed fields under an appropriate truth definition. This enables us to develop linear algebra and polynomial ring theory over real and complex numbers, so that we particularly obtain Hilbert’s Nullstellensatz in RCA 0.

In this paper, we introduce the systems ns-ACA₀ and ns-WKL₀ of non-standard second-order arithmetic in which we can formalize non-standard arguments in ACA₀ and WKL₀, respectively. Then, we give direct transformations from non-standard proofs in ns-ACA₀ or ns-WKL₀ into proofs in ACA₀ or WKL₀.

Yu, X., Riesz representation theorem, Borel measures and subsystems of second-order arithmetic, Annals of Pure and Applied Logic 59 65-78. Formalized concept of finite Borel measures is developed in the language of second-order arithmetic. Formalization of the Riesz representation theorem is proved to be equivalent to arithmetical comprehension. Codes of Borel sets of complete separable metric spaces are defined and proved to be meaningful in the subsystem ATR0. Arithmetical transfinite recursion is enough to prove (...) the measurability of Borel sets for any finite Borel measure on a compact complete separable metric space. (shrink)

We show that certain model-theoretic forcing arguments involving subsystems of second-order arithmetic can be formalized in the base theory, thereby converting them to effective proof-theoretic arguments. We use this method to sharpen the conservation theorems of Harrington and Brown-Simpson, giving an effective proof that WKL+0 is conservative over RCA0 with no significant increase in the lengths of proofs.

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.

In this paper, we show within ${\mathsf{RCA}_0}$ that both the Jordan curve theorem and the Schönflies theorem are equivalent to weak König’s lemma. Within ${\mathsf {WKL}_0}$ , we prove the Jordan curve theorem using an argument of non-standard analysis based on the fact that every countable non-standard model of ${\mathsf {WKL}_0}$ has a proper initial part that is isomorphic to itself (Tanaka in Math Logic Q 43:396–400, 1997).

Working within weak subsystems of second-order arithmetic Z2 we consider two versions of the Baire Category theorem which are not equivalent over the base system RCA0. We show that one version (B.C.T.I) is provable in RCA0 while the second version (B.C.T.II) requires a stronger system. We introduce two new subsystems of Z2, which we call RCA+ 0 and WKL+ 0, and show that RCA+ 0 suffices to prove B.C.T.II. Some model theory of WKL+ 0 and its (...) importance in view of Hilbert's program is discussed, as well as applications of our results to functional analysis. (shrink)

In this paper we study the logical strength of the determinacy of infinite binary games in terms of second order arithmetic. We define new determinacy schemata inspired by the Wadge classes of Polish spaces and show the following equivalences over the system RCA0*, which consists of the axioms of discrete ordered semi‐rings with exponentiation, Δ10 comprehension and Π00 induction, and which is known as a weaker system than the popularbase theory RCA0: 1. Bisep(Δ10, Σ10)‐Det* ↔ WKL0, 2. (...) Bisep(Δ10, Σ20)‐Det* ↔ ATR0 + Σ11 induction, 3. Bisep(Σ10, Σ20)‐Det* ↔ Sep(Σ10, Σ20)‐Det* ↔ Π11‐CA0, 4. Bisep(Δ20, Σ20)‐Det* ↔ Π11‐TR0, where Det* stands for the determinacy of infinite games in the Cantor space (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim). (shrink)

The paper characterizes the second order arithmetic theorems of a set theory that features a recursively Mahlo universe; thereby complementing prior proof-theoretic investigations on this notion. It is shown that the property of being recursively Mahlo corresponds to a certain kind of β-model reflection in second order arithmetic. Further, this leads to a characterization of the reals recursively computable in the superjump functional.

Neo-Fregean logicists claim that Hume's Principle (HP) may be taken as an implicit definition of cardinal number, true simply by fiat. A longstanding problem for neo-Fregean logicism is that HP is not deductively conservative over pure axiomatic second-order logic. This seems to preclude HP from being true by fiat. In this paper, we study Richard Kimberly Heck's Two-sorted Frege Arithmetic (2FA), a variation on HP which has been thought to be deductively conservative over second- (...) class='Hi'>order logic. We show that it isn't. In fact, 2FA is not conservative over $n$-th order logic, for all $n \geq 2$. It follows that in the usual one-sorted setting, HP is not deductively Field-conservative over second- or higher-order logic. (shrink)

We develop fundamental aspects of the theory of metric, Hilbert, and Banach spaces in the context of subsystems of second-order arithmetic. In particular, we explore issues having to do with distances, closed subsets and subspaces, closures, bases, norms, and projections. We pay close attention to variations that arise when formalizing definitions and theorems, and study the relationships between them.

We consider fragments of uniform reflection for formulas in the analytic hierarchy over theories of second order arithmetic. The main result is that for any second order arithmetic theory $T_0$ extending $\mathsf {RCA}_0$ and axiomatizable by a $\Pi ^1_{k+2}$ sentence, and for any $n\geq k+1$, $$\begin{align*}T_0+ \mathrm{RFN}_{\varPi^1_{n+2}} \ = \ T_0 + \mathrm{TI}_{\varPi^1_n}, \end{align*}$$ $$\begin{align*}T_0+ \mathrm{RFN}_{\varSigma^1_{n+1}} \ = \ T_0+ \mathrm{TI}_{\varPi^1_n}^{-}, \end{align*}$$ where T is $T_0$ augmented with full induction, and $\mathrm {TI}_{\varPi ^1_n}^{-}$ denotes (...) the schema of transfinite induction up to $\varepsilon _0$ for $\varPi ^1_n$ formulas without set parameters. (shrink)

We study Lebesgue and Atsuji spaces within subsystems of second order arithmetic. The former spaces are those such that every open covering has a Lebesgue number, while the latter are those such that every continuous function defined on them is uniformly continuous. The main results we obtain are the following: the statement “every compact space is Lebesgue” is equivalent to $\hbox{\sf WKL}_0$ ; the statements “every perfect Lebesgue space is compact” and “every perfect Atsuji space is compact” (...) are equivalent to $\hbox{\sf ACA}_0$ ; the statement “every Lebesgue space is Atsuji” is provable in $\hbox{\sf RCA}_0$ ; the statement “every Atsuji space is Lebesgue” is provable in $\hbox{\sf ACA}_0$ . We also prove that the statement “the distance from a closed set is a continuous function” is equivalent to $\Pi^1_1\hbox{-\sf CA}_0$. (shrink)

Hindman's Theorem is a prototypical example of a combinatorial theorem with a proof that uses the topology of the ultrafilters. We show how the methods of this proof, including topological arguments about ultrafilters, can be translated into second order arithmetic.

We study the formalization within sybsystems of second-order arithmetic of theorems concerning periodic points in dynamical systems on the real line. We show that Sharkovsky's theorem is provable in WKL0. We show that, with an additional assumption, Sharkovsky's theorem is provable in RCA0. We show that the existence for all n of n-fold iterates of continuous mappings of the closed unit interval into itself is equivalent to the disjunction of Σ02 induction and weak König's lemma.

I show that any sentence of nth-order (pure or applied) arithmetic can be expressed with no loss of compositionality as a second-order sentence containing no arithmetical vocabulary, and use this result to prove a completeness theorem for applied arithmetic. More specifically, I set forth an enriched second-order language L, a sentence A of L (which is true on the intended interpretation of L), and a compositionally recursive transformation Tr defined on formulas of (...) L, and show that they have the following two properties: (a) in a universe with at least [HEBREW LETTER BET] $_{n-2}$ objects, any formula of nth-order (pure or applied) arithmetic can be expressed as a formula of L, and (b) for any sentence $\ulcorner \phi \urcorner$ of L, $\ulcorner \phi^{Tr} \urcorner$ is a second-order sentence containing no arithmetical vocabulary, and nth $\mathcal{A} \vdash \ulcorner \phi \longleftrightarrow \phi^{Tr} \urcorner$. (shrink)

We study the provability in subsystems of second-order arithmetic of two theorems of Harrington and Shelah [6] about Borel quasi-orderings of the reals. These theorems turn out to be provable in ATR0, thus giving further evidence to the observation that ATR0 is the minimal subsystem of second-order arithmetic in which significant portion of descriptive set theory can be developed. As in [6] considering the lightface versions of the theorems will be instrumental in their proof (...) and the main techniques employed will be the reflection principles and Gandy forcing. (shrink)

We show that the maximal linear extension theorem for well partial orders is equivalent over RCA0 to ATR0. Analogously, the maximal chain theorem for well partial orders is equivalent to ATR0 over RCA0.

We give a new elementary proof of the comparison theorem relating $\sum^1_{n + 1}-\mathrm{AC}\uparrow$ and $\Pi^1_n -\mathrm{CA}\uparrow$ ; the proof does not use Skolem theories. By the same method we prove: a) $\sum^1_{n + 1}-\mathrm{DC} \uparrow \equiv (\Pi^1_n -CA)_{ , for suitable classes of sentences; b) $\sum^1_{n+1}-DC \uparrow$ proves the consistency of (Π 1 n -CA) ω k, for finite k, and hence is stronger than $\sum^1_{n+1}-AC \uparrow$ . a) and b) answer a question of Feferman and Sieg.

A theory T is tight if different deductively closed extensions of T (in the same language) cannot be bi-interpretable. Many well-studied foundational theories are tight, including $\mathsf {PA}$ [39], $\mathsf {ZF}$, $\mathsf {Z}_2$, and $\mathsf {KM}$ [6]. In this article we extend Enayat’s investigations to subsystems of these latter two theories. We prove that restricting the Comprehension schema of $\mathsf {Z}_2$ and $\mathsf {KM}$ gives non-tight theories. Specifically, we show that $\mathsf {GB}$ and $\mathsf {ACA}_0$ each admit different bi-interpretable extensions, (...) and the same holds for their extensions by adding $\Sigma ^1_k$ -Comprehension, for $k \ge 1$. These results provide evidence that tightness characterizes $\mathsf {Z}_2$ and $\mathsf {KM}$ in a minimal way. (shrink)

A fragment with the same provably recursive functions as n iterated inductive definitions is obtained by restricting second order arithmetic in the following way. The underlying language allows only up to n + 1 nested second order quantifications and those are in such a way, that no second order variable occurs free in the scope of another second order quantifier. The amount of induction on arithmetical formulae only affects the arithmetical consequences (...) of these theories, whereas adding induction for arbitrary formulae increases the strength by one inductive definition. (shrink)