-
Optimal Image Transport on Sparse Dictionaries
Authors:
Junqing Huang,
Haihui Wang,
Andreas Weiermann,
Michael Ruzhansky
Abstract:
In this paper, we derive a novel optimal image transport algorithm over sparse dictionaries by taking advantage of Sparse Representation (SR) and Optimal Transport (OT). Concisely, we design a unified optimization framework in which the individual image features (color, textures, styles, etc.) are encoded using sparse representation compactly, and an optimal transport plan is then inferred between…
▽ More
In this paper, we derive a novel optimal image transport algorithm over sparse dictionaries by taking advantage of Sparse Representation (SR) and Optimal Transport (OT). Concisely, we design a unified optimization framework in which the individual image features (color, textures, styles, etc.) are encoded using sparse representation compactly, and an optimal transport plan is then inferred between two learned dictionaries in accordance with the encoding process. This paradigm gives rise to a simple but effective way for simultaneous image representation and transformation, which is also empirically solvable because of the moderate size of sparse coding and optimal transport sub-problems. We demonstrate its versatility and many benefits to different image-to-image translation tasks, in particular image color transform and artistic style transfer, and show the plausible results for photo-realistic transferred effects.
△ Less
Submitted 3 November, 2023;
originally announced November 2023.
-
Fundamental sequences and fast-growing hierarchies for the Bachmann-Howard ordinal
Authors:
David Fernández-Duque,
Andreas Weiermann
Abstract:
We prove that Buchholz's system of fundamental sequences for the $\vartheta$ function enjoys various regularity conditions, including the Bachmann property. We partially extend these results to variants of the $\vartheta$ function, including a version without addition for countable ordinals. We conclude that the Hardy functions based on these notation systems enjoy natural monotonicity properties…
▽ More
We prove that Buchholz's system of fundamental sequences for the $\vartheta$ function enjoys various regularity conditions, including the Bachmann property. We partially extend these results to variants of the $\vartheta$ function, including a version without addition for countable ordinals. We conclude that the Hardy functions based on these notation systems enjoy natural monotonicity properties and majorize all functions defined by primitive recursion along $\vartheta(\varepsilon_{Ω+1})$.
△ Less
Submitted 4 January, 2024; v1 submitted 15 March, 2022;
originally announced March 2022.
-
Functorial Fast-Growing Hierarchies
Authors:
J. P. Aguilera,
F. Pakhomov,
A. Weiermann
Abstract:
Fast-growing hierarchies are sequences of functions obtained through various processes similar to the ones that yield multiplication from addition, exponentiation from multiplication, etc. We observe that fast-growing hierarchies can be naturally extended to functors on the categories of natural numbers and of linear orders. We show that the categorical extensions of binary fast-growing hierarchie…
▽ More
Fast-growing hierarchies are sequences of functions obtained through various processes similar to the ones that yield multiplication from addition, exponentiation from multiplication, etc. We observe that fast-growing hierarchies can be naturally extended to functors on the categories of natural numbers and of linear orders. We show that the categorical extensions of binary fast-growing hierarchies to ordinals are isomorphic to denotation systems given by ordinal collapsing functions, thus establishing a connection between two fundamental concepts in Proof Theory.
Using this fact, we obtain a restatement of the subsystem $Π^1_1$-CA$_0$ of analysis as a higher-type wellordering principle.
△ Less
Submitted 12 January, 2022;
originally announced January 2022.
-
Arithmetical and Hyperarithmetical Worm Battles
Authors:
David Fernández-Duque,
Joost J. Joosten,
Fedor Pakhomov,
Konstnatinos Papafilippou,
Andreas Weiermann
Abstract:
Japaridze's provability logic $GLP$ has one modality $[n]$ for each natural number and has been used by Beklemishev for a proof theoretic analysis of Peano aritmetic $(PA)$ and related theories. Among other benefits, this analysis yields the so-called Every Worm Dies $(EWD)$ principle, a natural combinatorial statement independent of $PA$. Recently, Beklemishev and Pakhomov have studied notions of…
▽ More
Japaridze's provability logic $GLP$ has one modality $[n]$ for each natural number and has been used by Beklemishev for a proof theoretic analysis of Peano aritmetic $(PA)$ and related theories. Among other benefits, this analysis yields the so-called Every Worm Dies $(EWD)$ principle, a natural combinatorial statement independent of $PA$. Recently, Beklemishev and Pakhomov have studied notions of provability corresponding to transfinite modalities in $GLP$. We show that indeed the natural transfinite extension of $GLP$ is sound for this interpretation, and yields independent combinatorial principles for the second order theory $ACA$ of arithmetical comprehension with full induction. We also provide restricted versions of $EWD$ related to the fragments $IΣ_n$ of Peano arithmetic. In order to prove the latter, we show that standard Hardy functions majorize their variants based on tree ordinals.
△ Less
Submitted 29 June, 2022; v1 submitted 14 December, 2021;
originally announced December 2021.
-
Fast Goodstein Walks
Authors:
David Fernández-Duque,
Andreas Weiermann
Abstract:
We define a variant of the Goodstein process based on fast-growing functions and show that it terminates, but this fact is not provable in Kripke-Platek set theory or other theories of strength the Bachmann-Howard ordinal. We moreover show that this Goodstein process is of maximal length, so that any alternative Goodstein process based on the same fast-growing functions will also terminate.
We define a variant of the Goodstein process based on fast-growing functions and show that it terminates, but this fact is not provable in Kripke-Platek set theory or other theories of strength the Bachmann-Howard ordinal. We moreover show that this Goodstein process is of maximal length, so that any alternative Goodstein process based on the same fast-growing functions will also terminate.
△ Less
Submitted 14 May, 2022; v1 submitted 30 November, 2021;
originally announced November 2021.
-
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.
-
Monadic second order limit laws for natural well orderings
Authors:
Andreas Weiermann
Abstract:
By combining classical results of Büchi, some elementary Tauberian theorems and some basic tools from logic and combinatorics we show that every ordinal $α$ with $\varepsilon_0\geq α\geq ω^ω$ satisfies a natural monadic second order limit law and that every ordinal $α$ with $ω^ω>α\geq ω$ satisfies a natural monadic second order Cesaro limit law. In both cases we identify as usual $α$ with the clas…
▽ More
By combining classical results of Büchi, some elementary Tauberian theorems and some basic tools from logic and combinatorics we show that every ordinal $α$ with $\varepsilon_0\geq α\geq ω^ω$ satisfies a natural monadic second order limit law and that every ordinal $α$ with $ω^ω>α\geq ω$ satisfies a natural monadic second order Cesaro limit law. In both cases we identify as usual $α$ with the class of substructures $\{β:β<α\}$.
We work in an additive setting where the norm function $N$ assigns to every ordinal $α$ the number of occurrrences of the symbol $ω$ in its Cantor normal form. This number is the same as the number of edges in the tree which is canonically associated with $α$.
For a given $α$ with $ω\leq α\leq \varepsilon_0$ the asymptotic probability of a monadic second order formula $\varphi$ from the language of linear orders is $\lim_{n\to\infty} \frac{\#\{β<α: Nβ=n\wedge β\models Φ\}}{\#\{β<α: Nβ=n\}}$ if this limit exists. If this limit exists only in the Cesaro sense we speak of the Cesaro asympotic probability of $\varphi$.
Moreover we prove monadic second order limit laws for the ordinal segments below below $Γ_0$ (where the norm function is extended appropriately) and we indicate how this paper's results can be extended to larger ordinal segments and even to certain impredicative ordinal notation systems having notations for uncountable ordinals. We also briefly indicate how to prove the corresponding multiplicative results for which the setting is defined relative to the Matula coding.
The results of this paper concerning ordinals not exceeding $\varepsilon_0$ have been obtained partly in joint work with Alan R. Woods.
△ Less
Submitted 28 July, 2020;
originally announced July 2020.
-
Giant and illusionary giant Goodstein principles
Authors:
Andreas Weiermann
Abstract:
We analyze several natural Goodstein principles which themselves are defined with respect to the Ackermann function and the extended Ackermann function. These Ackermann functions are well established canonical fast growing functions labeled by ordinals not exceeding $\varepsilon_0$. Among the Goodsteinprinciples under consideration, the giant ones, will be proof-theoretically strong (being unprova…
▽ More
We analyze several natural Goodstein principles which themselves are defined with respect to the Ackermann function and the extended Ackermann function. These Ackermann functions are well established canonical fast growing functions labeled by ordinals not exceeding $\varepsilon_0$. Among the Goodsteinprinciples under consideration, the giant ones, will be proof-theoretically strong (being unprovable in $\mathrm{PA}$ in the Ackermannian case and being unprovable in $\mathrm{ID}_1$ in the extended Ackermannian case) whereas others, the illusionary giant ones, will turn out to be comparatively much much weaker although they look strong at first sight.
△ Less
Submitted 17 July, 2020;
originally announced July 2020.
-
Intermediate Goodstein principles
Authors:
David Fernández-Duque,
Oriola Gjetaj,
Andreas Weiermann
Abstract:
The original Goodstein process proceeds by writing natural numbers in nested exponential $k$-normal form, then successively raising the base to $k+1$ and subtracting one from the end result. Such sequences always reach zero, but this fact is unprovable in Peano arithmetic. In this paper we instead consider notations for natural numbers based on the Ackermann function. We define three new Goodstein…
▽ More
The original Goodstein process proceeds by writing natural numbers in nested exponential $k$-normal form, then successively raising the base to $k+1$ and subtracting one from the end result. Such sequences always reach zero, but this fact is unprovable in Peano arithmetic. In this paper we instead consider notations for natural numbers based on the Ackermann function. We define three new Goodstein processes, obtaining new independence results for $ {\sf ACA}_0$, ${\sf ACA}_0'$ and ${\sf ACA}_0^+$, theories of second order arithmetic related to the existence of Turing jumps.
△ Less
Submitted 12 April, 2022; v1 submitted 20 April, 2020;
originally announced April 2020.
-
A walk with Goodstein
Authors:
David Fernández-Duque,
Andreas Weiermann
Abstract:
Goodstein's principle is arguably the first purely number-theoretic statement known to be independent of Peano arithmetic. It involves sequences of natural numbers which at first appear to grow very quickly, but eventually decrease to zero. These sequences are defined relative to a notation system based on exponentiation for the natural numbers. In this article, we explore notions of optimality fo…
▽ More
Goodstein's principle is arguably the first purely number-theoretic statement known to be independent of Peano arithmetic. It involves sequences of natural numbers which at first appear to grow very quickly, but eventually decrease to zero. These sequences are defined relative to a notation system based on exponentiation for the natural numbers. In this article, we explore notions of optimality for such notation systems and apply them to the classical Goodstein process, to a weaker variant based on multiplication rather than exponentiation, and to a stronger variant based on the Ackermann function. In particular, we introduce the notion of base-change maximality, and show how it leads to far-reaching extensions of Goodstein's result.
△ Less
Submitted 8 January, 2024; v1 submitted 20 April, 2020;
originally announced April 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.
-
Maximum linearizations of lower sets in $\mathbb{N}^m$ with application to monomial ideals
Authors:
Harry Altman,
Andreas Weiermann
Abstract:
We compute the type (maximum linearization) of the well partial order of bounded lower sets in $\mathbb{N}^m$, ordered under inclusion, and find it is $ω^{ω^{m-1}}$. Moreover we compute the type of the set of all lower sets in $\mathbb{N}^m$, a topic studied by Aschenbrenner and Pong, and find that it is equal to \[ ω^{\sum_{k=1}^{m} ω^{m-k}\binom{m}{k-1} }+ 1. \] As a consequence we deduce corres…
▽ More
We compute the type (maximum linearization) of the well partial order of bounded lower sets in $\mathbb{N}^m$, ordered under inclusion, and find it is $ω^{ω^{m-1}}$. Moreover we compute the type of the set of all lower sets in $\mathbb{N}^m$, a topic studied by Aschenbrenner and Pong, and find that it is equal to \[ ω^{\sum_{k=1}^{m} ω^{m-k}\binom{m}{k-1} }+ 1. \] As a consequence we deduce corresponding bounds on effectively given sequences of monomial ideals in $F[X,Y]$ where $F$ is a field.
△ Less
Submitted 25 January, 2024; v1 submitted 14 September, 2019;
originally announced September 2019.
-
Predicatively unprovable termination of the Ackermannian Goodstein process
Authors:
Toshiyasu Arai,
David Fernández-Duque,
Stanley Wainer,
Andreas Weiermann
Abstract:
The classical Goodstein process gives rise to long but finite sequences of natural numbers whose termination is not provable in Peano arithmetic. In this manuscript we consider a variant based on the Ackermann function. We show that Ackermannian Goodstein sequences eventually terminate, but this fact is not provable using predicative means.
The classical Goodstein process gives rise to long but finite sequences of natural numbers whose termination is not provable in Peano arithmetic. In this manuscript we consider a variant based on the Ackermann function. We show that Ackermannian Goodstein sequences eventually terminate, but this fact is not provable using predicative means.
△ Less
Submitted 31 May, 2019;
originally announced June 2019.
-
Ordinal notation systems corresponding to Friedman's linearized well-partial-orders with gap-condition
Authors:
Michael Rathjen,
Jeroen Van der Meeren,
Andreas Weiermann
Abstract:
In this article we investigate whether the addition-free theta functions form a canonical notation system for the linear versions of Friedman's well-partial-orders with the so-called gap-condition over a finite set of labels. Rather surprisingly, we can show this is the case for two labels, but not for more than two labels. To this end, we determine the order type of the notation systems for addit…
▽ More
In this article we investigate whether the addition-free theta functions form a canonical notation system for the linear versions of Friedman's well-partial-orders with the so-called gap-condition over a finite set of labels. Rather surprisingly, we can show this is the case for two labels, but not for more than two labels. To this end, we determine the order type of the notation systems for addition-free theta functions in terms of ordinals less than $\varepsilon_0$. We further show that the maximal order type of the Friedman ordering can be obtained by a certain ordinal notation system which is based on specific binary theta functions.
△ Less
Submitted 6 May, 2015;
originally announced May 2015.
-
An order-theoretic characterization of the Howard-Bachmann-hierarchy
Authors:
Jeroen Van der Meeren,
Michael Rathjen,
Andreas Weiermann
Abstract:
In this article we provide an intrinsic characterization of the famous Howard-Bachmann ordinal in terms of a natural well-partial-ordering by showing that this ordinal can be realized as a maximal order type of a class of generalized trees with respect to a homeomorphic embeddability relation. We use our calculations to draw some conclusions about some corresponding subsystems of second order arit…
▽ More
In this article we provide an intrinsic characterization of the famous Howard-Bachmann ordinal in terms of a natural well-partial-ordering by showing that this ordinal can be realized as a maximal order type of a class of generalized trees with respect to a homeomorphic embeddability relation. We use our calculations to draw some conclusions about some corresponding subsystems of second order arithmetic. All these subsystems deal with versions of light-face $Π^1_1$-comprehension
△ Less
Submitted 5 January, 2015; v1 submitted 17 November, 2014;
originally announced November 2014.
-
Asymptotic distribution of integers with certain prime factorizations
Authors:
Hans Vernaeve,
Jasson Vindas,
Andreas Weiermann
Abstract:
Let $p_{1}<p_2<... <p_ν<...$ be the sequence of prime numbers and let $m$ be a positive integer. We give a strong asymptotic formula for the distribution of the set of integers having prime factorizations of the form $p_{m^{k_1}}p_{m^{k_{2}}...p_{m^{k_{n}}}$ with $k_{1}\le k_{2}\le...\le k_{n}$. Such integers originate in various combinatorial counting problems; when $m=2$, they arise as Matula nu…
▽ More
Let $p_{1}<p_2<... <p_ν<...$ be the sequence of prime numbers and let $m$ be a positive integer. We give a strong asymptotic formula for the distribution of the set of integers having prime factorizations of the form $p_{m^{k_1}}p_{m^{k_{2}}...p_{m^{k_{n}}}$ with $k_{1}\le k_{2}\le...\le k_{n}$. Such integers originate in various combinatorial counting problems; when $m=2$, they arise as Matula numbers of certain rooted trees.
△ Less
Submitted 9 November, 2013; v1 submitted 11 March, 2013;
originally announced March 2013.
-
A Simplified Characterisation of Provably Computable Functions of the System ID_1 of Inductive Definitions
Authors:
Naohi Eguchi,
Andreas Weiermann
Abstract:
We present a simplified and streamlined characterisation of provably total computable functions of the theory ID_1 of non-iterated inductive definitions. The idea of the simplification is to employ the method of operator-controlled derivations that was originally introduced by Wilfried Buchholz and afterwards applied by the second author to a characterisation of provably total computable functions…
▽ More
We present a simplified and streamlined characterisation of provably total computable functions of the theory ID_1 of non-iterated inductive definitions. The idea of the simplification is to employ the method of operator-controlled derivations that was originally introduced by Wilfried Buchholz and afterwards applied by the second author to a characterisation of provably total computable functions of Peano arithmetic PA.
△ Less
Submitted 13 May, 2012;
originally announced May 2012.
-
Derivation Lengths Classification of Gödel's T Extending Howard's Assignment
Authors:
Gunnar Wilken,
Andreas Weiermann
Abstract:
Let T be Goedel's system of primitive recursive functionals of finite type in the lambda formulation. We define by constructive means using recursion on nested multisets a multivalued function I from the set of terms of T into the set of natural numbers such that if a term a reduces to a term b and if a natural number I(a) is assigned to a then a natural number I(b) can be assigned to b such that…
▽ More
Let T be Goedel's system of primitive recursive functionals of finite type in the lambda formulation. We define by constructive means using recursion on nested multisets a multivalued function I from the set of terms of T into the set of natural numbers such that if a term a reduces to a term b and if a natural number I(a) is assigned to a then a natural number I(b) can be assigned to b such that I(a) is greater than I(b). The construction of I is based on Howard's 1970 ordinal assignment for T and Weiermann's 1996 treatment of T in the combinatory logic version. As a corollary we obtain an optimal derivation length classification for the lambda formulation of T and its fragments. Compared with Weiermann's 1996 exposition this article yields solutions to several non-trivial problems arising from dealing with lambda terms instead of combinatory logic terms. It is expected that the methods developed here can be applied to other higher order rewrite systems resulting in new powerful termination orderings since T is a paradigm for such systems.
△ Less
Submitted 3 March, 2012; v1 submitted 1 March, 2012;
originally announced March 2012.
-
Partitioning $α$-large sets for $α<\varepsilon_ω$
Authors:
Michiel De Smet,
Andreas Weiermann
Abstract:
We generalise the results by Bigorajska and Kotlarski about partitioning $α$-large sets, by extending the domain up to ordinals below $\varepsilon_ω$. These results will be very useful to give a miniaturisation of the infinite Ramsey Theorem.
We generalise the results by Bigorajska and Kotlarski about partitioning $α$-large sets, by extending the domain up to ordinals below $\varepsilon_ω$. These results will be very useful to give a miniaturisation of the infinite Ramsey Theorem.
△ Less
Submitted 14 January, 2010;
originally announced January 2010.
-
Unprovability results involving braids
Authors:
Lorenzo Carlucci,
Patrick Dehornoy,
Andreas Weiermann
Abstract:
We construct long sequences of braids that are descending with respect to the standard order of braids (``Dehornoy order''), and we deduce that, contrary to all usual algebraic properties of braids, certain simple combinatorial statements involving the braid order are true, but not provable in the subsystems ISigma1 or ISigma2 of the standard Peano system.
We construct long sequences of braids that are descending with respect to the standard order of braids (``Dehornoy order''), and we deduce that, contrary to all usual algebraic properties of braids, certain simple combinatorial statements involving the braid order are true, but not provable in the subsystems ISigma1 or ISigma2 of the standard Peano system.
△ Less
Submitted 23 November, 2007;
originally announced November 2007.
