Related papers: Ordinal Notation
Here it is shown that standard set theory can be interpreted in a theory about order. The ordering here is about non-extensional flat classes, i.e. classes that are not elements of classes. So, stipulating a nearly well order over all those…
It is widely claimed that the natural axiom systems$\unicode{x2013}$including the large cardinal axioms$\unicode{x2013}$form a well-ordered hierarchy. Yet, as is well-known, it is possible to exhibit non-linearity and ill-foundedness by…
Using appropriate notation systems for proofs, cut-reduction can often be rendered feasible on these notations, and explicit bounds can be given. Developing a suitable notation system for Bounded Arithmetic, and applying these bounds, all…
This paper extends the class of ordinal regression models with a structured interpretation of the problem by applying a novel treatment of encoded labels. The net effect of this is to transform the underlying problem from an ordinal…
We present a unified theory for formal mathematical systems including recursive systems closely related to formal grammars, including the predicate calculus as well as a formal induction principle. We introduce recursive systems generating…
We present a new fragment of axiomatic set theory for pure sets and for the iteration of power sets within given transitive sets. It turns out that this formal system admits an interesting hierarchy of models with true membership relation…
We introduce a non-wellfounded proof system for intuitionistic logic extended with inductive and co-inductive definitions, based on a syntax in which fixpoint formulas are annotated with explicit variables for ordinals. We explore the…
In this paper, we give two proofs of the wellfoundedness of recursive notation systems for $\Pi_N$-reflecting ordinals. One is based on $\Pi_{N-1}^0$-inductive definitions, and the other is based on distinguished classes.
In this note we give a wellfoundedness proof of a computable notation system for first-order reflection.
We show that factorization systems, both strict and orthogonal, can be equivalently described as double categories satisfying certain properties. This provides conceptual reasons for why the category of sets and partial maps or the category…
Ordered logics and type systems have been used in a variety of applications including computational linguistics, memory allocation, stream processing, logical frameworks, parametricity, and enforcing security protocols. In most…
The purposes of this note are the following two; we first generalize Okada-Takeuti's well quasi ordinal diagram theory, utilizing the recent result of Dershowitz-Tzameret's version of tree embedding theorem with gap conditions. Second, we…
The paper focuses on the structure of fundamental sequences of ordinals smaller than $\epsilon_0$. A first result is the construction of a monadic second-order formula identifying a given structure, whereas such a formula cannot exist for…
In this note we give a simplified ordinal analysis of first-order reflection. An ordinal notation system $OT$ is introduced based on $\psi$-functions. Provable $\Sigma_{1}$-sentences on $L_{\omega_{1}^{CK}}$ are bounded through…
In the course of many mathematical developments involving 'number systems' like $\mathbb{N}, \mathbb{Z}, \mathbb{Q}, \mathbb{R}, \mathbb {C}$ etc., it sometimes becomes necessary to abstract away and study certain properties of the number…
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…
We motivate and study an infinite sequence of binary operations on the ordinal numbers, extending the standard arithmetic on the ordinals to higher degrees of iteration. Connections to the hyperoperations on the natural numbers are…
The generally accepted wisdom in computational circles is that pure proof verification is a solved problem and that the computationally hard elements and fertile areas of study lie in proof discovery. This wisdom presumably does hold for…
We present three ordinal notation systems representing ordinals below $\varepsilon_0$ in type theory, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. We show how ordinal…
Although there is a somewhat standard formalization of computability on countable sets given by Turing machines, the same cannot be said about uncountable sets. Among the approaches to define computability in these sets, order-theoretic…