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.

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.

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.

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

A transfinite sequence of ω-models

1972 ◽  
Vol 37 (1) ◽  
pp. 96-102 ◽  
Author(s):  
Andrzej Mostowski
Keyword(s):  
Order Type ◽  
Second Order ◽  
Axiomatic System ◽  
Second Order Arithmetic ◽  
Order Arithmetic ◽  
Image Position ◽  
Natural Relation

Let A2 be the axiomatic system of second order arithmetic as described in [2]. One of the models of A2 is the “principal model” Mpr consisting of all integers and all sets of integers. Obviously there exist many denumerable ω-models elementarily equivalent to Mpr and we shall deal in this paper with some questions pertaining to this family which we denote by .In §1 we define a rather natural relation ε between two denumerable families of sets of integers. From the upward Skolem-Löwenheim theorem it follows easily that there exists a family ordered by ε in the type ω1, but it is not immediately obvious whether there exist a subfamily of not well-ordered by ε. In the present paper we construct such a family of type η. ω1 where η is the order type of rationals and indicate some applications to hyperdegrees.We adopt the terminology and notation of [2], with the only change that we adjoin to the language of A2 the constants ν0, ν1, … for the consecutive numerals 0, 1, 2, … and axioms which characterise them:Also we modify the axioms of A2 given in [2] by prefixing them by general quantifiers bounded either to S or to N.

The strength of admissibility without foundation

1984 ◽  
Vol 49 (3) ◽  
pp. 867-879 ◽  
Author(s):  
Gerhard Jäger
Keyword(s):  
Standard Model ◽  
Set Theory ◽  
Recursion Theory ◽  
Second Order ◽  
Constructive Mathematics ◽  
Theoretic Analysis ◽  
Second Order Arithmetic ◽  
Admissible Sets ◽  
Order Arithmetic ◽  
Image Position

The following is part of a series of papers on theories for (iterated) admissible sets (cf. [10], [11], [12], [14], [15]). Although these theories are weak subsystems of Zermelo-Fraenkel set theory, they allow one to formalize and prove a fair amount of definability theory and generalized recursion theory. Using this machinery it is in general not very hard to establish the connections between theories for admissible sets and (for example) systems of second order arithmetic. A proof-theoretic analysis of theories for admissible sets therefore provides quite a uniform and powerful framework for the proof-theoretic treatment of many systems of set theory, second order arithmetic and constructive mathematics (see [12] and [15]). The strongest result in this direction so far is the pair of proof-theoretic equivalenceswhere T0 is Feferman's system for explicit mathematics of [5] and [6], (-CA) + (BI) is the usual system of second order arithmetic with the axiom of -comprehension and bar induction and KPi is Kripke-Platek set theory with ∈-inductionfor arbitrary formulas and the additional axiom.The least standard model of KPi is L(i0) where i0 is the first recursively inaccessible ordinal.In this paper we are mainly interested in the theory KPi0 which results from KPi by severely restricting the principles of induction. Basically, complete induction on the natural numbersis allowed only for ∆0-formulas, and (IND∈) is omitted completely.

CONSERVATIVITY OF ULTRAFILTERS OVER SUBSYSTEMS OF SECOND ORDER ARITHMETIC

2018 ◽  
Vol 83 (2) ◽  
pp. 740-765
Author(s):  
ANTONIO MONTALBÁN ◽  
RICHARD A. SHORE
Keyword(s):  
Second Order ◽  
Second Order Arithmetic ◽  
Hindman’S Theorem ◽  
Basic Language ◽  
Order Arithmetic ◽  
Image Position ◽  
Conservative Extensions ◽  
Turing Reduction ◽  
Metamathematical Result

AbstractWe extend the usual language of second order arithmetic to one in which we can discuss an ultrafilter over of the sets of a given model. The semantics are based on fixing a subclass of the sets in a structure for the basic language that corresponds to the intended ultrafilter. In this language we state axioms that express the notion that the subclass is an ultrafilter and additional ones that say it is idempotent or Ramsey. The axioms for idempotent ultrafilters prove, for example, Hindman’s theorem and its generalizations such as the Galvin--Glazer theorem and iterated versions of these theorems (IHT and IGG). We prove that adding these axioms to IHT produce conservative extensions of ACA0+IHT,${\rm{ACA}}_{\rm{0}}^ +$, ATR0,${\rm{\Pi }}_2^1$-CA0, and${\rm{\Pi }}_2^1$-CA0for all sentences of second order arithmetic and for full Z2for the class of${\rm{\Pi }}_4^1$sentences. We also generalize and strengthen a metamathematical result of Wang (1984) to show, for example, that any${\rm{\Pi }}_2^1$theorem ∀X∃YΘ(X,Y) provable in ACA0or${\rm{ACA}}_{\rm{0}}^ +$there aree,k∈ ℕ such that ACA0or${\rm{ACA}}_{\rm{0}}^ +$proves that ∀X(Θ(X, Φe(J(k)(X))) where Φeis theeth Turing reduction andJ(k)is thekth iterate of the Turing or Arithmetic jump, respectively. (A similar result is derived for${\rm{\Pi }}_3^1$theorems of${\rm{\Pi }}_1^1$-CA0and the hyperjump.)

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.

Sign in / Sign up

Export Citation Format

Share Document