Choice principles, the bar rule and autonomously iterated comprehension schemes in analysis

1983 ◽  
Vol 48 (1) ◽  
pp. 63-70 ◽  
Author(s):  
S. Feferman ◽  
G. Jäger
Keyword(s):  
General Result ◽  
Recursive Relation ◽  
Transfinite Induction ◽  
Conservative Extension ◽  
Main Result Theorem ◽  
Functional Interpretation ◽  
Result Theorem ◽  
Primitive Recursive ◽  
Comprehension Axiom

In [10] Friedman showed that (-AC) is a conservative extension of (-CA)<ε0for-sentences wherei= min(n+ 2, 4), i.e.,i= 2, 3, 4 forn= 0, 1, 2 +m. Feferman [5], [7] and Tait [11], [12] reobtained this result forn= 0, 1 and even with (-DC) instead of (-AC). Feferman and Sieg established in [9] the conservativeness of (-DC) over (-CA)<ε0for-sentences (ias above) for alln. In each paper, different methods of proof have been used. In particular, Feferman and Sieg showed how to apply familiar proof-theoretical techniques by passing through languages with Skolem functionals.In this paper we study the same choice principles in the presence of theBar Rule(BR), which permits one to infer the scheme of transfinite induction on a primitive recursive relation ≺ when it has been proved that ≺ is wellfounded. The main result (Theorem 1 below) characterizes (-DC) + (BR) as a conservative extension of a system of the autonomously iterated-comprehension axiom for-sentences (idepending onnas above). Forn= 0 this has been proved by Feferman in the form that (-DC) + (BR) is a conservative extension of (-CA)<Γ0; this was first done in [8] by use of the Gödel functional interpretation for the stronger systemZω+μ+ (QF-AC) + (BR) and then more recently by the simpler methods of [9]. Jäger showed how the latter methods could also be used to obtain the general result of Theorem 1 below.

A system of abstract constructive ordinals

1972 ◽  
Vol 37 (2) ◽  
pp. 355-374 ◽  
Author(s):  
W. A. Howard
Keyword(s):  
Finite Type ◽  
Free Variable ◽  
Transfinite Induction ◽  
Functional Interpretation ◽  
Variable Theory ◽  
Inductive Definitions ◽  
Heyting Arithmetic ◽  
Abstract Notion ◽  
Primitive Recursive ◽  
Primitive Recursive Functionals

As Gödel [6] has pointed out, there is a certain interchangeability between the intuitionistic notion of proof and the notion of constructive functional of finite type. He achieves this interchange in the direction from logic to functionals by his functional interpretation of Heyting arithmetic H in a free variable theory T of primitive recursive functionals of finite type. In the present paper we shall extend Gödel's functional interpretation to the case in which H and T are extended by adding an abstract notion of constructive ordinal. In other words, we obtain the Gödel functional interpretation of an intuitionistic theory U of numbers (i.e., nonnegative integers) and constructive ordinals in a free variable theory V of finite type over both numbers and constructive ordinals. This allows us to obtain an analysis of noniterated positive inductive definitions [8].The notion of constructive ordinal to be treated is as follows. There is given a function J which embeds the nonnegative integers in the constructive ordinals. A constructive ordinal of the form Jn is said to be minimal. There is also given a function δ which associates to each constructive ordinal Z and number n a constructive ordinal δZn which we denote by Zn. When Z is nonminimal, each Zn is called an immediate predecessor of Z. The basic principle for forming constructive ordinals says: for every function f from numbers n to constructive ordinals, there exists a constructive ordinal Z such that Zn = fn for all n. The principle of transfinite induction with respect to constructive ordinals says: if a property Q(Z) of constructive ordinals Z holds for minimal Z, and if ∀nQ(Zn) → Q(Z) holds for all Z, then Q(Z) holds for all Z.

scholarly journals A note on the paper "Optimality conditions for nonsmooth interval-valued and multiobjective semi-infinite programming"

2020 ◽  
Author(s):  
Nazih Abderrazzak Gadhi ◽  
Aissam Ichatouhane
Keyword(s):  
Optimality Conditions ◽  
Programming Problem ◽  
Optimality Condition ◽  
Short Proof ◽  
Necessary Optimality Condition ◽  
Main Result Theorem ◽  
Correct Formulation ◽  
Result Theorem ◽  
Infinite Programming ◽  
Interval Valued

A nonsmooth semi-infinite interval-valued vector programming problem is solved in the paper by Jennane et all. (RAIRO-Oper. Res. doi: 10.1051/ro/2020066, 2020). The necessary optimality condition obtained by the authors, as well as its proof, is false. Some counterexamples are given to refute some results on which the main result (Theorem 4.5) is based. For the convinience of the reader, we correct the faulty in those results, propose a correct formulation of Theorem 4.5 and give also a short proof.

