Making the hyperreal line both saturated and complete

1991 ◽  
Vol 56 (3) ◽  
pp. 1016-1025 ◽  
Author(s):  
H. Jerome Keisler ◽  
James H. Schmerl
Keyword(s):  
Set Theory ◽  
Nonempty Intersection ◽  
Finite Intersection ◽  
Second Order Arithmetic ◽  
Ordered Field ◽  
Finite Intersection Property ◽  
Regular Cardinals ◽  
Hyperreal Numbers ◽  
Order Arithmetic ◽  
Internal Sets

AbstractIn a nonstandard universe, the κ-saturation property states that any family of fewer than κ internal sets with the finite intersection property has a nonempty intersection. An ordered field F is said to have the λ-Bolzano-Weierstrass property iff F has cofinality λ and every bounded λ-sequence in F has a convergent λ-subsequence. We show that if κ < λ are uncountable regular cardinals and βα < λ whenever α < κ and β < λ then there is a κ-saturated nonstandard universe in which the hyperreal numbers have the λ-Bolzano-Weierstrass property. The result also applies to certain fragments of set theory and second order arithmetic.

Proof theory

2018 ◽  
Author(s):  
Wilfried Sieg
Keyword(s):  
Finite Type ◽  
Set Theory ◽  
Proof Theory ◽  
Second Order ◽  
Von Neumann ◽  
Second Order Arithmetic ◽  
First Order ◽  
David Hilbert ◽  
Heyting Arithmetic ◽  
Order Arithmetic

Proof theory is a branch of mathematical logic founded by David Hilbert around 1920 to pursue Hilbert’s programme. The problems addressed by the programme had already been formulated, in some sense, at the turn of the century, for example, in Hilbert’s famous address to the First International Congress of Mathematicians in Paris. They were closely connected to the set-theoretic foundations for analysis investigated by Cantor and Dedekind – in particular, to difficulties with the unrestricted notion of system or set; they were also related to the philosophical conflict with Kronecker on the very nature of mathematics. At that time, the central issue for Hilbert was the ‘consistency of sets’ in Cantor’s sense. Hilbert suggested that the existence of consistent sets, for example, the set of real numbers, could be secured by proving the consistency of a suitable, characterizing axiom system, but indicated only vaguely how to give such proofs model-theoretically. Four years later, Hilbert departed radically from these indications and proposed a novel way of attacking the consistency problem for theories. This approach required, first of all, a strict formalization of mathematics together with logic; then, the syntactic configurations of the joint formalism would be considered as mathematical objects; finally, mathematical arguments would be used to show that contradictory formulas cannot be derived by the logical rules. This two-pronged approach of developing substantial parts of mathematics in formal theories (set theory, second-order arithmetic, finite type theory and still others) and of proving their consistency (or the consistency of significant sub-theories) was sharpened in lectures beginning in 1917 and then pursued systematically in the 1920s by Hilbert and a group of collaborators including Paul Bernays, Wilhelm Ackermann and John von Neumann. In particular, the formalizability of analysis in a second-order theory was verified by Hilbert in those very early lectures. So it was possible to focus on the second prong, namely to establish the consistency of ‘arithmetic’ (second-order number theory and set theory) by elementary mathematical, ‘finitist’ means. This part of the task proved to be much more recalcitrant than expected, and only limited results were obtained. That the limitation was inevitable was explained in 1931 by Gödel’s theorems; indeed, they refuted the attempt to establish consistency on a finitist basis – as soon as it was realized that finitist considerations could be carried out in a small fragment of first-order arithmetic. This led to the formulation of a general reductive programme. Gentzen and Gödel made the first contributions to this programme by establishing the consistency of classical first-order arithmetic – Peano arithmetic (PA) – relative to intuitionistic arithmetic – Heyting arithmetic. In 1936 Gentzen proved the consistency of PA relative to a quantifier-free theory of arithmetic that included transfinite recursion up to the first epsilon number, ε0; in his 1941 Yale lectures, Gödel proved the consistency of the same theory relative to a theory of computable functionals of finite type. These two fundamental theorems turned out to be most important for subsequent proof-theoretic work. Currently it is known how to analyse, in Gentzen’s style, strong subsystems of second-order arithmetic and set theory. The first prong of proof-theoretic investigations, the actual formal development of parts of mathematics, has also been pursued – with a surprising result: the bulk of classical analysis can be developed in theories that are conservative over (fragments of) first-order arithmetic.

