The mean value theorem in second order arithmetic

2001 ◽  
Vol 66 (3) ◽  
pp. 1353-1358 ◽  
Author(s):  
Christopher S. Hardin ◽  
Daniel J. Velleman
Keyword(s):  
Mean Value ◽  
Second Order ◽  
Mean Value Theorem ◽  
Natural Numbers ◽  
Second Order Arithmetic ◽  
Elementary Analysis ◽  
Logical Connectives ◽  
The Mean ◽  
Order Arithmetic ◽  
Image Position

This paper is a contribution to the project of determining which set existence axioms are needed to prove various theorems of analysis. For more on this project and its history we refer the reader to [1] and [2].We work in a weak subsystem of second order arithmetic. The language of second order arithmetic includes the symbols 0, 1, =, <, +, ·, and ∈, together with number variables x, y, z, … (which are intended to stand for natural numbers), set variables X, Y, Z, … (which are intended to stand for sets of natural numbers), and the usual quantifiers (which can be applied to both kinds of variables) and logical connectives. We write ∀x < t φ and ∃x < t φ as abbreviations for ∀x(x < t → φ) and ∃x{x < t ∧ φ) respectively; these are called bounded quantifiers. A formula is said to be if it has no quantifiers applied to set variables, and all quantifiers applied to number variables are bounded. It is if it has the form ∃xθ and it is if it has the form ∀xθ, where in both cases θ is .The theory RCA0 has as axioms the usual Peano axioms, with the induction scheme restricted to formulas, and in addition the comprehension scheme, which consists of all formulas of the formwhere φ is , ψ is , and X does not occur free in φ(n). (“RCA” stands for “Recursive Comprehension Axiom.” The reason for the name is that the comprehension scheme is only strong enough to prove the existence of recursive sets.) It is known that this theory is strong enough to allow the development of many of the basic properties of the real numbers, but that certain theorems of elementary analysis are not provable in this theory. Most relevant for our purposes is the fact that it is impossible to prove in RCA0 that every continuous function on the closed interval [0, 1] attains maximum and minimum values (see [1]).Since the most common proof of the Mean Value Theorem makes use of this theorem, it might be thought that the Mean Value Theorem would also not be provable in RCA0. However, we show in this paper that the Mean Value Theorem can be proven in RCA0. All theorems stated in this paper are theorems of RCA0, and all of our reasoning will take place in RCA0.

The use of Kripke's schema as a reduction principle

1977 ◽  
Vol 42 (2) ◽  
pp. 238-240 ◽  
Author(s):  
D. van Dalen
Keyword(s):  
Second Order ◽  
Reduction Technique ◽  
Reduction Principle ◽  
Natural Numbers ◽  
Second Order Arithmetic ◽  
Intuitionistic Theory ◽  
Order Arithmetic ◽  
Definition Of ◽  
Image Position ◽  
Creative Subject

The comprehension principle of second order arithmetic asserts the existence of certain species (sets) corresponding to properties of natural numbers. In the intuitionistic theory of sequences of natural numbers there is an analoguous principle, implicit in Brouwer's writing and explicitly stated by Kripke, which asserts the existence of certain sequences corresponding to statements. The justification of this principle, Kripke's Schema, makes use of the concept of the so-called creative subject. For more information the reader is referred to Troelstra [5].Kripke's Schema readsThere is a weaker versionThe idea to reduce species to sequences via Kripke's schema occurred several years ago (cf. [2, p. 128], [5, p. 104]). In [1] the reduction technique was applied in the construction of a model for HAS.On second thought, however, I realized that there is a straightforward, simpler way to exploit Kripke's schema, avoiding models altogether. The idea to present this material separately was forced on the author by C. Smorynski.Consider a second order arithmetic with both species and sequence variables. By KS we have(for convenience we restrict ourselves in KS to 0-1-sequences). An application of AC-NF givesOf course ξ is not uniquely determined. This is the key to the reduction of full second order arithmetic, or HAS, to a theory of sequences.We now introduce a translation τ to eliminate species variables. It is no restriction to suppose that the formulae contain only the sequence variables ξ1, ξ3, ξ5, …Note that by virtue of the definition of τ the axiom of extensionality is automatically verified after translation. The translation τ eliminates the species variables and leaves formulae without species variables invariant.

