-
Helmut Karzel (1928-2021)
Authors:
Hans Havlicek,
Alexander Kreuzer,
Hans-Joachim Kroll,
Kay Sörensen
Abstract:
Obituary for Professor Dr. Dr. h.c. Helmut Karzel, who passed away on June 22, 2021, at the age of 93.
Obituary for Professor Dr. Dr. h.c. Helmut Karzel, who passed away on June 22, 2021, at the age of 93.
△ Less
Submitted 17 September, 2022;
originally announced September 2022.
-
WaLDORf: Wasteless Language-model Distillation On Reading-comprehension
Authors:
James Yi Tian,
Alexander P. Kreuzer,
Pai-Hung Chen,
Hans-Martin Will
Abstract:
Transformer based Very Large Language Models (VLLMs) like BERT, XLNet and RoBERTa, have recently shown tremendous performance on a large variety of Natural Language Understanding (NLU) tasks. However, due to their size, these VLLMs are extremely resource intensive and cumbersome to deploy at production time. Several recent publications have looked into various ways to distil knowledge from a trans…
▽ More
Transformer based Very Large Language Models (VLLMs) like BERT, XLNet and RoBERTa, have recently shown tremendous performance on a large variety of Natural Language Understanding (NLU) tasks. However, due to their size, these VLLMs are extremely resource intensive and cumbersome to deploy at production time. Several recent publications have looked into various ways to distil knowledge from a transformer based VLLM (most commonly BERT-Base) into a smaller model which can run much faster at inference time. Here, we propose a novel set of techniques which together produce a task-specific hybrid convolutional and transformer model, WaLDORf, that achieves state-of-the-art inference speed while still being more accurate than previous distilled models.
△ Less
Submitted 18 February, 2020; v1 submitted 13 December, 2019;
originally announced December 2019.
-
Bayesian inference for dynamic vine copulas in higher dimensions
Authors:
Alexander Kreuzer,
Claudia Czado
Abstract:
We propose a class of dynamic vine copula models. This is an extension of static vine copulas and a generalization of dynamic C-vine and D-vine copulas studied by Almeida et al (2016) and Goel and Mehra (2019). Within this class, we allow for time-varying dependence by driving the vine copula parameters with latent AR(1) processes. This modeling approach is very flexible but estimation is not stra…
▽ More
We propose a class of dynamic vine copula models. This is an extension of static vine copulas and a generalization of dynamic C-vine and D-vine copulas studied by Almeida et al (2016) and Goel and Mehra (2019). Within this class, we allow for time-varying dependence by driving the vine copula parameters with latent AR(1) processes. This modeling approach is very flexible but estimation is not straightforward due to the high-dimensional parameter space. We propose a Bayesian estimation approach, which relies on a novel approximation of the posterior distribution. This approximation allows to use Markov Chain Monte Carlo methods, such as elliptical slice sampling, in a sequential way. In contrast to other Bayesian sequential estimation procedures for vine copula models as proposed by Gruber and Czado (2015), there is no need to collapse copula parameters to point estimates before proceeding to the next tree. Thus more information and uncertainty is propagated from lower to higher trees. A simulation study shows satisfactory performance of the Bayesian procedure. This dynamic modeling and inference approach can be applied in various fields, where static vine copulas have already proven to be successful, including environmental sciences, medicine and finance. Here we study the dependence among 21 exchange rates. For comparison we also estimate a static vine copula model and dynamic C-vine and D-vine copula models. This comparison shows superior performance of the proposed dynamic vine copula model with respect to one day ahead forecasting accuracy.
△ Less
Submitted 2 November, 2019;
originally announced November 2019.
-
Bayesian Multivariate Nonlinear State Space Copula Models
Authors:
Alexander Kreuzer,
Luciana Dalla Valle,
Claudia Czado
Abstract:
In this paper we propose a flexible class of multivariate nonlinear non-Gaussian state space models, based on copulas. More precisely, we assume that the observation equation and the state equation are defined by copula families that are not necessarily equal. For each time point, the resulting model can be described by a C-vine copula truncated after the first tree, where the root node is represe…
▽ More
In this paper we propose a flexible class of multivariate nonlinear non-Gaussian state space models, based on copulas. More precisely, we assume that the observation equation and the state equation are defined by copula families that are not necessarily equal. For each time point, the resulting model can be described by a C-vine copula truncated after the first tree, where the root node is represented by the latent state. Inference is performed within the Bayesian framework, using the Hamiltonian Monte Carlo method, where a further D-vine truncated after the first tree is used as prior distribution to capture the temporal dependence in the latent states. Simulation studies show that the proposed copula-based approach is extremely flexible, since it is able to describe a wide range of dependence structures and, at the same time, allows us to deal with missing data. The application to atmospheric pollutant measurement data shows that our approach is suitable for accurate modeling and prediction of data dynamics in the presence of missing values. Comparison to a Gaussian linear state space model and to Bayesian additive regression trees shows the superior performance of the proposed model with respect to predictive accuracy.
△ Less
Submitted 1 November, 2019;
originally announced November 2019.
-
The DEEP-ER project: I/O and resiliency extensions for the Cluster-Booster architecture
Authors:
Anke Kreuzer,
Norbert Eicker,
Jorge Amaya,
Raphael Leger,
Estela Suarez
Abstract:
The recently completed research project DEEP-ER has developed a variety of hardware and software technologies to improve the I/O capabilities of next generation high-performance computers, and to enable applications recovering from the larger hardware failure rates expected on these machines.
The heterogeneous Cluster-Booster architecture --first introduced in the predecessor DEEP project-- has…
▽ More
The recently completed research project DEEP-ER has developed a variety of hardware and software technologies to improve the I/O capabilities of next generation high-performance computers, and to enable applications recovering from the larger hardware failure rates expected on these machines.
The heterogeneous Cluster-Booster architecture --first introduced in the predecessor DEEP project-- has been extended by a multi-level memory hierarchy employing non-volatile and network-attached memory devices. Based on this hardware infrastructure, an I/O and resiliency software stack has been implemented combining and extending well established libraries and software tools, and sticking to standard user-interfaces. Real-world scientific codes have tested the projects' developments and demonstrated the improvements achieved without compromising the portability of the applications.
△ Less
Submitted 15 April, 2019;
originally announced April 2019.
-
Application performance on a Cluster-Booster system
Authors:
Anke Kreuzer,
Jorge Amaya,
Norbert Eicker,
Estela Suarez
Abstract:
The DEEP projects have developed a variety of hardware and software technologies aiming at improving the efficiency and usability of next generation high-performance computers. They evolve around an innovative concept for heterogeneous systems: the Cluster-Booster architecture. In it, a general purpose cluster is tightly coupled to a many-core system (the Booster). This modular way of integrating…
▽ More
The DEEP projects have developed a variety of hardware and software technologies aiming at improving the efficiency and usability of next generation high-performance computers. They evolve around an innovative concept for heterogeneous systems: the Cluster-Booster architecture. In it, a general purpose cluster is tightly coupled to a many-core system (the Booster). This modular way of integrating heterogeneous components enables applications to freely choose the kind of computing resources on which it runs most efficiently. Codes might even be partitioned to map specific requirements of code-parts onto the best suited hardware. This paper presents for the first time measurements done by a real world scientific application demonstrating the performance gain achieved with this kind of code-partition approach.
△ Less
Submitted 10 April, 2019;
originally announced April 2019.
-
A Bayesian Non-linear State Space Copula Model to Predict Air Pollution in Bei**g
Authors:
Alexander Kreuzer,
Luciana Dalla Valle,
Claudia Czado
Abstract:
Air pollution is a serious issue that currently affects many industrial cities in the world and can cause severe illness to the population. In particular, it has been proven that extreme high levels of airborne contaminants have dangerous short-term effects on human health, in terms of increased hospital admissions for cardiovascular and respiratory diseases and increased mortality risk. For these…
▽ More
Air pollution is a serious issue that currently affects many industrial cities in the world and can cause severe illness to the population. In particular, it has been proven that extreme high levels of airborne contaminants have dangerous short-term effects on human health, in terms of increased hospital admissions for cardiovascular and respiratory diseases and increased mortality risk. For these reasons, accurate estimation and prediction of airborne pollutant concentration is crucial. In this paper, we propose a flexible novel approach to model hourly measurements of fine particulate matter and meteorological data collected in Bei**g in 2014. We show that the standard state space model, based on Gaussian assumptions, does not correctly capture the time dynamics of the observations. Therefore, we propose a non-linear non-Gaussian state space model where both the observation and the state equations are defined by copula specifications, and we perform Bayesian inference using the Hamiltonian Monte Carlo method. The proposed copula state space approach is very flexible, since it allows us to separately model the marginals and to accommodate a wide variety of dependence structures in the data dynamics. We show that the proposed approach allows us not only to predict particulate matter measurements, but also to investigate the effects of user specified climate scenarios.
△ Less
Submitted 11 November, 2019; v1 submitted 20 March, 2019;
originally announced March 2019.
-
Efficient Bayesian inference for nonlinear state space models with univariate autoregressive state equation
Authors:
Alexander Kreuzer,
Claudia Czado
Abstract:
Latent autoregressive processes are a popular choice to model time varying parameters. These models can be formulated as nonlinear state space models for which inference is not straightforward due to the high number of parameters. Therefore maximum likelihood methods are often infeasible and researchers rely on alternative techniques, such as Gibbs sampling. But conventional Gibbs samplers are oft…
▽ More
Latent autoregressive processes are a popular choice to model time varying parameters. These models can be formulated as nonlinear state space models for which inference is not straightforward due to the high number of parameters. Therefore maximum likelihood methods are often infeasible and researchers rely on alternative techniques, such as Gibbs sampling. But conventional Gibbs samplers are often tailored to specific situations and suffer from high autocorrelation among repeated draws. We present a Gibbs sampler for general nonlinear state space models with an univariate autoregressive state equation. For this we employ an interweaving strategy and elliptical slice sampling to exploit the dependence implied by the autoregressive process. Within a simulation study we demonstrate the efficiency of the proposed sampler for bivariate dynamic copula models. Further we are interested in modeling the volatility return relationship. Therefore we use the proposed sampler to estimate the parameters of stochastic volatility models with skew Student t errors and the parameters of a novel bivariate dynamic mixture copula model. This model allows for dynamic asymmetric tail dependence. Comparison to relevant benchmark models, such as the DCC-GARCH or a Student t copula model, with respect to predictive accuracy shows the superior performance of the proposed approach.
△ Less
Submitted 31 October, 2019; v1 submitted 27 February, 2019;
originally announced February 2019.
-
Bayesian inference for a single factor copula stochastic volatility model using Hamiltonian Monte Carlo
Authors:
Alexander Kreuzer,
Claudia Czado
Abstract:
For modeling multivariate financial time series we propose a single factor copula model together with stochastic volatility margins. This model generalizes single factor models relying on the multivariate normal distribution and allows for symmetric and asymmetric tail dependence. We develop joint Bayesian inference using Hamiltonian Monte Carlo (HMC) within Gibbs sampling. Thus we avoid informati…
▽ More
For modeling multivariate financial time series we propose a single factor copula model together with stochastic volatility margins. This model generalizes single factor models relying on the multivariate normal distribution and allows for symmetric and asymmetric tail dependence. We develop joint Bayesian inference using Hamiltonian Monte Carlo (HMC) within Gibbs sampling. Thus we avoid information loss caused by the two-step approach for margins and dependence in copula models as followed by Schamberger et al(2017). Further, the Bayesian approach allows for high dimensional parameter spaces as they are present here in addition to uncertainty quantification through credible intervals. By allowing for indicators for different copula families the copula families are selected automatically in the Bayesian framework. In a first simulation study the performance of HMC is compared to the Markov Chain Monte Carlo (MCMC) approach developed by Schamberger et al(2017) for the copula part. It is shown that HMC considerably outperforms this approach in terms of effective sample size, MSE and observed coverage probabilities. In a second simulation study satisfactory performance is seen for the full HMC within Gibbs procedure. The approach is illustrated for a portfolio of financial assets with respect to one-day ahead value at risk forecasts. We provide comparison to a two-step estimation procedure of the proposed model and to relevant benchmark models: a model with dynamic linear models for the margins and a single factor copula for the dependence proposed by Schamberger et al(2017) and a multivariate factor stochastic volatility model proposed by Kastner et al(2017). Our proposed approach shows superior performance.
△ Less
Submitted 19 July, 2019; v1 submitted 26 August, 2018;
originally announced August 2018.
-
Heavy tailed spatial autocorrelation models
Authors:
A. Kreuzer,
T. Erhardt,
T. Nagler,
C. Czado
Abstract:
Appropriate models for spatially autocorrelated data account for the fact that observations are not independent. A popular model in this context is the simultaneous autoregressive (SAR) model that allows to model the spatial dependency structure of a response variable and the influence of covariates on this variable. This spatial regression model assumes that the error follows a normal distributio…
▽ More
Appropriate models for spatially autocorrelated data account for the fact that observations are not independent. A popular model in this context is the simultaneous autoregressive (SAR) model that allows to model the spatial dependency structure of a response variable and the influence of covariates on this variable. This spatial regression model assumes that the error follows a normal distribution. Since this assumption cannot always be met, it is necessary to extend this model to other error distributions. We propose the extension to the $t$-distribution, the tSAR model, which can be used if we observe heavy tails in the fitted residuals of the SAR model. In addition, we provide a variance estimate that considers the spatial structure of a variable which helps us to specify inputs for our models. An extended simulation study shows that the proposed estimators of the tSAR model are performing well and in an application to fire danger we see that the tSAR model is a notable improvement compared to the SAR model.
△ Less
Submitted 11 July, 2017;
originally announced July 2017.
-
Obituary: Walter Benz (1931-2017)
Authors:
Alexander Kreuzer,
Hans Havlicek
Abstract:
Emeritus Professor Dr. Dr. h.c. Walter Benz passed away on 13 January 2017.
Emeritus Professor Dr. Dr. h.c. Walter Benz passed away on 13 January 2017.
△ Less
Submitted 8 April, 2017;
originally announced April 2017.
-
On the Uniform Computational Content of the Baire Category Theorem
Authors:
Vasco Brattka,
Matthew Hendtlass,
Alexander P. Kreuzer
Abstract:
We study the uniform computational content of different versions of the Baire Category Theorem in the Weihrauch lattice. The Baire Category Theorem can be seen as a pigeonhole principle that states that a complete (i.e., "large") metric space cannot be decomposed into countably many nowhere dense (i.e., "small") pieces. The Baire Category Theorem is an illuminating example of a theorem that can be…
▽ More
We study the uniform computational content of different versions of the Baire Category Theorem in the Weihrauch lattice. The Baire Category Theorem can be seen as a pigeonhole principle that states that a complete (i.e., "large") metric space cannot be decomposed into countably many nowhere dense (i.e., "small") pieces. The Baire Category Theorem is an illuminating example of a theorem that can be used to demonstrate that one classical theorem can have several different computational interpretations. For one, we distinguish two different logical versions of the theorem, where one can be seen as the contrapositive form of the other one. The first version aims to find an uncovered point in the space, given a sequence of nowhere dense closed sets. The second version aims to find the index of a closed set that is somewhere dense, given a sequence of closed sets that cover the space. Even though the two statements behind these versions are equivalent to each other in classical logic, they are not equivalent in intuitionistic logic and likewise they exhibit different computational behavior in the Weihrauch lattice. Besides this logical distinction, we also consider different ways how the sequence of closed sets is "given". Essentially, we can distinguish between positive and negative information on closed sets. We discuss all the four resulting versions of the Baire Category Theorem. Somewhat surprisingly it turns out that the difference in providing the input information can also be expressed with the jump operation. Finally, we also relate the Baire Category Theorem to notions of genericity and computably comeager sets.
△ Less
Submitted 24 August, 2016; v1 submitted 7 October, 2015;
originally announced October 2015.
-
A lower bound on Gowers' FIN_k theorem
Authors:
Alexander P. Kreuzer
Abstract:
Gowers' FIN$_k$ theorem, also called Gowers' pigeonhole principle or Gowers' theorem, is a Ramsey-type theorem. It first occurred in the study of Banach space theory and is a natural generalization of Hindman's theorem. In this short note, we will show that Gowers' FIN$_k$ theorem does not follow from ACA$_0$.
Gowers' FIN$_k$ theorem, also called Gowers' pigeonhole principle or Gowers' theorem, is a Ramsey-type theorem. It first occurred in the study of Banach space theory and is a natural generalization of Hindman's theorem. In this short note, we will show that Gowers' FIN$_k$ theorem does not follow from ACA$_0$.
△ Less
Submitted 7 October, 2015;
originally announced October 2015.
-
On the Uniform Computational Content of Computability Theory
Authors:
Vasco Brattka,
Matthew Hendtlass,
Alexander P. Kreuzer
Abstract:
We demonstrate that the Weihrauch lattice can be used to classify the uniform computational content of computability-theoretic properties as well as the computational content of theorems in one common setting. The properties that we study include diagonal non-computability, hyperimmunity, complete consistent extensions of Peano arithmetic, 1-genericity, Martin-Löf randomness, and cohesiveness. The…
▽ More
We demonstrate that the Weihrauch lattice can be used to classify the uniform computational content of computability-theoretic properties as well as the computational content of theorems in one common setting. The properties that we study include diagonal non-computability, hyperimmunity, complete consistent extensions of Peano arithmetic, 1-genericity, Martin-Löf randomness, and cohesiveness. The theorems that we include in our case study are the low basis theorem of Jockusch and Soare, the Kleene-Post theorem, and Friedberg's jump inversion theorem. It turns out that all the aforementioned properties and many theorems in computability theory, including all theorems that claim the existence of some Turing degree, have very little uniform computational content: they are located outside of the upper cone of binary choice (also known as LLPO); we call problems with this property indiscriminative. Since practically all theorems from classical analysis whose computational content has been classified are discriminative, our observation could yield an explanation for why theorems and results in computability theory typically have very few direct consequences in other disciplines such as analysis. A notable exception in our case study is the low basis theorem which is discriminative. This is perhaps why it is considered to be one of the most applicable theorems in computability theory. In some cases a bridge between the indiscriminative world and the discriminative world of classical mathematics can be established via a suitable residual operation and we demonstrate this in the case of the cohesiveness problem and the problem of consistent complete extensions of Peano arithmetic. Both turn out to be the quotient of two discriminative problems.
△ Less
Submitted 27 June, 2017; v1 submitted 2 January, 2015;
originally announced January 2015.
-
Measure theory and higher order arithmetic
Authors:
Alexander P. Kreuzer
Abstract:
We investigate the statement that the Lebesgue measure defined on all subsets of the Cantor space exists. As base system we take $\mathsf{ACA}_0^ω+ (μ)$. The system $\mathsf{ACA}_0^ω$ is the higher order extension of Friedman's system $\mathsf{ACA}_0$, and $(μ)$ denotes Feferman's $μ$, that is a uniform functional for arithmetical comprehension defined by $f(μ(f))=0$ if $\exists n f(n)=0$ for…
▽ More
We investigate the statement that the Lebesgue measure defined on all subsets of the Cantor space exists. As base system we take $\mathsf{ACA}_0^ω+ (μ)$. The system $\mathsf{ACA}_0^ω$ is the higher order extension of Friedman's system $\mathsf{ACA}_0$, and $(μ)$ denotes Feferman's $μ$, that is a uniform functional for arithmetical comprehension defined by $f(μ(f))=0$ if $\exists n f(n)=0$ for $f\in \mathbb{N}^\mathbb{N}$.
Feferman's $μ$ will provide countable unions and intersections of sets of reals and is, in fact, equivalent to this. For this reasons $\mathsf{ACA}_0^ω+ (μ)$ is the weakest fragment of higher order arithmetic where $σ$-additive measures are directly definable.
We obtain that over $\mathsf{ACA}_0^ω+ (μ)$ the existence of the Lebesgue measure is $Π^1_2$-conservative over $\mathsf{ACA}_0^ω$ and with this conservative over $\mathsf{PA}$. Moreover, we establish a corresponding program extraction result.
△ Less
Submitted 8 April, 2015; v1 submitted 5 December, 2013;
originally announced December 2013.
-
Bounded variation and the strength of Helly's selection theorem
Authors:
Alexander P. Kreuzer
Abstract:
We analyze the strength of Helly's selection theorem HST, which is the most important compactness theorem on the space of functions of bounded variation. For this we utilize a new representation of this space intermediate between $L_1$ and the Sobolev space W1,1, compatible with the, so called, weak* topology. We obtain that HST is instance-wise equivalent to the Bolzano-Weierstraß principle over…
▽ More
We analyze the strength of Helly's selection theorem HST, which is the most important compactness theorem on the space of functions of bounded variation. For this we utilize a new representation of this space intermediate between $L_1$ and the Sobolev space W1,1, compatible with the, so called, weak* topology. We obtain that HST is instance-wise equivalent to the Bolzano-Weierstraß principle over RCA0. With this HST is equivalent to ACA0 over RCA0. A similar classification is obtained in the Weihrauch lattice.
△ Less
Submitted 23 December, 2014; v1 submitted 18 August, 2013;
originally announced August 2013.
-
On principles between $Σ_1$- and $Σ_2$-induction, and monotone enumerations
Authors:
Alexander P. Kreuzer,
Keita Yokoyama
Abstract:
We show that many principles of first-order arithmetic, previously only known to lie strictly between $Σ_1$-induction and $Σ_2$-induction, are equivalent to the well-foundedness of $ω^ω$.
Among these principles are the iteration of partial functions ($PΣ_1$) of Hájek and Paris, the bounded monotone enumerations principle (non-iterated, BME$_1$) by Chong, Slaman, and Yang, the relativized Paris-H…
▽ More
We show that many principles of first-order arithmetic, previously only known to lie strictly between $Σ_1$-induction and $Σ_2$-induction, are equivalent to the well-foundedness of $ω^ω$.
Among these principles are the iteration of partial functions ($PΣ_1$) of Hájek and Paris, the bounded monotone enumerations principle (non-iterated, BME$_1$) by Chong, Slaman, and Yang, the relativized Paris-Harrington principle for pairs, and the totality of the relativized Ackermann-Péter function.
With this we show that the well-foundedness of $ω^ω$ is a far more widespread than usually suspected.
Further, we investigate the $k$-iterated version of the bounded monotone iterations principle (BME$_k$), and show that it is equivalent to the well-foundedness of the $k+1$-height $ω$-tower.
△ Less
Submitted 13 December, 2015; v1 submitted 8 June, 2013;
originally announced June 2013.
-
Minimal idempotent ultrafilters and the Auslander-Ellis theorem
Authors:
Alexander P. Kreuzer
Abstract:
We characterize the existence of minimal idempotent ultrafilters (on N) in the style of reverse mathematics and higher-order reverse mathematics using the Auslander-Ellis theorem and variant thereof.
We obtain that the existence of minimal idempotent ultrafilters restricted to countable algebras of sets is equivalent to the Auslander-Ellis theorem (AET) and that the existence of minimal idempote…
▽ More
We characterize the existence of minimal idempotent ultrafilters (on N) in the style of reverse mathematics and higher-order reverse mathematics using the Auslander-Ellis theorem and variant thereof.
We obtain that the existence of minimal idempotent ultrafilters restricted to countable algebras of sets is equivalent to the Auslander-Ellis theorem (AET) and that the existence of minimal idempotent ultrafilters as higher-order objects is $Π^1_2$-conservative over a refinement of AET.
△ Less
Submitted 9 October, 2015; v1 submitted 28 May, 2013;
originally announced May 2013.
-
On idempotent ultrafilters in higher-order reverse mathematics
Authors:
Alexander P. Kreuzer
Abstract:
We analyze the strength of the existence of idempotent ultrafilters in higher-order reverse mathematics.
Let (Uidem) be the statement that an idempotent ultrafilter on the natural numbers exists. We show that over ACA_0^w, the higher-order extension of ACA_0, the statement (Uidem) implies the iterated Hindman's theorem (IHT), and we show that ACA_0^w + (Uidem) is Pi^1_2-conservative over ACA_0^w…
▽ More
We analyze the strength of the existence of idempotent ultrafilters in higher-order reverse mathematics.
Let (Uidem) be the statement that an idempotent ultrafilter on the natural numbers exists. We show that over ACA_0^w, the higher-order extension of ACA_0, the statement (Uidem) implies the iterated Hindman's theorem (IHT), and we show that ACA_0^w + (Uidem) is Pi^1_2-conservative over ACA_0^w + IHT and thus over ACA_0^+.
△ Less
Submitted 28 February, 2013; v1 submitted 7 August, 2012;
originally announced August 2012.
-
From Bolzano-Weierstraß to Arzelà-Ascoli
Authors:
Alexander P. Kreuzer
Abstract:
We show how one can obtain solutions to the Arzelà-Ascoli theorem using suitable applications of the Bolzano-Weierstraß principle. With this, we can apply the results from \cite{aK} and obtain a classification of the strength of instances of the Arzelà-Ascoli theorem and a variant of it.
Let AA be the statement that each equicontinuous sequence of functions f_n: [0,1] --> [0,1] contains a subseq…
▽ More
We show how one can obtain solutions to the Arzelà-Ascoli theorem using suitable applications of the Bolzano-Weierstraß principle. With this, we can apply the results from \cite{aK} and obtain a classification of the strength of instances of the Arzelà-Ascoli theorem and a variant of it.
Let AA be the statement that each equicontinuous sequence of functions f_n: [0,1] --> [0,1] contains a subsequence that converges uniformly with the rate 2^-k and let AA_weak be the statement that each such sequence contains a subsequence which converges uniformly but possibly without any rate.
We show that AA is instance-wise equivalent over RCA_0 to the Bolzano-Weierstraß principle BW and that AA_weak is instance-wise equivalent over WKL_0 to BW_weak, and thus to the strong cohesive principle StCOH. Moreover, we show that over RCA_0 the principles AA_weak, BW_weak + WKL and StCOH + WKL are equivalent.
△ Less
Submitted 24 May, 2012;
originally announced May 2012.
-
Non-principal ultrafilters, program extraction and higher order reverse mathematics
Authors:
Alexander P. Kreuzer
Abstract:
We investigate the strength of the existence of a non-principal ultrafilter over fragments of higher order arithmetic.
Let U be the statement that a non-principal ultrafilter exists and let ACA_0^ω be the higher order extension of ACA_0. We show that ACA_0^ω+U is Π^1_2-conservative over ACA_0^ω and thus that ACA_0^ω+\U is conservative over PA.
Moreover, we provide a program extraction method a…
▽ More
We investigate the strength of the existence of a non-principal ultrafilter over fragments of higher order arithmetic.
Let U be the statement that a non-principal ultrafilter exists and let ACA_0^ω be the higher order extension of ACA_0. We show that ACA_0^ω+U is Π^1_2-conservative over ACA_0^ω and thus that ACA_0^ω+\U is conservative over PA.
Moreover, we provide a program extraction method and show that from a proof of a strictly Π^1_2 statement \forall f \exists g A(f,g) in ACA_0^ω+U a realizing term in Gödel's system T can be extracted. This means that one can extract a term t, such that A(f,t(f)).
△ Less
Submitted 20 September, 2011;
originally announced September 2011.
-
On the strength of weak compactness
Authors:
Alexander P. Kreuzer
Abstract:
We study the logical and computational strength of weak compactness in the separable Hilbert space \ell_2.
Let weak-BW be the statement the every bounded sequence in \ell_2 has a weak cluster point. It is known that weak-BW is equivalent to ACA_0 over RCA_0 and thus that it is equivalent to (nested uses of) the usual Bolzano-Weierstraß principle BW. We show that weak-BW is instance-wise equivale…
▽ More
We study the logical and computational strength of weak compactness in the separable Hilbert space \ell_2.
Let weak-BW be the statement the every bounded sequence in \ell_2 has a weak cluster point. It is known that weak-BW is equivalent to ACA_0 over RCA_0 and thus that it is equivalent to (nested uses of) the usual Bolzano-Weierstraß principle BW. We show that weak-BW is instance-wise equivalent to the Π^0_2-CA. This means that for each Π^0_2 sentence A(n) there is a sequence (x_i) in \ell_2, such that one can define the comprehension functions for A(n) recursively in a cluster point of (x_i). As consequence we obtain that the Turing degrees d > 0" are exactly those degrees that contain a weak cluster point of any computable, bounded sequence in \ell_2. Since a cluster point of any sequence in the unit interval [0,1] can be computed in a degree low over 0', this show also that instances of weak-BW are strictly stronger than instances of BW.
We also comment on the strength of weak-BW in the context of abstract Hilbert spaces in the sense of Kohlenbach and show that his construction of a solution for the functional interpretation of weak compactness is optimal.
△ Less
Submitted 25 June, 2011;
originally announced June 2011.
-
The cohesive principle and the Bolzano-Weierstraß principle
Authors:
Alexander P. Kreuzer
Abstract:
The aim of this paper is to determine the logical and computational strength of instances of the Bolzano-Weierstraß principle (BW) and a weak variant of it.
We show that BW is instance-wise equivalent to the weak König's lemma for $Σ^0_1$-trees ($Σ^0_1$-WKL). This means that from every bounded sequence of reals one can compute an infinite $Σ^0_1$-0/1-tree, such that each infinite branch of it yi…
▽ More
The aim of this paper is to determine the logical and computational strength of instances of the Bolzano-Weierstraß principle (BW) and a weak variant of it.
We show that BW is instance-wise equivalent to the weak König's lemma for $Σ^0_1$-trees ($Σ^0_1$-WKL). This means that from every bounded sequence of reals one can compute an infinite $Σ^0_1$-0/1-tree, such that each infinite branch of it yields an accumulation point and vice versa. Especially, this shows that the degrees d >> 0' are exactly those containing an accumulation point for all bounded computable sequences.
Let BW_weak be the principle stating that every bounded sequence of real numbers contains a Cauchy subsequence (a sequence converging but not necessarily fast). We show that BW_weak is instance-wise equivalent to the (strong) cohesive principle (StCOH) and - using this - obtain a classification of the computational and logical strength of BW_weak. Especially we show that BW_weak does not solve the halting problem and does not lead to more than primitive recursive growth. Therefore it is strictly weaker than BW. We also discuss possible uses of BW_weak.
△ Less
Submitted 18 January, 2011; v1 submitted 28 May, 2010;
originally announced May 2010.