Forcing and reducibilities. III. Forcing in fragments of set theory

1983 ◽  
Vol 48 (4) ◽  
pp. 1013-1034
Author(s):  
Piergiorgio Odifreddi
Keyword(s):  
Set Theory ◽  
Recursion Theory ◽  
Second Order ◽  
Analytic Hierarchy ◽  
Second Order Arithmetic ◽  
First Order ◽  
Order Language ◽  
Order Arithmetic ◽  
Definition Of ◽  
Generic Set

We conclude here the treatment of forcing in recursion theory begun in Part I and continued in Part II of [31]. The numbering of sections is the continuation of the numbering of the first two parts. The bibliography is independent.In Part I our language was a first-order language: the only set we considered was the (set constant for the) generic set. In Part II a second-order language was introduced, and we had to interpret the second-order variables in some way. What we did was to consider the ramified analytic hierarchy, defined by induction as:A0 = {X ⊆ ω: X is arithmetic},Aα+1 = {X ⊆ ω: X is definable (in 2nd order arithmetic) over Aα},Aλ = ⋃α<λAα (λ limit),RA = ⋃αAα.We then used (a relativized version of) the fact that (Kleene [27]). The definition of RA is obviously modeled on the definition of the constructible hierarchy introduced by Gödel [14]. For this we no longer work in a language for second-order arithmetic, but in a language for (first-order) set theory with membership as the only nonlogical relation:L0 = ⊘,Lα+1 = {X: X is (first-order) definable over Lα},Lλ = ⋃α<λLα (λ limit),L = ⋃αLα.

On the strength of nonstandard analysis

1986 ◽  
Vol 51 (2) ◽  
pp. 377-386 ◽  
Author(s):  
C. Ward Henson ◽  
H. Jerome Keisler
Keyword(s):  
Set Theory ◽  
Nonstandard Analysis ◽  
Mathematical Practice ◽  
Second Order ◽  
Erroneous Conclusion ◽  
Second Order Arithmetic ◽  
Correct Statement ◽  
Classical Mathematics ◽  
Order Arithmetic ◽  
Almost All

It is often asserted in the literature that any theorem which can be proved using nonstandard analysis can also be proved without it. The purpose of this paper is to show that this assertion is wrong, and in fact there are theorems which can be proved with nonstandard analysis but cannot be proved without it. There is currently a great deal of confusion among mathematicians because the above assertion can be interpreted in two different ways. First, there is the following correct statement: any theorem which can be proved using nonstandard analysis can be proved in Zermelo-Fraenkel set theory with choice, ZFC, and thus is acceptable by contemporary standards as a theorem in mathematics. Second, there is the erroneous conclusion drawn by skeptics: any theorem which can be proved using nonstandard analysis can be proved without it, and thus there is no need for nonstandard analysis.The reason for this confusion is that the set of principles which are accepted by current mathematics, namely ZFC, is much stronger than the set of principles which are actually used in mathematical practice. It has been observed (see [F] and [S]) that almost all results in classical mathematics use methods available in second order arithmetic with appropriate comprehension and choice axiom schemes.

Compactification of groups and rings and nonstandard analysis

1970 ◽  
Vol 34 (4) ◽  
pp. 576-588 ◽  
Author(s):  
Abraham Robinson
Keyword(s):  
Topological Group ◽  
Finite Subset ◽  
Nonstandard Analysis ◽  
Nonempty Intersection ◽  
Intersection Property ◽  
Finite Intersection ◽  
Finite Intersection Property ◽  
Formal Properties