Extension of Lifschitz' realizability to higher order arithmetic, and a solution to a problem of F. Richman

1991 ◽  
Vol 56 (3) ◽  
pp. 964-973 ◽  
Author(s):  
Jaap van Oosten
Keyword(s):  
Higher Order ◽  
Second Order ◽  
Church’S Thesis ◽  
Second Order Arithmetic ◽  
Church's Thesis ◽  
Order Arithmetic ◽  
Image Position

AbstractF. Richman raised the question of whether the following principle of second order arithmetic is valid in intuitionistic higher order arithmetic HAH:and if not, whether assuming Church's Thesis CT and Markov's Principle MP would help. Blass and Scedrov gave models of HAH in which this principle, which we call RP, is not valid, but their models do not satisfy either CT or MP.In this paper a realizability topos Lif is constructed in which CT and MP hold, but RP is false. (It is shown, however, that RP is derivable in HAH + CT + MP + ECT0, so RP holds in the effective topos.) Lif is a generalization of a realizability notion invented by V. Lifschitz. Furthermore, Lif is a subtopos of the effective topos.

scholarly journals HYPERCLASS FORCING IN MORSE-KELLEY CLASS THEORY

2017 ◽  
Vol 82 (2) ◽  
pp. 549-575 ◽  
Author(s):  
CAROLIN ANTOS ◽  
SY-DAVID FRIEDMAN
Keyword(s):  
Second Order ◽  
Inaccessible Cardinal ◽  
Second Order Arithmetic ◽  
Class Theory ◽  
Order Arithmetic ◽  
Image Position ◽  
Class Forcing

AbstractIn this article we introduce and study hyperclass-forcing (where the conditions of the forcing notion are themselves classes) in the context of an extension of Morse-Kelley class theory, called MK**. We define this forcing by using a symmetry between MK** models and models of ZFC− plus there exists a strongly inaccessible cardinal (called SetMK**). We develop a coding between β-models ${\cal M}$ of MK** and transitive models M+ of SetMK** which will allow us to go from ${\cal M}$ to M+ and vice versa. So instead of forcing with a hyperclass in MK** we can force over the corresponding SetMK** model with a class of conditions. For class-forcing to work in the context of ZFC− we show that the SetMK** model M+ can be forced to look like LK*[X], where κ* is the height of M+, κ strongly inaccessible in M+ and $X \subseteq \kappa$. Over such a model we can apply definable class forcing and we arrive at an extension of M+ from which we can go back to the corresponding β-model of MK**, which will in turn be an extension of the original ${\cal M}$. Our main result combines hyperclass forcing with coding methods of [3] and [4] to show that every β-model of MK** can be extended to a minimal such model of MK** with the same ordinals. A simpler version of the proof also provides a new and analogous minimality result for models of second-order arithmetic.

scholarly journals Curves with zero derivative in F-spaces

1981 ◽  
Vol 22 (1) ◽  
pp. 19-29 ◽  
Author(s):  
N. J. Kalton
Keyword(s):  
Characteristic Function ◽  
Mean Value ◽  
Mean Value Theorem ◽  
Continuous Linear ◽  
Linear Functionals ◽  
Continuous Map ◽  
Left And Right ◽  
The Mean ◽  
Image Position ◽  
Locally Convex

Let X be an F-space (complete metric linear space) and suppose g:[0, 1] → X is a continuous map. Suppose that g has zero derivative on [0, 1], i.e.for 0≤t≤1 (we take the left and right derivatives at the end points). Then, if X is locally convex or even if it merely possesses a separating family of continuous linear functionals, we can conclude that g is constant by using the Mean Value Theorem. If however X* = {0} then it may happen that g is not constant; for example, let X = Lp(0, 1) (0≤p≤1) and g(t) = l[0,t] (0≤t≤1) (the characteristic function of [0, t]). This example is due to Rolewicz [6], [7; p. 116].

STRONG REDUCTIONS BETWEEN COMBINATORIAL PRINCIPLES

