Related papers: Well-orders in the transfinite Japaridze algebra
We show that arithmetical transfinite recursion is equivalent to a suitable formalization of the following: For every ordinal $\alpha$ there exists an ordinal $\beta$ such that $1+\beta\cdot(\beta+\alpha)$ (ordinal arithmetic) admits an…
We study the computability-theoretic complexity and proof-theoretic strength of the following statements: (1) "If X is a well-ordering, then so is epsilon_X", and (2) "If X is a well-ordering, then so is phi(alpha,X)", where alpha is a…
We consider anti-unification for simply typed lambda terms in associative, commutative, and associative-commutative theories and develop a sound and complete algorithm which takes two lambda terms and computes their generalizations in the…
We describe the extension of normal iteration strategies with appropriate condensation properties to strategies for stacks of normal trees, with full normalization. Given a regular uncountable cardinal $\Omega$ and an…
Polymodal provability logic GLP is incomplete w.r.t. Kripke frames. It is known to be complete w.r.t. topological semantics, where the diamond modalities correspond to topological derivative operations. However, the topologies needed for…
Let $\Lambda=\Bbb Z[t,t^{-1}]$ be the ring of Laurent polynomials over $\Bbb Z$. We classify all $\Lambda$-modules $M$ with $|M|=p^n$, where $p$ is a primes and $n\le 4$. Consequently, we have a classification of Alexander quandles of order…
The $\lambda$-superposition calculus is a successful approach to proving higher-order formulas. However, some parts of the calculus are extremely explosive, notably due to the higher-order unifier enumeration and the functional…
We study the computational strength of resetting $\alpha$-register machines, a model of transfinite computability introduced by P. Koepke in \cite{K1}. Specifically, we prove the following strengthening of a result from \cite{C}: For an…
Let $\mathfrak g$ be a finite-dimensional simple Lie algebra of type $D$ or $E$ and $\lambda$ be a dominant integral weight whose support bounds the subdiagram of type $D_4$. We study certain quantum affinizations of the simple $\mathfrak…
We prove, via transfinite recursion, the existence, inside any linearly ordered set of appropriate regular cardinality $\lambda$, of a particular kind of well-ordered subsets characterized by the property of $\lambda$-fullness. Let $H$ be a…
Randomized higher-order computation can be seen as being captured by a lambda calculus endowed with a single algebraic operation, namely a construct for binary probabilistic choice. What matters about such computations is the probability of…
We present a type inference algorithm for lambda-terms in Elementary Affine Logic using linear constraints. We prove that the algorithm is correct and complete.
We introduce axiomatically the ring $\bf{Z}_\kappa$ of the Euclidean integers, that can be viewed as the ``integral part" of the field $\mathbb{E}$ of Euclidean numbers of [4], where the transfinite sum of ordinal indexed $\kappa$-sequences…
In this note the well-ordering principle for the derivative of normal functions on ordinals is shown to be equivalent to the existence of arbitrarily large countable coded omega-models of the well-ordering principle for the function.
For commutative rings, we introduce the notion of a {\em universal grading}, which can be viewed as the "largest possible grading". While not every commutative ring (or order) has a universal grading, we prove that every {\em reduced order}…
Many different systems with explicit substitutions have been proposed to implement a large class of higher-order languages. Motivations and challenges that guided the development of such calculi in functional frameworks are surveyed in the…
Abashidze and Blass independently proved that the modal logic $\sf{GL}$ is complete for its topological interpretation over any ordinal greater than or equal to $\omega^\omega$ equipped with the interval topology. Icard later introduced a…
We bring forward a logical system of transition algebras that enhances many-sorted first-order logic using features from dynamic logics. The sentences we consider include compositions, unions, and transitive closures of transition…
We present a new approach to termination analysis of logic programs. The essence of the approach is that we make use of general orderings (instead of level mappings), like it is done in transformational approaches to logic program…
In this paper, we discuss a proof system $\mathsf{NGL}$ for the logic $\mathbf{GL}$ of provability, which is equipped with an $\omega$-rule. We show the three classes of transitive Kripke frames, the class which strongly validates the…