Let G be a separated (Hausdorff) topological group and let *G be an enlargement of G (see [8]). Thus, *G (i) possesses the same formal properties as G in the sense explained in [8], and (ii) every set of subsets {Aν} of G with the finite intersection property—i.e. such that every nonempty finite subset of {Aν} has a nonempty intersection—satisfies ∩*Aν ≠ ø, where the *Aν are the extensions of the Aν in *G, respectively.

A STRONG MULTI-TYPED INTUITIONISTIC THEORY OF FUNCTIONALS

2015 ◽  
Vol 80 (3) ◽  
pp. 1035-1065 ◽  
Author(s):  
FARIDA KACHAPOVA
Keyword(s):  
Set Theory ◽  
Classical Theory ◽  
Second Order ◽  
Point Of View ◽  
Second Order Arithmetic ◽  
Intuitionistic Theory ◽  
Classical Mathematics ◽  
Order Arithmetic ◽  
Comprehension Axiom

AbstractIn this paper we describe an intuitionistic theory SLP. It is a relatively strong theory containing intuitionistic principles for functionals of many types, in particular, the theory of the “creating subject”, axioms for lawless functionals and some versions of choice axioms. We construct a Beth model for the language of intuitionistic functionals of high types and use it to prove the consistency of SLP.We also prove that the intuitionistic theory SLP is equiconsistent with a classical theory TI. TI is a typed set theory, where the comprehension axiom for sets of type n is restricted to formulas with no parameters of types > n. We show that each fragment of SLP with types ≤ s is equiconsistent with the corresponding fragment of TI and that it is stronger than the previous fragment of SLP. Thus, both SLP and TI are much stronger than the second order arithmetic. By constructing the intuitionistic theory SLP and interpreting in it the classical set theoryTI, we contribute to the program of justifying classical mathematics from the intuitionistic point of view.

Definitions of compact

1990 ◽  
Vol 55 (2) ◽  
pp. 645-655 ◽  
Author(s):  
Paul E. Howard
Keyword(s):  
Accumulation Point ◽  
Infinite Subset ◽  
Nonempty Intersection ◽  
Topological Spaces ◽  
Finite Intersection ◽  
Original Proof ◽  
Closed Sets ◽  
Finite Intersection Property ◽  
The Axiom Of Choice ◽  
Tychonoff Theorem

Several definitions of “compact” for topological spaces have appeared in the literature (see [5]). We will consider the following:Definition. A topological space X is1. Compact(1) if every open cover of X has a finite subcover.2. Compact(2) if every infinite subset E of X has a complete accumulation point (i.e., a point x0 ∈ X such that for every neighborhood U of x0, |E ∩ U| = |E|).3. Compact(3) if there is a subbase S for the topology on X such that every cover of X by members of S has a finite subcover.4. Compact(4) if each nest of closed, nonempty sets has a nonempty intersection.5. Compact(5) if every family of closed sets in X which has the finite intersection property (every finite subfamily has a nonempty intersection) has a nonempty intersection.6. Compact(6) if each net in X has a cluster point.7. Compact(7) if each net in X has a convergent subnet.This work was motivated primarily by consideration of various proofs that the Tychonoff theorem, T (“the product of compact topological spaces is compact”) is equivalent to the Axiom of Choice, AC. Tychonoff's original proof that AC implies T used Definition 2 [13]. Other proofs have used Definitions 3 and 5; see [5]. The proof by Kelley that T implies AC uses Definition 5 [6].

scholarly journals Interpreting classical theories in constructive ones

2000 ◽  
Vol 65 (4) ◽  
pp. 1785-1812 ◽  
Author(s):  
Jeremy Avigad
Keyword(s):  
Set Theory ◽  
Intuitionistic Logic ◽  
Second Order ◽  
Bounded Arithmetic ◽  
Admissible Set ◽  
Second Order Arithmetic ◽  
Order Arithmetic

AbstractA number of classical theories are interpreted in analogous theories that are based on intuitionistic logic. The classical theories considered include subsystems of first- and second-order arithmetic, bounded arithmetic, and admissible set theory.

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.

Sign in / Sign up

Export Citation Format

Share Document