Closure Theorem for Analytic Subgroups of Real Lie Groups

1976 ◽  
Vol 19 (4) ◽  
pp. 435-439 ◽  
Author(s):  
D. Ž. Djoković
Keyword(s):  
Lie Groups ◽  
Lie Group ◽  
Closed Subgroup ◽  
Main Result Theorem ◽  
Closure Theorem ◽  
Result Theorem ◽  
Analytic Subgroup

Let G be a real Lie group, A a closed subgroup of G and B an analytic subgroup of G. Assume that B normalizes A and that AB is closed in G. Then our main result (Theorem 1) asserts that .This result generalizes Lemma 2 in the paper [4], G. Hochschild has pointed out to me that the proof of that lemma given in [4] is not complete but that it can be easily completed.

Parallel Translation in Vector Bundles with Abelian Structure Group and the Gauss-Bonnet Formula

1973 ◽  
Vol 25 (4) ◽  
pp. 765-771
Author(s):  
Hansklaus Rummler
Keyword(s):  
Riemannian Manifold ◽  
Simple Proof ◽  
General Result ◽  
Tangent Bundle ◽  
Vector Bundles ◽  
Structure Group ◽  
Parallel Translation ◽  
Result Theorem

Most proofs for the classical Gauss-Bonnet formula use special coordinates, or other non-trivial preparations. Here, a simple proof is given, based on the fact that the structure group SO(2) of the tangent bundle of an oriented 2-dimensional Riemannian manifold is abelian. Since only this hypothesis is used, we prove a slightly more general result (Theorem 1).

scholarly journals NOTES AND PROBLEMS A GENERAL BOUND FOR THE LIMITING DISTRIBUTION OF BREITUNG'S STATISTIC

2008 ◽  
Vol 24 (5) ◽  
pp. 1443-1455 ◽  
Author(s):  
James Davidson ◽  
Jan R. Magnus ◽  
Jan Wiegerinck
Keyword(s):  
General Result ◽  
Random Variables ◽  
Nonparametric Test ◽  
Limiting Distribution ◽  
Residue Theorem ◽  
Prove Theorem ◽  
General Bound ◽  
Result Theorem ◽  
Special Case ◽  
Cauchy’S Residue Theorem

We consider the Breitung (2002, Journal of Econometrics 108, 343–363) statistic ξn, which provides a nonparametric test of the I(1) hypothesis. If ξ denotes the limit in distribution of ξn as n → ∞, we prove (Theorem 1) that 0 ≤ ξ ≤ 1/π2, a result that holds under any assumption on the underlying random variables. The result is a special case of a more general result (Theorem 3), which we prove using the so-called cotangent method associated with Cauchy's residue theorem.

scholarly journals On radicals of finite near-rings

1984 ◽  
Vol 27 (3) ◽  
pp. 247-259 ◽  
Author(s):  
K. Kaarli
Keyword(s):  
Main Result Theorem ◽  
Result Theorem

In this paper the study of radicals of finite near-rings is initiated. The main result (Theorem 4.3) gives a description of hereditary radicals having hereditary semisimple classes too. Also it is shown that there exist non-hereditary radicals having hereditary semisimple classes.

Absorption Probabilities for Sums of Random Variables Defined on a Finite Markov Chain

1962 ◽  
Vol 58 (2) ◽  
pp. 286-298 ◽  
Author(s):  
H. D. Miller
Keyword(s):  
Markov Chain ◽  
Asymptotic Expression ◽  
Random Variables ◽  
Partial Sums ◽  
Finite Markov Chain ◽  
Initial State ◽  
Main Result Theorem ◽  
Sums Of Random Variables ◽  
Result Theorem ◽  
Image Position

SummaryThis paper is essentially a continuation of the previous one (5) and the notation established therein will be freely repeated. The sequence {ξr} of random variables is defined on a positively regular finite Markov chain {kr} as in (5) and the partial sums and are considered. Let ζn be the first positive ζr and let πjk(y), the ‘ruin’ function or absorption probability, be defined by The main result (Theorem 1) is an asymptotic expression for πjk(y) for large y in the case when , the expectation of ξ1 being computed under the unique stationary distribution for k0, the initial state of the chain, and unconditional on k1.

scholarly journals Independent inner functions in the classical domains

1987 ◽  
Vol 29 (2) ◽  
pp. 229-236
Author(s):  
Tomasz M. Wolniewicz
Keyword(s):  
Unit Ball ◽  
Hardy Spaces ◽  
Isometric Embedding ◽  
Symmetric Domain ◽  
Type I ◽  
Bounded Symmetric Domains ◽  
Inner Functions ◽  
Main Result Theorem ◽  
Complemented Subspace ◽  
Result Theorem