2016 ◽  
Vol 81 (4) ◽  
pp. 1405-1431 ◽  
Author(s):  
DAMIR D. DZHAFAROV
Keyword(s):  
Reverse Mathematics ◽  
Second Order ◽  
New Techniques ◽  
Ramsey's Theorem ◽  
Second Order Arithmetic ◽  
Ramsey’S Theorem ◽  
Problems And Solutions ◽  
Combinatorial Principles ◽  
Order Arithmetic ◽  
Image Position

AbstractThis paper is a contribution to the growing investigation of strong reducibilities between ${\rm{\Pi }}_2^1$ statements of second-order arithmetic, viewed as an extension of the traditional analysis of reverse mathematics. We answer several questions of Hirschfeldt and Jockusch [13] about Weihrauch (uniform) and strong computable reductions between various combinatorial principles related to Ramsey’s theorem for pairs. Among other results, we establish that the principle $SRT_2^2$ is not Weihrauch or strongly computably reducible to $D_{ < \infty }^2$, and that COH is not Weihrauch reducible to $SRT_{ < \infty }^2$, or strongly computably reducible to $SRT_2^2$. The last result also extends a prior result of Dzhafarov [9]. We introduce a number of new techniques for controlling the combinatorial and computability-theoretic properties of the problems and solutions we construct in our arguments.

scholarly journals INTERPRETATIONS BETWEENω-LOGIC AND SECOND-ORDER ARITHMETIC

2014 ◽  
Vol 79 (3) ◽  
pp. 845-858
Author(s):  
RICHARD KAYE
Keyword(s):  
Model Theory ◽  
Second Order ◽  
Standard System ◽  
Technical Result ◽  
Second Order Arithmetic ◽  
Nonstandard Model ◽  
Order Arithmetic ◽  
Single Formula ◽  
Image Position

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

scholarly journals Multi-sorted version of second order arithmetic

2016 ◽  
Vol 13 (5) ◽  
Author(s):  
Farida Kachapova
Keyword(s):  
Reverse Mathematics ◽  
Peano Arithmetic ◽  
Second Order ◽  
Natural Numbers ◽  
Natural Form ◽  
Second Order Arithmetic ◽  
Arithmetical Truth ◽  
Order Arithmetic

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.

A simpler proof of Levinson's theorem

1985 ◽  
Vol 97 (3) ◽  
pp. 385-395 ◽  
Author(s):  
J. B. Conrey ◽  
A. Ghosh
Keyword(s):  
Functional Equation ◽  
Critical Line ◽  
Mean Value ◽  
Mean Value Theorem ◽  
Levinson’S Theorem ◽  
The Mean ◽  
Image Position

In this paper we present a proof of the mean-value theorem required by Levinson to show that at least one-third of the zeros of ζ(s) are on the critical line. As in Levinson [3], letwhere Χ(s)=ζ(s)/ζ(1−s) is the usual factor from the functional equation, and letwhereandwhere

scholarly journals RANDOMNESS NOTIONS AND REVERSE MATHEMATICS

2019 ◽  
Vol 85 (1) ◽  
pp. 271-299
Author(s):  
ANDRÉ NIES ◽  
PAUL SHAFER
Keyword(s):  
Reverse Mathematics ◽  
Second Order ◽  
Second Order Arithmetic ◽  
Existence Principle ◽  
Order Arithmetic ◽  
Image Position

AbstractWe investigate the strength of a randomness notion ${\cal R}$ as a set-existence principle in second-order arithmetic: for each Z there is an X that is ${\cal R}$-random relative to Z. We show that the equivalence between 2-randomness and being infinitely often C-incompressible is provable in $RC{A_0}$. We verify that $RC{A_0}$ proves the basic implications among randomness notions: 2-random $\Rightarrow$ weakly 2-random $\Rightarrow$ Martin-Löf random $\Rightarrow$ computably random $\Rightarrow$ Schnorr random. Also, over $RC{A_0}$ the existence of computable randoms is equivalent to the existence of Schnorr randoms. We show that the existence of balanced randoms is equivalent to the existence of Martin-Löf randoms, and we describe a sense in which this result is nearly optimal.

Sign in / Sign up

Export Citation Format

Share Document