Related papers: Dilators and the reverse mathematics zoo
We introduce the notion of \tau-like partial order, where \tau is one of the linear order types \omega, \omega*, \omega+\omega*, and \zeta. For example, being \omega-like means that every element has finitely many predecessors, while being…
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…
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$.…
In mathematical logic there are two seemingly distinct kinds of principles called "reflection principles." Semantic reflection principles assert that if a formula holds in the whole universe, then it holds in a set-sized model. Syntactic…
There are two major generalizations of the standard ordinal analysis: One is Girard's $\Pi^1_2$-proof theory in which dilators are assigned to theories instead of ordinals. The other is Pohlers' generalized ordinal analysis with Spector…
Linear arithmetics are extensions of Presburger arithmetic (Pr) by one or more unary functions, each intended as multiplication by a fixed element (scalar), and containing the full induction schemes for their respective languages. In this…
Dilation theory is a paradigm for studying operators by way of exhibiting an operator as a compression of another operator which is in some sense well behaved. For example, every contraction can be dilated to (i.e., is a compression of) a…
A well-ordering principle is a principle of the form: If $X$ is well-ordered then $F(X)$ is well-ordered, where $F$ is some natural operator transforming linear orders into linear orders. Many important subsystems of Second-order Arithmetic…
In previous work, the author has shown that $\Pi^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…
A proof using the theory of completely positive maps is given to the fact that if $A \in M_2$, or $A \in M_3$ has a reducing eigenvalue, then every bounded linear operator $B$ with $W(B) \subseteq W(A)$ has a dilation of the form $I \otimes…
In the refinement calculus, monotonic predicate transformers are used to model specifications for (imperative) programs. Together with a natural notion of simulation, they form a category enjoying many algebraic properties. We build on this…
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…
We consider a class of tempered subordinators, namely a class of subordinators with one-dimensional marginal tempered distributions which belong to a family studied in [3]. The main contribution in this paper is a non-central moderate…
The reverse derivative is a fundamental operation in machine learning and automatic differentiation. This paper gives a direct axiomatization of a category with a reverse derivative operation, in a similar style to that given by Cartesian…
Let $\mathcal{H}$ be a complex Hilbert space and let $\big\{A_{n}\big\}_{n\geq 1}$ be a sequence of bounded linear operators on $\mathcal{H}$. Then a bounded operator $B$ on a Hilbert space $\mathcal{K} \supseteq \mathcal{H}$ is said to be…
We rigorously prove a form of disorder-resistance for a class of one-dimensional cellular automaton rules, including some that arise as boundary dynamics of two-dimensional solidification rules. Specifically, when started from a random…
Using the framework of operator or Calder\'on preconditioning, uniform preconditioners are constructed for elliptic operators discretized with continuous finite (or boundary) elements. The preconditioners are constructed as the composition…
We define a game semantics for second order classical arithmetic PA2 (with quantifiers over predicates on integers and full comprehension axiom). Our semantics is effective: moves are described by a finite amount of information and whenever…
We show that when certain statements are provable in subsystems of constructive analysis using intuitionistic predicate calculus, related sequential statements are provable in weak classical subsystems. In particular, if a $\Pi^1_2$…
Disjunctive Linear Arithmetic (DLA) is a major decidable theory that is supported by almost all existing theorem provers. The theory consists of Boolean combinations of predicates of the form $\Sigma_{j=1}^{n}a_j\cdot x_j \le b$, where the…