-
Fraïssé's conjecture, partial impredicativity and well-ordering principles, part I
Authors:
Anton Freund
Abstract:
Fraïssé's conjecture (proved by Laver) is implied by the $Π^1_1$-comprehension axiom of reverse mathematics, as shown by Montalbán. The implication must be strict for reasons of quantifier complexity, but it seems that no better bound has been known. We locate such a bound in a hierarchy of Suzuki and Yokoyama, which extends Towsner's framework of partial impredicativity. Specifically, we show tha…
▽ More
Fraïssé's conjecture (proved by Laver) is implied by the $Π^1_1$-comprehension axiom of reverse mathematics, as shown by Montalbán. The implication must be strict for reasons of quantifier complexity, but it seems that no better bound has been known. We locate such a bound in a hierarchy of Suzuki and Yokoyama, which extends Towsner's framework of partial impredicativity. Specifically, we show that Fraïssé's conjecture is implied by a principle of pseudo $Π^1_1$-comprehension. As part of the proof, we introduce a cofinite version of the $Δ^0_2$-Ramsey theorem, which may be of independent interest. We also relate pseudo $Π^1_1$-comprehension to principles of pseudo $β$-model reflection (due to Suzuki and Yokoyama) and reflection for $ω$-models of transfinite induction (studied by Rathjen and Valencia-Vizcaíno). In a forthcoming companion paper, we characterize pseudo $Π^1_1$-comprehension by a well-ordering principle, to get a transparent combinatorial bound for the strength of Fraïssé's conjecture.
△ Less
Submitted 19 June, 2024;
originally announced June 2024.
-
Dilators and the reverse mathematics zoo
Authors:
Anton Freund
Abstract:
A predilator is a particularly uniform transformation of linear orders. We have a dilator when the transformation preserves well-foundedness. Over the theory $\mathsf{ACA}_0$ from reverse mathematics, any $Π^1_2$-formula is equivalent to the statement that some predilator is a dilator. We show how this completeness result breaks down without arithmetical comprehension: over…
▽ More
A predilator is a particularly uniform transformation of linear orders. We have a dilator when the transformation preserves well-foundedness. Over the theory $\mathsf{ACA}_0$ from reverse mathematics, any $Π^1_2$-formula is equivalent to the statement that some predilator is a dilator. We show how this completeness result breaks down without arithmetical comprehension: over $\mathsf{RCA}_0+\mathsf{PA}$, the statements from a large part of the reverse mathematics zoo are not equivalent to some predilator being a dilator.
△ Less
Submitted 10 April, 2024;
originally announced April 2024.
-
An Introduction to Mathematical Logic
Authors:
Anton Freund
Abstract:
This introduction begins with a section on fundamental notions of mathematical logic, including propositional logic, predicate or first-order logic, completeness, compactness, the Löwenheim-Skolem theorem, Craig interpolation, Beth's definability theorem and Herbrand's theorem. It continues with a section on Gödel's incompleteness theorems, which includes a discussion of first-order arithmetic and…
▽ More
This introduction begins with a section on fundamental notions of mathematical logic, including propositional logic, predicate or first-order logic, completeness, compactness, the Löwenheim-Skolem theorem, Craig interpolation, Beth's definability theorem and Herbrand's theorem. It continues with a section on Gödel's incompleteness theorems, which includes a discussion of first-order arithmetic and primitive recursive functions. This is followed by three sections that are devoted, respectively, to proof theory (provably total recursive functions and Goodstein sequences for $\mathsf{IΣ}_1$), computability (fundamental notions and an analysis of Kőnig's lemma in terms of the low basis theorem) and model theory (ultraproducts, chains and the Ax-Grothendieck theorem). We conclude with some brief introductory remarks about set theory (with more details reserved for a separate lecture). The author uses these notes for a first logic course for undergraduates in mathematics, which consists of 28 lectures and 14 exercise sessions of 90 minutes each. In such a course, it may be necessary to omit some material, which is straightforward since all sections except for the first two are independent of each other.
△ Less
Submitted 27 November, 2023; v1 submitted 15 October, 2023;
originally announced October 2023.
-
Extension of the Langevin power curve analysis by separation per operational state
Authors:
Christian Wiedemann,
Henrik M. Bette,
Matthias Wächter,
Jan A. Freund,
Thomas Guhr,
Joachim Peinke
Abstract:
In the last few years, the dynamical characterization of the power output of a wind turbine by means of a Langevin equation has been well established. For this approach, temporally highly resolved measurements of wind speed and power output are used to obtain the drift and diffusion coefficients of the energy conversion process. These coefficients fully determine a Langevin stochastic differential…
▽ More
In the last few years, the dynamical characterization of the power output of a wind turbine by means of a Langevin equation has been well established. For this approach, temporally highly resolved measurements of wind speed and power output are used to obtain the drift and diffusion coefficients of the energy conversion process. These coefficients fully determine a Langevin stochastic differential equation with Gaussian white noise. The drift term specifies the deterministic behavior of the system whereas the diffusion term describes the stochastic behavior of the system. A precise estimation of these coefficients is essential to understand the dynamics of the power conversion process of the wind turbine. We show that the dynamics of the power output of a wind turbine have a hidden dependency on turbine's different operational states. Here, we use an approach based on clustering Pearson correlation matrices for different observables on a moving time window to identify different operational states. We have identified five operational states in total, for example the state of rated power. Those different operational states distinguish non-stationary behavior in the mutual dependencies and represent different turbine control settings. As a next step, we condition our Langevin analysis on these different states to reveal distinctly different behaviors of the power conversion process for each operational state. Moreover, in our new representation hysteresis effects which have typically appeared in the Langevin dynamics of wind turbines seem to be resolved. We assign these typically observed hysteresis effects clearly to the change of the wind energy system between our estimated different operational states. In this contribution, we discuss further consequences for the meaning of hysteric switching and detection of malbehaviors in wind turbines.
△ Less
Submitted 5 February, 2024; v1 submitted 24 May, 2023;
originally announced May 2023.
-
Provable better quasi orders
Authors:
Anton Freund,
Alberto Marcone,
Fedor Pakhomov,
Giovanni Soldà
Abstract:
It has recently been shown that fairly strong axiom systems such as $\mathsf{ACA}_0$ cannot prove that the antichain with three elements is a better quasi order ($\mathsf{bqo}$). In the present paper, we give a complete characterization of the finite partial orders that are provably $\mathsf{bqo}$ in such axiom systems. The result will also be extended to infinite orders. As an application, we der…
▽ More
It has recently been shown that fairly strong axiom systems such as $\mathsf{ACA}_0$ cannot prove that the antichain with three elements is a better quasi order ($\mathsf{bqo}$). In the present paper, we give a complete characterization of the finite partial orders that are provably $\mathsf{bqo}$ in such axiom systems. The result will also be extended to infinite orders. As an application, we derive that a version of the minimal bad array lemma is weak over $\mathsf{ACA_0}$. In sharp contrast, a recent result shows that the same version is equivalent to $Π^1_2$-comprehension over the stronger base theory $\mathsf{ATR}_0$.
△ Less
Submitted 1 May, 2023;
originally announced May 2023.
-
Weak well orders and Fraïssé's conjecture
Authors:
Anton Freund,
Davide Manca
Abstract:
The notion of well order admits an alternative definition in terms of embeddings between initial segments. We use the framework of reverse mathematics to investigate the logical strength of this definition and its connection with Fraïssé's conjecture, which has been proved by Laver. We also fill a small gap in Shore's proof that Fraïssé's conjecture implies arithmetic transfinite recursion over…
▽ More
The notion of well order admits an alternative definition in terms of embeddings between initial segments. We use the framework of reverse mathematics to investigate the logical strength of this definition and its connection with Fraïssé's conjecture, which has been proved by Laver. We also fill a small gap in Shore's proof that Fraïssé's conjecture implies arithmetic transfinite recursion over ${\bf RCA}_0$, by giving a new proof of $Σ^0_2$-induction.
△ Less
Submitted 6 April, 2023;
originally announced April 2023.
-
The logical strength of minimal bad arrays
Authors:
Anton Freund,
Fedor Pakhomov,
Giovanni Soldà
Abstract:
This paper studies logical aspects of the notion of better quasi order, which has been introduced by C. Nash-Williams (Mathematical Proceedings of the Cambridge Philosophical Society 1965 & 1968). A central tool in the theory of better quasi orders is the minimal bad array lemma. We show that this lemma is exceptionally strong from the viewpoint of reverse mathematics, a framework from mathematica…
▽ More
This paper studies logical aspects of the notion of better quasi order, which has been introduced by C. Nash-Williams (Mathematical Proceedings of the Cambridge Philosophical Society 1965 & 1968). A central tool in the theory of better quasi orders is the minimal bad array lemma. We show that this lemma is exceptionally strong from the viewpoint of reverse mathematics, a framework from mathematical logic. Specifically, it is equivalent to the set existence principle of $Π^1_2$-comprehension, over the base theory $\mathsf{ATR_0}$.
△ Less
Submitted 1 April, 2023;
originally announced April 2023.
-
Normal functions and maximal order types
Authors:
Anton Freund,
Davide Manca
Abstract:
Transformations of well partial orders induce functions on the ordinals, via the notion of maximal order type. In most examples from the literature, these functions are not normal, in marked contrast with the central role that normal functions play in ordinal analysis and related work from computability theory. The present paper aims to explain this phenomenon. In order to do so, we investigate a…
▽ More
Transformations of well partial orders induce functions on the ordinals, via the notion of maximal order type. In most examples from the literature, these functions are not normal, in marked contrast with the central role that normal functions play in ordinal analysis and related work from computability theory. The present paper aims to explain this phenomenon. In order to do so, we investigate a rich class of order transformations that are known as $\mathsf{WPO}$-dilators. According to a first main result of this paper, $\mathsf{WPO}$-dilators induce normal functions when they satisfy a rather restrictive condition, which we call strong normality. Moreover, the reverse implication holds as well, for reasonably well behaved $\mathsf{WPO}$-dilators. Strong normality also allows us to explain another phenomenon: by previous work of Freund, Rathjen and Weiermann, a uniform Kruskal theorem for $\mathsf{WPO}$-dilators is as strong as $Π^1_1$-comprehension, while the corresponding result for normal dilators on linear orders is equivalent to the much weaker principle of $Π^1_1$-induction. As our second main result, we show~that $Π^1_1$-induction is equivalent to the uniform Kruskal theorem for $\mathsf{WPO}$-dilators that are strongly normal.
△ Less
Submitted 23 September, 2022;
originally announced September 2022.
-
The uniform Kruskal theorem: between finite combinatorics and strong set existence
Authors:
Anton Freund,
Patrick Uftring
Abstract:
The uniform Kruskal theorem extends the original result for trees to general recursive data types. As shown by A. Freund, M. Rathjen and A. Weiermann, it is equivalent to $Π^1_1$-comprehension, over $\mathsf{RCA_0}$ with the chain antichain principle ($\mathsf{CAC}$). This result provides a connection between finite combinatorics and abstract set existence. The present paper sheds further light on…
▽ More
The uniform Kruskal theorem extends the original result for trees to general recursive data types. As shown by A. Freund, M. Rathjen and A. Weiermann, it is equivalent to $Π^1_1$-comprehension, over $\mathsf{RCA_0}$ with the chain antichain principle ($\mathsf{CAC}$). This result provides a connection between finite combinatorics and abstract set existence. The present paper sheds further light on this connection. First, we show that the original Kruskal theorem is equivalent to the uniform version for data types that are finitely generated. Secondly, we prove a dichotomy result for a natural variant of the uniform Kruskal theorem. On the one hand, this variant still implies $Π^1_1$-comprehension over $\mathsf{RCA}_0+\mathsf{CAC}$. On the other hand, it becomes weak when $\mathsf{CAC}$ is removed from the base theory.
△ Less
Submitted 30 July, 2022;
originally announced August 2022.
-
On the logical strength of the better quasi order with three elements
Authors:
Anton Freund
Abstract:
The notion of better quasi order ($\mathsf{BQO}$), due to Nash-Williams, is very fruitful mathematically and intriguing from the standpoint of logic, due to several long-standing open problems. In the present paper, we make a significant step towards one of these: Let $\mathbf 3$ be the discrete order with three elements. We show that arithmetical recursion along the natural numbers (…
▽ More
The notion of better quasi order ($\mathsf{BQO}$), due to Nash-Williams, is very fruitful mathematically and intriguing from the standpoint of logic, due to several long-standing open problems. In the present paper, we make a significant step towards one of these: Let $\mathbf 3$ be the discrete order with three elements. We show that arithmetical recursion along the natural numbers ($\mathsf{ACA}_0^+$) follows from $\mathbf 3$ being $\mathsf{BQO}$, over the base theory $\mathsf{RCA_0}$ from reverse mathematics. Also over the latter, we deduce arithmetical transfinite recursion ($\mathsf{ATR}_0$) from the assumption that $\mathbf 3$ is $Δ^0_2\text{-}\mathsf{BQO}$, which plays a role in work of Montalbán.
△ Less
Submitted 10 August, 2022; v1 submitted 22 June, 2022;
originally announced June 2022.
-
Higman's lemma is stronger for better quasi orders
Authors:
Anton Freund
Abstract:
We prove that Higman's lemma is strictly stronger for better quasi orders than for well quasi orders, within the framework of reverse mathematics. In fact, we show a stronger result: the infinite Ramsey theorem (for tuples of all lengths) follows from the statement that any array $[\mathbb N]^{n+1}\to\mathbb N^n\times X$ for a well order $X$ and $n\in\mathbb N$ is good, over the base theory…
▽ More
We prove that Higman's lemma is strictly stronger for better quasi orders than for well quasi orders, within the framework of reverse mathematics. In fact, we show a stronger result: the infinite Ramsey theorem (for tuples of all lengths) follows from the statement that any array $[\mathbb N]^{n+1}\to\mathbb N^n\times X$ for a well order $X$ and $n\in\mathbb N$ is good, over the base theory $\mathsf{RCA_0}$.
△ Less
Submitted 9 May, 2022;
originally announced May 2022.
-
Impredicativity and Trees with Gap Condition: A Second Course on Ordinal Analysis
Authors:
Anton Freund
Abstract:
These lecture notes introduce central notions of impredicative ordinal analysis, such as the Bachmann-Howard ordinal and the method of collapsing, which transforms uncountable proof trees into countable ones. Specifically, we analyze parameter-free $Π^1_1$-comprehension and show that it cannot prove the extended Kruskal theorem due to Harvey Friedman (not even for two labels). In terms of prerequi…
▽ More
These lecture notes introduce central notions of impredicative ordinal analysis, such as the Bachmann-Howard ordinal and the method of collapsing, which transforms uncountable proof trees into countable ones. Specifically, we analyze parameter-free $Π^1_1$-comprehension and show that it cannot prove the extended Kruskal theorem due to Harvey Friedman (not even for two labels). In terms of prerequisites, we build on a previous lecture on the ordinal analysis of Peano arithmetic. The present material is intended for 12 lectures and 6 exercise sessions of 90 minutes each.
△ Less
Submitted 10 August, 2022; v1 submitted 20 April, 2022;
originally announced April 2022.
-
R.E. Bruck, proof mining and a rate of asymptotic regularity for ergodic averages in Banach spaces
Authors:
Anton Freund,
Ulrich Kohlenbach
Abstract:
We analyze a proof of Bruck to obtain an explicit rate of asymptotic regularity for Cesàro means in uniformly convex Banach spaces. Our rate will only depend on a norm bound and a modulus $η$ of uniform convexity. One ingredient for the proof by Bruck is a result of Pisier, which shows that every uniformly convex (in fact every uniformly nonsquare) Banach space has some Rademacher type $q>1$ with…
▽ More
We analyze a proof of Bruck to obtain an explicit rate of asymptotic regularity for Cesàro means in uniformly convex Banach spaces. Our rate will only depend on a norm bound and a modulus $η$ of uniform convexity. One ingredient for the proof by Bruck is a result of Pisier, which shows that every uniformly convex (in fact every uniformly nonsquare) Banach space has some Rademacher type $q>1$ with a suitable constant $C_q$. We explicitly determine $q$ and $C_q$, which only depend on the single value $η(1)$ of our modulus. Beyond these specific results, we summarize how work of Bruck has inspired developments in the proof mining program, which applies tools from logic to obtain results in various areas of mathematics.
△ Less
Submitted 10 August, 2022; v1 submitted 8 April, 2022;
originally announced April 2022.
-
Reverse mathematics of a uniform Kruskal-Friedman theorem
Authors:
Anton Freund
Abstract:
The Kruskal-Friedman theorem asserts: in any infinite sequence of finite trees with ordinal labels, some tree can be embedded into a later one, by an embedding that respects a certain gap condition. This strengthening of the original Kruskal theorem has been proved by I. Kříž (Ann. Math. 1989), in confirmation of a conjecture due to H. Friedman, who had established the result for finitely many lab…
▽ More
The Kruskal-Friedman theorem asserts: in any infinite sequence of finite trees with ordinal labels, some tree can be embedded into a later one, by an embedding that respects a certain gap condition. This strengthening of the original Kruskal theorem has been proved by I. Kříž (Ann. Math. 1989), in confirmation of a conjecture due to H. Friedman, who had established the result for finitely many labels. It provides one of the strongest mathematical examples for the independence phenomenon from Gödel's theorems. The gap condition is particularly relevant due to its connection with the graph minor theorem of N. Robertson and P. Seymour. In the present paper, we consider a uniform version of the Kruskal-Friedman theorem, which extends the result from trees to general recursive data types. Our main theorem shows that this uniform version is equivalent both to $Π^1_1$-transfinite recursion and to a minimal bad sequence principle of Kříž, over the base theory $\mathsf{RCA_0}$ from reverse mathematics. This sheds new light on the role of infinity in finite combinatorics.
△ Less
Submitted 23 February, 2022; v1 submitted 16 December, 2021;
originally announced December 2021.
-
Well ordering principles for iterated $Π^1_1$-comprehension
Authors:
Anton Freund,
Michael Rathjen
Abstract:
We introduce ordinal collapsing principles that are inspired by proof theory but have a set theoretic flavor. These principles are shown to be equivalent to iterated $Π^1_1$-comprehension and the existence of admissible sets, over weak base theories. Our work extends a previous result on the non-iterated case, which had been conjectured in Montalbán's "Open questions in reverse mathematics" (Bull.…
▽ More
We introduce ordinal collapsing principles that are inspired by proof theory but have a set theoretic flavor. These principles are shown to be equivalent to iterated $Π^1_1$-comprehension and the existence of admissible sets, over weak base theories. Our work extends a previous result on the non-iterated case, which had been conjectured in Montalbán's "Open questions in reverse mathematics" (Bull. Symb. Log. 17(3)2011). This previous result has already been applied to the reverse mathematics of combinatorial and set theoretic principles. The present paper is a significant contribution to a general approach that connects these fields.
△ Less
Submitted 15 December, 2021;
originally announced December 2021.
-
Unprovability in Mathematics: A First Course on Ordinal Analysis
Authors:
Anton Freund
Abstract:
These are the lecture notes of an introductory course on ordinal analysis. Our selection of topics is guided by the aim to give a complete and direct proof of a mathematical independence result: Kruskal's theorem for binary trees is unprovable in conservative extensions of Peano arithmetic (note that much stronger results of this type are due to Harvey Friedman). Concerning prerequisites, we assum…
▽ More
These are the lecture notes of an introductory course on ordinal analysis. Our selection of topics is guided by the aim to give a complete and direct proof of a mathematical independence result: Kruskal's theorem for binary trees is unprovable in conservative extensions of Peano arithmetic (note that much stronger results of this type are due to Harvey Friedman). Concerning prerequisites, we assume a solid introduction to mathematical logic but no specialized knowledge of proof theory. The material in these notes is intended for 12 lectures and 6 exercise sessions of 90 minutes each.
△ Less
Submitted 21 April, 2022; v1 submitted 13 September, 2021;
originally announced September 2021.
-
Bounds for a nonlinear ergodic theorem for Banach spaces
Authors:
Anton Freund,
Ulrich Kohlenbach
Abstract:
We extract quantitative information (specifically, a rate of metastability in the sense of Terence Tao) from a proof due to Kazuo Kobayasi and Isao Miyadera, which shows strong convergence for Cesàro means of nonexpansive maps on Banach spaces.
We extract quantitative information (specifically, a rate of metastability in the sense of Terence Tao) from a proof due to Kazuo Kobayasi and Isao Miyadera, which shows strong convergence for Cesàro means of nonexpansive maps on Banach spaces.
△ Less
Submitted 19 August, 2021;
originally announced August 2021.
-
Bachmann-Howard Derivatives
Authors:
Anton Freund
Abstract:
It is generally accepted that H. Friedman's gap condition is closely related to iterated collapsing functions from ordinal analysis. But what precisely is the connection? We offer the following answer: In a previous paper we have shown that the gap condition arises from an iterative construction on transformations of partial orders. Here we show that the parallel construction for linear orders yie…
▽ More
It is generally accepted that H. Friedman's gap condition is closely related to iterated collapsing functions from ordinal analysis. But what precisely is the connection? We offer the following answer: In a previous paper we have shown that the gap condition arises from an iterative construction on transformations of partial orders. Here we show that the parallel construction for linear orders yields familiar collapsing functions. The iteration step in the linear case is an instance of a general construction that we call `Bachmann-Howard derivative'. In the present paper, we focus on the unary case, i.e., on the gap condition for sequences rather than trees and, correspondingly, on addition-free ordinal notation systems. This is partly for convenience, but it also allows us to clarify a phenomenon that is specific to the unary setting: As shown by van der Meeren, Rathjen and Weiermann, the gap condition on sequences admits two linearizations with rather different properties. We will see that these correspond to different recursive constructions of sequences.
△ Less
Submitted 20 May, 2021;
originally announced May 2021.
-
Patterns of resemblance and Bachmann-Howard fixed points
Authors:
Anton Freund
Abstract:
Timothy Carlson's patterns of resemblance employ the notion of $Σ_1$-elementarity to describe large computable ordinals. It has been conjectured that a relativization of these patterns to dilators leads to an equivalence with $Π^1_1$-comprehension (Question 27 of A. Montalbán's "Open questions in reverse mathematics", Bull. Symb. Log. 17(3)2011, 431-454). In the present paper we prove this conject…
▽ More
Timothy Carlson's patterns of resemblance employ the notion of $Σ_1$-elementarity to describe large computable ordinals. It has been conjectured that a relativization of these patterns to dilators leads to an equivalence with $Π^1_1$-comprehension (Question 27 of A. Montalbán's "Open questions in reverse mathematics", Bull. Symb. Log. 17(3)2011, 431-454). In the present paper we prove this conjecture. The crucial direction (towards $Π^1_1$-comprehension) is reduced to a previous result of the author, which is concerned with relativizations of the Bachmann-Howard ordinal.
△ Less
Submitted 6 January, 2021; v1 submitted 18 December, 2020;
originally announced December 2020.
-
Ackermann and Goodstein go functorial
Authors:
Juan P. Aguilera,
Anton Freund,
Michael Rathjen,
Andreas Weiermann
Abstract:
We present variants of Goodstein's theorem that are equivalent to arithmetical comprehension and to arithmetical transfinite recursion, respectively, over a weak base theory. These variants differ from the usual Goodstein theorem in that they (necessarily) entail the existence of complex infinite objects. As part of our proof, we show that the Veblen hierarchy of normal functions on the ordinals i…
▽ More
We present variants of Goodstein's theorem that are equivalent to arithmetical comprehension and to arithmetical transfinite recursion, respectively, over a weak base theory. These variants differ from the usual Goodstein theorem in that they (necessarily) entail the existence of complex infinite objects. As part of our proof, we show that the Veblen hierarchy of normal functions on the ordinals is closely related to an extension of the Ackermann function by direct limits.
△ Less
Submitted 2 December, 2020; v1 submitted 6 November, 2020;
originally announced November 2020.
-
Well ordering principles and $Π^1_4$-statements: a pilot study
Authors:
Anton Freund
Abstract:
In previous work, the author has shown that $Π^1_1$-induction along $\mathbb N$ is equivalent to a suitable formalization of the statement that every normal function on the ordinals has a fixed point. More precisely, this was proved for a representation of normal functions in terms of J.-Y. Girard's dilators, which are particularly uniform transformations of well orders. The present paper works on…
▽ More
In previous work, the author has shown that $Π^1_1$-induction along $\mathbb N$ is equivalent to a suitable formalization of the statement that every normal function on the ordinals has a fixed point. More precisely, this was proved for a representation of normal functions in terms of J.-Y. Girard's dilators, which are particularly uniform transformations of well orders. The present paper works on the next type level and considers uniform transformations of dilators, which are called $2$-ptykes. We show that $Π^1_2$-induction along $\mathbb N$ is equivalent to the existence of fixed points for all $2$-ptykes that satisfy a certain normality condition. Beyond this specific result, the paper paves the way for the analysis of further $Π^1_4$-statements in terms of well ordering principles.
△ Less
Submitted 22 June, 2020;
originally announced June 2020.
-
What is effective transfinite recursion in reverse mathematics?
Authors:
Anton Freund
Abstract:
In the context of reverse mathematics, effective transfinite recursion refers to a principle that allows us to construct sequences of sets by recursion along arbitrary well orders, provided that each set is $Δ^0_1$-definable relative to the previous stages of the recursion. It is known that this principle is provable in $\mathbf{ACA}_0$. In the present note, we argue that a common formulation of e…
▽ More
In the context of reverse mathematics, effective transfinite recursion refers to a principle that allows us to construct sequences of sets by recursion along arbitrary well orders, provided that each set is $Δ^0_1$-definable relative to the previous stages of the recursion. It is known that this principle is provable in $\mathbf{ACA}_0$. In the present note, we argue that a common formulation of effective transfinite recursion is too restrictive. We then propose a more liberal formulation, which appears very natural and is still provable in $\mathbf{ACA}_0$.
△ Less
Submitted 30 June, 2021; v1 submitted 16 June, 2020;
originally announced June 2020.
-
A mathematical commitment without computational strength
Authors:
Anton Freund
Abstract:
We present a new manifestation of Gödel's second incompleteness theorem and discuss its foundational significance, in particular with respect to Hilbert's program. Specifically, we consider a proper extension of Peano arithmetic ($\mathbf{PA}$) by a mathematically meaningful axiom scheme that consists of $Σ^0_2$-sentences. These sentences assert that each computably enumerable ($Σ^0_1$-definable w…
▽ More
We present a new manifestation of Gödel's second incompleteness theorem and discuss its foundational significance, in particular with respect to Hilbert's program. Specifically, we consider a proper extension of Peano arithmetic ($\mathbf{PA}$) by a mathematically meaningful axiom scheme that consists of $Σ^0_2$-sentences. These sentences assert that each computably enumerable ($Σ^0_1$-definable without parameters) property of finite binary trees has a finite basis. Since this fact entails the existence of polynomial time algorithms, it is important for computer science. On a technical level, our axiom scheme is a variant of an independence result due to Harvey Friedman. At the same time, the meta-mathematical properties of our axiom scheme distinguish it from most known independence results: Due to its logical complexity, our axiom scheme does not add computational strength. The only known method to establish its independence relies on Gödel's second incompleteness theorem. In contrast, Gödel's theorem is not needed for typical examples of $Π^0_2$-independence (such as the Paris-Harrington principle), since computational strength provides an extensional invariant on the level of $Π^0_2$-sentences.
△ Less
Submitted 15 April, 2020;
originally announced April 2020.
-
From Kruskal's theorem to Friedman's gap condition
Authors:
Anton Freund
Abstract:
Harvey Friedman's gap condition on embeddings of finite labelled trees plays an important role in combinatorics (proof of the graph minor theorem) and mathematical logic (strong independence results). In the present paper we show that the gap condition can be reconstructed from a small number of well-motivated building blocks: it arises via iterated applications of a uniform Kruskal theorem.
Harvey Friedman's gap condition on embeddings of finite labelled trees plays an important role in combinatorics (proof of the graph minor theorem) and mathematical logic (strong independence results). In the present paper we show that the gap condition can be reconstructed from a small number of well-motivated building blocks: it arises via iterated applications of a uniform Kruskal theorem.
△ Less
Submitted 5 March, 2020;
originally announced March 2020.
-
Minimal bad sequences are necessary for a uniform Kruskal theorem
Authors:
Anton Freund,
Michael Rathjen,
Andreas Weiermann
Abstract:
The minimal bad sequence argument due to Nash-Williams is a powerful tool in combinatorics with important implications for theoretical computer science. In particular, it yields a very elegant proof of Kruskal's theorem. At the same time, it is known that Kruskal's theorem does not require the full strength of the minimal bad sequence argument. This claim can be made precise in the framework of re…
▽ More
The minimal bad sequence argument due to Nash-Williams is a powerful tool in combinatorics with important implications for theoretical computer science. In particular, it yields a very elegant proof of Kruskal's theorem. At the same time, it is known that Kruskal's theorem does not require the full strength of the minimal bad sequence argument. This claim can be made precise in the framework of reverse mathematics, where the existence of minimal bad sequences is equivalent to a principle known as $Π^1_1$-comprehension, which is much stronger than Kruskal's theorem. In the present paper we give a uniform version of Kruskal's theorem by relativizing it to certain transformations of well partial orders. We show that $Π^1_1$-comprehension is equivalent to our uniform Kruskal theorem (over $\mathbf{RCA}_0$ together with the chain-antichain principle). This means that any proof of the uniform Kruskal theorem must entail the existence of minimal bad sequences. As a by-product of our investigation, we obtain uniform proofs of several Kruskal-type independence results.
△ Less
Submitted 17 January, 2020;
originally announced January 2020.
-
Set-theoretic reflection is equivalent to induction over well-founded classes
Authors:
Anton Freund
Abstract:
We show that induction over $Δ(\mathbb R)$-definable well-founded classes is equivalent to the reflection principle which asserts that any true formula of first order set theory with real parameters holds in some transitive set. The equivalence is proved in primitive recursive set theory (which is weaker than Kripke-Platek set theory) extended by the axiom of dependent choice.
We show that induction over $Δ(\mathbb R)$-definable well-founded classes is equivalent to the reflection principle which asserts that any true formula of first order set theory with real parameters holds in some transitive set. The equivalence is proved in primitive recursive set theory (which is weaker than Kripke-Platek set theory) extended by the axiom of dependent choice.
△ Less
Submitted 6 July, 2021; v1 submitted 2 September, 2019;
originally announced September 2019.
-
A note on ordinal exponentiation and derivatives of normal functions
Authors:
Anton Freund
Abstract:
Michael Rathjen and the present author have shown that $Π^1_1$-bar induction is equivalent to (a suitable formalization of) the statement that every normal function has a derivative, provably in $\mathbf{ACA_0}$. In this note we show that the base theory can be weakened to $\mathbf{RCA_0}$. Our argument makes crucial use of a normal function $f$ with $f(α)\leq 1+α^2$ and $f'(α)=ω^{ω^α}$. We will a…
▽ More
Michael Rathjen and the present author have shown that $Π^1_1$-bar induction is equivalent to (a suitable formalization of) the statement that every normal function has a derivative, provably in $\mathbf{ACA_0}$. In this note we show that the base theory can be weakened to $\mathbf{RCA_0}$. Our argument makes crucial use of a normal function $f$ with $f(α)\leq 1+α^2$ and $f'(α)=ω^{ω^α}$. We will also exhibit a normal function $g$ with $g(α)\leq 1+α\cdot 2$ and $g'(α)=ω^{1+α}$.
△ Less
Submitted 30 June, 2021; v1 submitted 1 August, 2019;
originally announced August 2019.
-
Predicative collapsing principles
Authors:
Anton Freund
Abstract:
We show that arithmetical transfinite recursion is equivalent to a suitable formalization of the following: For every ordinal $α$ there exists an ordinal $β$ such that $1+β\cdot(β+α)$ (ordinal arithmetic) admits an almost order preserving collapse into $β$. Arithmetical comprehension is equivalent to a statement of the same form, with $β\cdotα$ at the place of $β\cdot(β+α)$. We will also character…
▽ More
We show that arithmetical transfinite recursion is equivalent to a suitable formalization of the following: For every ordinal $α$ there exists an ordinal $β$ such that $1+β\cdot(β+α)$ (ordinal arithmetic) admits an almost order preserving collapse into $β$. Arithmetical comprehension is equivalent to a statement of the same form, with $β\cdotα$ at the place of $β\cdot(β+α)$. We will also characterize the principles that any set is contained in a countable coded $ω$-model of arithmetical transfinite recursion resp. arithmetical comprehension.
△ Less
Submitted 5 August, 2020; v1 submitted 18 June, 2019;
originally announced June 2019.
-
How strong are single fixed points of normal functions?
Authors:
Anton Freund
Abstract:
In a recent paper by M. Rathjen and the present author it has been shown that the statement ``every normal function has a derivative'' is equivalent to $Π^1_1$-bar induction. The equivalence was proved over $\mathbf{ACA_0}$, for a suitable representation of normal functions in terms of dilators. In the present paper we show that the statement ``every normal function has at least one fixed point''…
▽ More
In a recent paper by M. Rathjen and the present author it has been shown that the statement ``every normal function has a derivative'' is equivalent to $Π^1_1$-bar induction. The equivalence was proved over $\mathbf{ACA_0}$, for a suitable representation of normal functions in terms of dilators. In the present paper we show that the statement ``every normal function has at least one fixed point'' is equivalent to $Π^1_1$-induction along the natural numbers.
△ Less
Submitted 6 July, 2021; v1 submitted 3 June, 2019;
originally announced June 2019.
-
Derivatives of normal functions in reverse mathematics
Authors:
Anton Freund,
Michael Rathjen
Abstract:
Consider a normal function $f$ on the ordinals (i. e. a function $f$ that is strictly increasing and continuous at limit stages). By enumerating the fixed points of $f$ we obtain a faster normal function $f'$, called the derivative of $f$. The present paper investigates this important construction from the viewpoint of reverse mathematics. Within this framework we must restrict our attention to no…
▽ More
Consider a normal function $f$ on the ordinals (i. e. a function $f$ that is strictly increasing and continuous at limit stages). By enumerating the fixed points of $f$ we obtain a faster normal function $f'$, called the derivative of $f$. The present paper investigates this important construction from the viewpoint of reverse mathematics. Within this framework we must restrict our attention to normal functions $f:\aleph_1\rightarrow\aleph_1$ that are represented by dilators (i. e. particularly uniform endofunctors on the category of well-orders, as introduced by J.-Y. Girard). Due to a categorical construction of P. Aczel, each normal dilator $T$ has a derivative $\partial T$. We will give a new construction of the derivative, which shows that the existence and fundamental properties of $\partial T$ can already be established in the theory $\mathbf{RCA}_0$. The latter does not prove, however, that $\partial T$ preserves well-foundedness. Our main result shows that the statement ``for every normal dilator $T$, its derivative $\partial T$ preserves well-foundedness'' is $\mathbf{ACA}_0$-provably equivalent to $Π^1_1$-bar induction (and hence to $Σ^1_1$-dependent choice and to $Π^1_2$-reflection for $ω$-models).
△ Less
Submitted 8 July, 2021; v1 submitted 9 April, 2019;
originally announced April 2019.
-
Weak-winner phase synchronization: A curious case of weak interactions
Authors:
Anshul Choudhary,
Arindam Saha,
Samuel Krueger,
Christian Finke,
Epaminondas Rosa, Jr.,
Jan A. Freund,
Ulrike Feudel
Abstract:
We report the observation of a novel and non-trivial synchronization state in a system consisting of three oscillators coupled in a linear chain. For certain ranges of coupling strength the weakly coupled oscillator pair exhibits phase synchronization while the strongly coupled oscillator pair does not. This intriguing "weak-winner" synchronization phenomenon can be explained by the interplay betw…
▽ More
We report the observation of a novel and non-trivial synchronization state in a system consisting of three oscillators coupled in a linear chain. For certain ranges of coupling strength the weakly coupled oscillator pair exhibits phase synchronization while the strongly coupled oscillator pair does not. This intriguing "weak-winner" synchronization phenomenon can be explained by the interplay between non-isochronicity and natural frequency of the oscillator, as coupling strength is varied. Further, we present sufficient conditions under which the weak-winner phase synchronization can occur for limit cycle as well as chaotic oscillators. Employing model system from ecology as well as a paradigmatic model from physics, we demonstrate that this phenomenon is a generic feature for a large class of coupled oscillator systems. The realization of this peculiar yet quite generic weak-winner dynamics can have far reaching consequences in a wide range of scientific disciplines that deal with the phenomenon of phase synchronization. Our results also highlight the role of non-isochronicity (shear) as a fundamental feature of an oscillator in sha** the emergent dynamics.
△ Less
Submitted 13 August, 2020; v1 submitted 6 December, 2018;
originally announced December 2018.
-
Computable Aspects of the Bachmann-Howard Principle
Authors:
Anton Freund
Abstract:
We have previously established that $Π^1_1$-comprehension is equivalent to the statement that every dilator has a well-founded Bachmann-Howard fixed point, over $\mathbf{ATR_0}$. In the present paper we show that the base theory can be lowered to $\mathbf{RCA_0}$. We also show that the minimal Bachmann-Howard fixed point of a dilator $T$ can be represented by a notation system $\vartheta(T)$, whic…
▽ More
We have previously established that $Π^1_1$-comprehension is equivalent to the statement that every dilator has a well-founded Bachmann-Howard fixed point, over $\mathbf{ATR_0}$. In the present paper we show that the base theory can be lowered to $\mathbf{RCA_0}$. We also show that the minimal Bachmann-Howard fixed point of a dilator $T$ can be represented by a notation system $\vartheta(T)$, which is computable relative to $T$. The statement that $\vartheta(T)$ is well-founded for any dilator $T$ will still be equivalent to $Π^1_1$-comprehension. Thus the latter is split into the computable transformation $T\mapsto\vartheta(T)$ and a statement about the preservation of well-foundedness, over a system of computable mathematics.
△ Less
Submitted 5 August, 2020; v1 submitted 18 September, 2018;
originally announced September 2018.
-
A Categorical Construction of Bachmann-Howard Fixed Points
Authors:
Anton Freund
Abstract:
Peter Aczel has given a categorical construction for fixed points of normal functors, i.e. dilators which preserve initial segments. For a general dilator $X\mapsto T_X$ we cannot expect to obtain a well-founded fixed point, as the order type of $T_X$ may always exceed the order type of $X$. In the present paper we show how to construct a Bachmann-Howard fixed point of $T$, i.e. an order…
▽ More
Peter Aczel has given a categorical construction for fixed points of normal functors, i.e. dilators which preserve initial segments. For a general dilator $X\mapsto T_X$ we cannot expect to obtain a well-founded fixed point, as the order type of $T_X$ may always exceed the order type of $X$. In the present paper we show how to construct a Bachmann-Howard fixed point of $T$, i.e. an order $\operatorname{BH}(T)$ with an "almost" order preserving collapse $\vartheta:T_{\operatorname{BH}(T)}\rightarrow\operatorname{BH}(T)$. Building on previous work, we show that $Π^1_1$-comprehension is equivalent to the assertion that $\operatorname{BH}(T)$ is well-founded for any dilator $T$.
△ Less
Submitted 17 September, 2019; v1 submitted 18 September, 2018;
originally announced September 2018.
-
$Π^1_1$-Comprehension as a Well-Ordering Principle
Authors:
Anton Freund
Abstract:
A dilator is a particularly uniform transformation $X\mapsto T_X$ of linear orders that preserves well-foundedness. We say that $X$ is a Bachmann-Howard fixed point of $T$ if there is an almost order preserving collapsing function $\vartheta:T_X\rightarrow X$ (precise definition to follow). In the present paper we show that $Π^1_1$-comprehension is equivalent to the assertion that every dilator ha…
▽ More
A dilator is a particularly uniform transformation $X\mapsto T_X$ of linear orders that preserves well-foundedness. We say that $X$ is a Bachmann-Howard fixed point of $T$ if there is an almost order preserving collapsing function $\vartheta:T_X\rightarrow X$ (precise definition to follow). In the present paper we show that $Π^1_1$-comprehension is equivalent to the assertion that every dilator has a well-founded Bachmann-Howard fixed point. This proves a conjecture of M. Rathjen and A. Montalbán.
△ Less
Submitted 19 August, 2019; v1 submitted 18 September, 2018;
originally announced September 2018.
-
Density functional theory modeling of vortex shedding in superfluid He-4
Authors:
A. Freund,
D. Gonzalez,
X. Buelna,
F. Ancilotto,
J. Eloranta
Abstract:
Formation of vortex rings around moving spherical objects in superfluid He-4 at 0 K is modeled by time-dependent density functional theory. The simulations provide detailed information of the microscopic events that lead to vortex ring emission through characteristic observables such as liquid current circulation, drag force, and hydrodynamic mass. A series of simulations were performed to determi…
▽ More
Formation of vortex rings around moving spherical objects in superfluid He-4 at 0 K is modeled by time-dependent density functional theory. The simulations provide detailed information of the microscopic events that lead to vortex ring emission through characteristic observables such as liquid current circulation, drag force, and hydrodynamic mass. A series of simulations were performed to determine velocity thresholds for the onset of dissipation as a function of the sphere radius up to 1.8 nm and at external pressures of zero and 1 bar. The threshold was observed to decrease with the sphere radius and increase with pressure thus showing that the onset of dissipation does not involve roton emission events (Landau critical velocity), but rather vortex emission (Feynman critical velocity), which is also confirmed by the observed periodic response of the hydrodynamic observables as well as visualization of the liquid current circulation. An empirical model, which considers the ratio between the boundary layer kinetic and vortex ring formation energies, is presented for extrapolating the current results to larger length scales. The calculated critical velocity value at zero pressure for a sphere that mimics an electron bubble is in good agreement with the previous experimental observations at low temperatures. The stability of the system against symmetry breaking was linked to its ability to excite quantized Kelvin waves around the vortex rings during the vortex shedding process. At high vortex ring emission rates, the downstream dynamics showed complex vortex ring fission and reconnection events that appear similar to those seen in previous Gross-Pitaevskii theory-based calculations, and which mark the onset of turbulent behavior.
△ Less
Submitted 23 July, 2018;
originally announced July 2018.
-
Short Proofs for Slow Consistency
Authors:
Anton Freund,
Fedor Pakhomov
Abstract:
Let $\operatorname{Con}(\mathbf T)\!\restriction\!x$ denote the finite consistency statement "there are no proofs of contradiction in $\mathbf T$ with $\leq x$ symbols". For a large class of natural theories $\mathbf T$, Pudlák has shown that the lengths of the shortest proofs of $\operatorname{Con}(\mathbf T)\!\restriction\!n$ in the theory $\mathbf T$ itself are bounded by a polynomial in $n$. A…
▽ More
Let $\operatorname{Con}(\mathbf T)\!\restriction\!x$ denote the finite consistency statement "there are no proofs of contradiction in $\mathbf T$ with $\leq x$ symbols". For a large class of natural theories $\mathbf T$, Pudlák has shown that the lengths of the shortest proofs of $\operatorname{Con}(\mathbf T)\!\restriction\!n$ in the theory $\mathbf T$ itself are bounded by a polynomial in $n$. At the same time he conjectures that $\mathbf T$ does not have polynomial proofs of the finite consistency statements $\operatorname{Con}(\mathbf T+\operatorname{Con}(\mathbf T))\!\restriction\!n$. In contrast we show that Peano arithmetic ($\mathbf{PA}$) has polynomial proofs of $\operatorname{Con}(\mathbf{PA}+\operatorname{Con}^*(\mathbf{PA}))\!\restriction\!n$, where $\operatorname{Con}^*(\mathbf{PA})$ is the slow consistency statement for Peano arithmetic, introduced by S.-D. Friedman, Rathjen and Weiermann. We also obtain a new proof of the result that the usual consistency statement $\operatorname{Con}(\mathbf{PA})$ is equivalent to $\varepsilon_0$ iterations of slow consistency. Our argument is proof-theoretic, while previous investigations of slow consistency relied on non-standard models of arithmetic.
△ Less
Submitted 6 March, 2020; v1 submitted 8 December, 2017;
originally announced December 2017.
-
A Note on Iterated Consistency and Infinite Proofs
Authors:
Anton Freund
Abstract:
Schmerl and Beklemishev's work on iterated reflection achieves two aims: It introduces the important notion of $Π^0_1$-ordinal, characterizing the $Π^0_1$-theorems of a theory in terms of transfinite iterations of consistency; and it provides an innovative calculus to compute the $Π^0_1$-ordinals for a range of theories. The present note demonstrates that these achievements are independent: We rea…
▽ More
Schmerl and Beklemishev's work on iterated reflection achieves two aims: It introduces the important notion of $Π^0_1$-ordinal, characterizing the $Π^0_1$-theorems of a theory in terms of transfinite iterations of consistency; and it provides an innovative calculus to compute the $Π^0_1$-ordinals for a range of theories. The present note demonstrates that these achievements are independent: We read off $Π^0_1$-ordinals from a Schütte-style ordinal analysis via infinite proofs, in a direct and transparent way.
△ Less
Submitted 16 July, 2018; v1 submitted 5 September, 2017;
originally announced September 2017.
-
A Higher Bachmann-Howard Principle
Authors:
Anton Freund
Abstract:
We present a higher well-ordering principle which is equivalent (over Simpson's set theoretic version of $\text{ATR}_0$) to the existence of transitive models of Kripke-Platek set theory, and thus to $Π^1_1$-comprehension. This is a partial solution to a conjecture of Montalbán and Rathjen: partial in the sense that our well-ordering principle is less constructive than demanded in the conjecture.
We present a higher well-ordering principle which is equivalent (over Simpson's set theoretic version of $\text{ATR}_0$) to the existence of transitive models of Kripke-Platek set theory, and thus to $Π^1_1$-comprehension. This is a partial solution to a conjecture of Montalbán and Rathjen: partial in the sense that our well-ordering principle is less constructive than demanded in the conjecture.
△ Less
Submitted 19 September, 2018; v1 submitted 5 April, 2017;
originally announced April 2017.
-
Slow Reflection
Authors:
Anton Freund
Abstract:
We describe a "slow" version of the hierarchy of uniform reflection principles over Peano Arithmetic ($\mathbf{PA}$). These principles are unprovable in Peano Arithmetic (even when extended by usual reflection principles of lower complexity) and introduce a new provably total function. At the same time the consistency of $\mathbf{PA}$ plus slow reflection is provable in…
▽ More
We describe a "slow" version of the hierarchy of uniform reflection principles over Peano Arithmetic ($\mathbf{PA}$). These principles are unprovable in Peano Arithmetic (even when extended by usual reflection principles of lower complexity) and introduce a new provably total function. At the same time the consistency of $\mathbf{PA}$ plus slow reflection is provable in $\mathbf{PA}+\operatorname{Con}(\mathbf{PA})$. We deduce a conjecture of S.-D. Friedman, Rathjen and Weiermann: Transfinite iterations of slow consistency generate a hierarchy of precisely $\varepsilon_0$ stages between $\mathbf{PA}$ and $\mathbf{PA}+\operatorname{Con}(\mathbf{PA})$ (where $\operatorname{Con}(\mathbf{PA})$ refers to the usual consistency statement).
△ Less
Submitted 29 June, 2017; v1 submitted 29 January, 2016;
originally announced January 2016.
-
Proof Lengths for Instances of the Paris-Harrington Principle
Authors:
Anton Freund
Abstract:
As Paris and Harrington have famously shown, Peano Arithmetic does not prove that for all numbers $k,m,n$ there is an $N$ which satisfies the statement $\operatorname{PH}(k,m,n,N)$: For any $k$-colouring of its $n$-element subsets the set $\{0,\dots,N-1\}$ has a large homogeneous subset of size $\geq m$. At the same time very weak theories can establish the $Σ_1$-statement…
▽ More
As Paris and Harrington have famously shown, Peano Arithmetic does not prove that for all numbers $k,m,n$ there is an $N$ which satisfies the statement $\operatorname{PH}(k,m,n,N)$: For any $k$-colouring of its $n$-element subsets the set $\{0,\dots,N-1\}$ has a large homogeneous subset of size $\geq m$. At the same time very weak theories can establish the $Σ_1$-statement $\exists_N\operatorname{PH}(\overline k,\overline m,\overline n,N)$ for any fixed parameters $k,m,n$. Which theory, then, does it take to formalize natural proofs of these instances? It is known that $\forall_m\exists_N\operatorname{PH}(\overline k,m,\overline n,N)$ has a natural and short proof (relative to $n$ and $k$) by $Σ_{n-1}$-induction. In contrast, we show that there is an elementary function $e$ such that any proof of $\exists_N\operatorname{PH}(\overline{e(n)},\overline{n+1},\overline n,N)$ by $Σ_{n-2}$-induction is ridiculously long. In order to establish this result on proof lengths we give a computational analysis of slow provability, a notion introduced by Sy-David Friedman, Rathjen and Weiermann. We will see that slow uniform $Σ_1$-reflection is related to a function that has a considerably lower growth rate than $F_{\varepsilon_0}$ but dominates all functions $F_α$ with $α<\varepsilon_0$ in the fast-growing hierarchy.
△ Less
Submitted 13 January, 2017; v1 submitted 29 January, 2016;
originally announced January 2016.
-
A Uniform Characterization of $Σ_1$-Reflection over the Fragments of Peano Arithmetic
Authors:
Anton Freund
Abstract:
We show that the theory $IΣ_1$ of $Σ_1$-induction proves the following statement: For all $n\geq 2$, the uniform $Σ_1$-reflection principle over the theory $IΣ_n$ is equivalent to the totality of the function $F_{ω_n}$ at stage $ω_n$ of the fast-growing hierarchy. The method applied is a formalization of infinite proof theory. The literature contains several proofs which place the quantification o…
▽ More
We show that the theory $IΣ_1$ of $Σ_1$-induction proves the following statement: For all $n\geq 2$, the uniform $Σ_1$-reflection principle over the theory $IΣ_n$ is equivalent to the totality of the function $F_{ω_n}$ at stage $ω_n$ of the fast-growing hierarchy. The method applied is a formalization of infinite proof theory. The literature contains several proofs which place the quantification over $n$ in the meta-theory (and also prove the separate cases $n=0,1$). In contrast, the author knows of no explicit argument that would allow us to internalize the quantification while kee** the meta-theory as low as $IΣ_1$. It is well possible that this has been considered before. Our aim is merely to provide a detailed exposition of this important result.
△ Less
Submitted 16 December, 2015;
originally announced December 2015.
-
Coherent bremsstrahlung, boherent pair production, birefringence and polarimetry in the 20-170 GeV energy range using aligned crystals
Authors:
NA59 Collaboration,
A. Apyan,
R. O. Avakian,
B. Badelek,
S. Ballestrero,
C. Biino,
I. Birol,
P. Cenci,
S. H. Connell,
S. Eichblatt,
T. Fonseca,
A. Freund,
B. Gorini,
R. Groess,
K. Ispirian,
T. J. Ketel,
Yu. V. Kononets,
A. Lopez,
A. Mangiarotti,
B. van Rens,
J. P. F. Sellschop,
M. Shieh,
P. Sona,
V. Strakhovenko,
E. Uggerhoj
, et al. (5 additional authors not shown)
Abstract:
The processes of coherent bremsstrahlung (CB) and coherent pair production (CPP) based on aligned crystal targets have been studied in the energy range 20-170 GeV. The experimental arrangement allowed for measurements of single photon properties of these phenomena including their polarization dependences. This is significant as the theoretical description of CB and CPP is an area of active theor…
▽ More
The processes of coherent bremsstrahlung (CB) and coherent pair production (CPP) based on aligned crystal targets have been studied in the energy range 20-170 GeV. The experimental arrangement allowed for measurements of single photon properties of these phenomena including their polarization dependences. This is significant as the theoretical description of CB and CPP is an area of active theoretical debate and development. With the theoretical approach used in this paper both the measured cross sections and polarization observables are predicted very well. This indicates a proper understanding of CB and CPP up to energies of 170 GeV. Birefringence in CPP on aligned crystals is applied to determine the polarization parameters in our measurements. New technologies for high energy photon beam optics including phase plates and polarimeters for linear and circular polarization are demonstrated in this experiment. Coherent bremsstrahlung for the strings-on-strings (SOS) orientation yields a larger enhancement for hard photons than CB for the channeling orientations of the crystal. Our measurements and our calculations indicate low photon polarizations for the high energy SOS photons.
△ Less
Submitted 26 February, 2008; v1 submitted 7 December, 2005;
originally announced December 2005.
-
Results on the Coherent Interaction of High Energy Electrons and Photons in Oriented Single Crystals
Authors:
NA59 Collaboration,
A. Apyan,
R. O. Avakian,
B. Badelek,
S. Ballestrero,
C. Biino,
I. Birol,
P. Cenci,
S. H. Connell,
S. Eichblatt,
T. Fonseca,
A. Freund,
B. Gorini,
R. Groess,
K. Ispirian,
T. J. Ketel,
Yu. V. Kononets,
A. Lopez,
A. Mangiarotti,
B. van Rens,
J. P. F. Sellschop,
M. Shieh,
P. Sona,
V. Strakhovenko,
E. Uggerhoj
, et al. (5 additional authors not shown)
Abstract:
The CERN-NA-59 experiment examined a wide range of electromagnetic processes for multi-GeV electrons and photons interacting with oriented single crystals. The various types of crystals and their orientations were used for producing photon beams and for converting and measuring their polarisation.
The radiation emitted by 178 GeV unpolarised electrons incident on a 1.5 cm thick Si crystal orie…
▽ More
The CERN-NA-59 experiment examined a wide range of electromagnetic processes for multi-GeV electrons and photons interacting with oriented single crystals. The various types of crystals and their orientations were used for producing photon beams and for converting and measuring their polarisation.
The radiation emitted by 178 GeV unpolarised electrons incident on a 1.5 cm thick Si crystal oriented in the Coherent Bremsstrahlung (CB) and the String-of-Strings (SOS) modes was used to obtain multi-GeV linearly polarised photon beams.
A new crystal polarimetry technique was established for measuring the linear polarisation of the photon beam. The polarimeter is based on the dependence of the Coherent Pair Production (CPP) cross section in oriented single crystals on the direction of the photon polarisation with respect to the crystal plane. Both a 1 mm thick single crystal of Germanium and a 4 mm thick multi-tile set of synthetic Diamond crystals were used as analyzers of the linear polarisation.
A birefringence phenomenon, the conversion of the linear polarisation of the photon beam into circular polarisation, was observed. This was achieved by letting the linearly polarised photon beam pass through a 10 cm thick Silicon single crystal that acted as a "quarter wave plate" (QWP) as suggested by N. Cabibbo et al.
△ Less
Submitted 22 June, 2005;
originally announced June 2005.
-
Measurement of Coherent Emission and Linear Polarization of Photons by Electrons in the Strong Fields of Aligned Crystals
Authors:
NA59 Collaboration,
A. Apyan,
R. O. Avakian,
B. Badelek,
S. Ballestrero,
C. Biino,
I. Birol,
P. Cenci,
S. H. Connell,
S. Eichblatt,
T. Fonseca,
A. Freund,
B. Gorini,
R. Groess,
K. Ispirian,
T. J. Ketel,
Yu. V. Kononets,
A. Lopez,
A. Mangiarotti,
B. van Rens,
J. P. F. Sellschop,
M. Shieh,
P. Sona,
V. Strakhovenko,
E. Uggerhoj
, et al. (5 additional authors not shown)
Abstract:
We present new results regarding the features of high energy photon emission by an electron beam of 178 GeV penetrating a 1.5 cm thick single Si crystal aligned at the Strings-Of-Strings (SOS) orientation. This concerns a special case of coherent bremsstrahlung where the electron interacts with the strong fields of successive atomic strings in a plane and for which the largest enhancement of the…
▽ More
We present new results regarding the features of high energy photon emission by an electron beam of 178 GeV penetrating a 1.5 cm thick single Si crystal aligned at the Strings-Of-Strings (SOS) orientation. This concerns a special case of coherent bremsstrahlung where the electron interacts with the strong fields of successive atomic strings in a plane and for which the largest enhancement of the highest energy photons is expected. The polarization of the resulting photon beam was measured by the asymmetry of electron-positron pair production in an aligned diamond crystal analyzer. By the selection of a single pair the energy and the polarization of individual photons could be measured in an the environment of multiple photons produced in the radiator crystal. Photons in the high energy region show less than 20% linear polarization at the 90% confidence level.
△ Less
Submitted 24 June, 2004; v1 submitted 9 June, 2004;
originally announced June 2004.
-
DVCS on nuclei: Observability and Consequences
Authors:
A. Freund,
M. Strikman
Abstract:
In this paper, we discuss the feasibility of measuring deeply virtual Compton scattering (DVCS) on nuclei in a collider setting, as for example, the planned high-luminosity Electron-Ion-Collider (EIC). We demonstrate that employing our recent model for nuclear generalized parton distributions (nGPDs), the one-photon unpolarized DVCS cross section as well as the azimuthal- and spin asymmetry are…
▽ More
In this paper, we discuss the feasibility of measuring deeply virtual Compton scattering (DVCS) on nuclei in a collider setting, as for example, the planned high-luminosity Electron-Ion-Collider (EIC). We demonstrate that employing our recent model for nuclear generalized parton distributions (nGPDs), the one-photon unpolarized DVCS cross section as well as the azimuthal- and spin asymmetry are of the same size as in the proton case. This will allow for an experimental extraction of nuclear GPDs with high precision shedding new light on nuclear shadowing at small $x_{bj}$ and the interplay of shadowing and nuclear enhancement at $x_{bj}~0.1$.
△ Less
Submitted 28 November, 2003; v1 submitted 8 September, 2003;
originally announced September 2003.
-
Nuclear effects and their interplay in nuclear DVCS amplitudes
Authors:
A. Freund,
M. Strikman
Abstract:
In this paper we analyze nuclear medium effects on DVCS amplitudes in the $\Bx$ range of $0.1-0.0001$ for a large range of $Q^2$ and four different nuclei. We use our nucleon GPD model capable of describing all currently available DVCS data on the proton and extend it to the nuclear case using two competing parameterizations of nuclear effects. The two parameterizations, though giving different…
▽ More
In this paper we analyze nuclear medium effects on DVCS amplitudes in the $\Bx$ range of $0.1-0.0001$ for a large range of $Q^2$ and four different nuclei. We use our nucleon GPD model capable of describing all currently available DVCS data on the proton and extend it to the nuclear case using two competing parameterizations of nuclear effects. The two parameterizations, though giving different absolute numbers, yield the same type and magnitude of effects for the imaginary and real part of the nuclear DVCS amplitude. The imaginary part shows stronger nuclear shadowing effects compared to the inclusive case i.e. $F^N_2$, whereas in the real part nuclear shadowing at small $\Bx$ and anti-shadowing at large $\Bx$ combine through evolution to yield an even greater suppression than in the imaginary part up to large values of $\Bx$. This is the first time that such a combination of nuclear effects has been observed in a hadronic amplitude. The experimental implications will be discussed in a subsequent publication.
△ Less
Submitted 28 November, 2003; v1 submitted 16 July, 2003;
originally announced July 2003.
-
A detailed QCD analysis of twist-3 effects in DVCS observables
Authors:
A. Freund
Abstract:
In this paper I present a detailed QCD analysis of twist-3 effects in the Wandzura-Wilczek (WW) approximation in deeply virtual Compton scattering (DVCS) observables for various kinematical settings, representing the HERA, HERMES, CLAS and the planned EIC (electron-ion-collider) experiments. I find that the twist-3 effects in the WW approximation are almost always negligible at collider energies…
▽ More
In this paper I present a detailed QCD analysis of twist-3 effects in the Wandzura-Wilczek (WW) approximation in deeply virtual Compton scattering (DVCS) observables for various kinematical settings, representing the HERA, HERMES, CLAS and the planned EIC (electron-ion-collider) experiments. I find that the twist-3 effects in the WW approximation are almost always negligible at collider energies but can be large for low Q^2 and smaller x_bj in observables for the lower energy, fixed target experiments directly sensitive to the real part of DVCS amplitudes like the charge asymmetry (CA). Conclusions are then drawn about the reliability of extracting twist-2 generalized parton distributions (GPDs) from experimental data and a first, phenomenological, parameterization of the LO and NLO twist-2 GPD $H$, describing all the currently available DVCS data within the experimental errors is given.
△ Less
Submitted 14 October, 2003; v1 submitted 2 June, 2003;
originally announced June 2003.
-
Linear to Circular Polarisation Conversion using Birefringent Properties of Aligned Crystals for Multi-GeV Photons
Authors:
NA59 Collaboration,
A. Apyan,
R. O. Avakian,
B. Badelek,
S. Ballestrero,
C. Biino,
I. Birol,
P. Cenci,
S. H. Connell,
S. Eichblatt,
T. Fonseca,
A. Freund,
B. Gorini,
R. Groess,
K. Ispirian,
T. J. Ketel,
Yu. V. Kononets,
A. Lopez,
A. Mangiarotti,
B. van Rens,
J. P. F. Sellschop,
M. Shieh,
P. Sona,
V. Strakhovenko,
E. Uggerhoj
, et al. (5 additional authors not shown)
Abstract:
We present the first experimental results on the use of a thick aligned Si crystal acting as a quarter wave plate to induce a degree of circular polarisation in a high energy linearly polarised photon beam. The linearly polarised photon beam is produced from coherent bremsstrahlung radiation by 178 GeV unpolarised electrons incident on an aligned Si crystal, acting as a radiator. The linear pola…
▽ More
We present the first experimental results on the use of a thick aligned Si crystal acting as a quarter wave plate to induce a degree of circular polarisation in a high energy linearly polarised photon beam. The linearly polarised photon beam is produced from coherent bremsstrahlung radiation by 178 GeV unpolarised electrons incident on an aligned Si crystal, acting as a radiator. The linear polarisation of the photon beam is characterised by measuring the asymmetry in electron-positron pair production in a Ge crystal, for different crystal orientations. The Ge crystal therefore acts as an analyser. The birefringence phenomenon, which converts the linear polarisation to circular polarisation, is observed by letting the linearly polarised photons beam pass through a thick Si quarter wave plate crystal, and then measuring the asymmetry in electron-positron pair production again for a selection of relative angles between the crystallographic planes of the radiator, analyser and quarter wave plate. The systematics of the difference between the measured asymmetries with and without the quarter wave plate are predicted by theory to reveal an evolution in the Stokes parameters from which the appearance of a circularly polarised component in the photon beam can be demonstrated. The measured magnitude of the circularly polarised component was consistent with the theoretical predictions, and therefore is in indication of the existence of the birefringence effect.
△ Less
Submitted 24 June, 2004; v1 submitted 18 June, 2003;
originally announced June 2003.
-
Coherent Pair Production by Photons in the 20-170 GeV Energy Range Incident on Crystals and Birefringence
Authors:
NA59 Collaboration,
A. Apyan,
R. O. Avakian,
B. Badelek,
S. Ballestrero,
C. Biino,
I. Birol,
P. Cenci,
S. H. Connell,
S. Eichblatt,
T. Fonseca,
A. Freund,
B. Gorini,
R. Groess,
K. Ispirian,
T. J. Ketel,
Yu. V. Kononets,
A. Lopez,
A. Mangiarotti,
B. van Rens,
J. P. F. Sellschop,
M. Shieh,
P. Sona,
V. Strakhovenko,
E. Uggerhoj
, et al. (5 additional authors not shown)
Abstract:
The cross section for coherent pair production by linearly polarised photons in the 20-170 GeV energy range was measured for photon aligned incidence on ultra-high quality diamond and germanium crystals. The theoretical description of coherent bremsstrahlung and coherent pair production phenomena is an area of active theoretical debate and development. However, under our experimental conditions,…
▽ More
The cross section for coherent pair production by linearly polarised photons in the 20-170 GeV energy range was measured for photon aligned incidence on ultra-high quality diamond and germanium crystals. The theoretical description of coherent bremsstrahlung and coherent pair production phenomena is an area of active theoretical debate and development. However, under our experimental conditions, the theory predicted the combined cross section and polarisation experimental observables very well indeed. In macroscopic terms, our experiment measured a birefringence effect in pair production in a crystal. This study of this effect also constituted a measurement of the energy dependent linear polarisation of photons produced by coherent bremsstrahlung in aligned crystals. New technologies for manipulating high energy photon beams can be realised based on an improved understanding of QED phenomena at these energies. In particular, this experiment demonstrates an efficient new polarimetry technique. The pair production measurements were done using two independent methods simultaneously. The more complex method using a magnet spectrometer showed that the simpler method using a multiplicity detector was also viable.
△ Less
Submitted 24 June, 2004; v1 submitted 11 June, 2003;
originally announced June 2003.
-
Demystifying generalized parton distributions
Authors:
A. Freund
Abstract:
In this paper, I will explain in as simple and intuitive physical terms as possible what generalized parton distributions are, what new information about the structure of hadrons they convey and therefore what picture of the hadron will emerge. To develop this picture, I will use the example of deeply virtual Compton scattering (DVCS) and exclusive meson electroproduction processes. Based on thi…
▽ More
In this paper, I will explain in as simple and intuitive physical terms as possible what generalized parton distributions are, what new information about the structure of hadrons they convey and therefore what picture of the hadron will emerge. To develop this picture, I will use the example of deeply virtual Compton scattering (DVCS) and exclusive meson electroproduction processes. Based on this picture, I will make some general predictions for these processes.
△ Less
Submitted 20 August, 2003; v1 submitted 2 December, 2002;
originally announced December 2002.