Let Bn denote the unit ball and Un the unit polydisc in Cn. In this paper we consider questions concerned with inner functions and embeddings of Hardy spaces over bounded symmetric domains. The main result (Theorem 2) states that for a classical symmetric domain D of type I and rank(D) = s, there exists an isometric embedding of Hl(Us) onto a complemented subspace of Hl(D). This should be compared with results of Wojtaszczyk [13] and Bourgain [3, 4] which state that H1(Bn) is isomorphic to Hl(U) while for n>m, Hl(Un) cannot be isomorphically embedded onto a complemented subspace of H1(Um). Since balls are the only bounded symmetric domains of rank 1 and they are of type I, Theorem 2 shows that if rank(D1) = 1, rank(D2) > 1 then H1(D1) is not isomorphic to H1(D2). It is natural to expect this to hold always when rank(D1 ≠ rank(D2) but unfortunately we were not able to prove this.

scholarly journals Term extraction and Ramsey's theorem for pairs

2012 ◽  
Vol 77 (3) ◽  
pp. 853-895 ◽  
Author(s):  
Alexander P. Kreuzer ◽  
Ulrich Kohlenbach
Keyword(s):  
Uniform Method ◽  
Second Step ◽  
Functional Interpretation ◽  
Ramsey's Theorem ◽  
Term Extraction ◽  
Ramsey’S Theorem ◽  
Skolem Functions ◽  
Primitive Recursive

AbstractIn this paper we study with proof-theoretic methods the function(al)s provably recursive relative to Ramsey's theorem for pairs and the cohesive principle (COH).Our main result on COH is that the type 2 functional provably recursive fromare primitive recursive. This also provides a uniform method to extract bounds from proofs that use these principles. As a consequence we obtain a new proof of the fact thatis-conservative over PRA.Recent work of the first author showed thatis equivalent to a weak variant of the Bolzano-Weierstraß principle. This makes it possible to use our results to analyze not only combinatorial but also analytical proofs.For Ramsey's theorem for pairs and two colorswe obtain the upper bounded that the type 2 functional provable recursive relative toare inT1. This is the fragment of Gödel's systemTcontaining only type 1 recursion—roughly speaking it consists of functions of Ackermann type. With this we also obtain a uniform method for the extraction ofT1-bounds from proofs that use. Moreover, this yields a new proof of the fact thatis-conservative over.The results are obtained in two steps: in the first step a term including Skolem functions for the above principles is extracted from a given proof. This is done using Gödel's functional interpretation. After this the term is normalized, such that only specific instances of the Skolem functions are used. In the second step this term is interpreted using-comprehension. The comprehension is then eliminated in favor of induction using either elimination of monotone Skolem functions (for COH) or Howard's ordinal analysis of bar recursion (for).

A formalization of the theory of ordinal numbers

1965 ◽  
Vol 30 (3) ◽  
pp. 295-317 ◽  
Author(s):  
Gaisi Takeuti
Keyword(s):  
Set Theory ◽  
Natural Extension ◽  
Mathematical Induction ◽  
Predicate Calculus ◽  
Transfinite Induction ◽  
First Order ◽  
Recursive Functions ◽  
Ordinal Numbers ◽  
Primitive Recursive ◽  
Order Predicate Calculus

Although Peano's arithmetic can be developed in set theories, it can also be developed independently. This is also true for the theory of ordinal numbers. The author formalized the theory of ordinal numbers in logical systems GLC (in [2]) and FLC (in [3]). These logical systems which contain the concept of ‘arbitrary predicates’ or ‘arbitrary functions’ are of higher order than the first order predicate calculus with equality. In this paper we shall develop the theory of ordinal numbers in the first order predicate calculus with equality as an extension of Peano's arithmetic. This theory will prove to be easy to manage and fairly powerful in the following sense: If A is a sentence of the theory of ordinal numbers, then A is a theorem of our system if and only if the natural translation of A in set theory is a theorem of Zermelo-Fraenkel set theory. It will be treated as a natural extension of Peano's arithmetic. The latter consists of axiom schemata of primitive recursive functions and mathematical induction, while the theory of ordinal numbers consists of axiom schemata of primitive recursive functions of ordinal numbers (cf. [5]), of transfinite induction, of replacement and of cardinals. The latter three axiom schemata can be considered as extensions of mathematical induction.In the theory of ordinal numbers thus developed, we shall construct a model of Zermelo-Fraenkel's set theory by following Gödel's construction in [1]. Our intention is as follows: We shall define a relation α ∈ β as a primitive recursive predicate, which corresponds to F′ α ε F′ β in [1]; Gödel defined the constructible model Δ using the primitive notion ε in the universe or, in other words, using the whole set theory.

Sign in / Sign up

Export Citation Format

Share Document