Related papers: Cut-elimination for $\omega_{1}$
There is no infinite sequence of $\Pi^1_1$-sound extensions of $\mathsf{ACA}_0$ each of which proves $\Pi^1_1$-reflection of the next. This engenders a well-founded ``reflection ranking'' of $\Pi^1_1$-sound extensions of $\mathsf{ACA}_0$.…
We introduce infinitary action logic with exponentiation -- that is, the multiplicative-additive Lambek calculus extended with Kleene star and with a family of subexponential modalities, which allows some of the structural rules…
We give a calculus for reasoning about the first-order fragment of classical logic that is adequate for giving the truth conditions of intuitionistic Kripke frames, and outline a proof-theoretic soundness and completeness proof, which we…
We characterize the compactness properties of the product of \lambda\ copies of the space \omega\ with the discrete topology, dealing in particular with the case \lambda\ singular, using regular and uniform ultrafilters, infinitary…
Using relativized ordinal analysis, we give a proof-theoretic characterization of the provably total set-recursive-from-$\omega$ functions of KPl and related theories.
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…
This article expands our work in [Ca16]. By its reliance on Turing computability, the classical theory of effectivity, along with effective reducibility and Weihrauch reducibility, is only applicable to objects that are either countable or…
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…
In this note we are concerned with the validity of an uncountable analogue of a combinatorial lemma due to Vlastimil Pt\'ak. We show that the validity of the result for $\omega_1$ can not be decided in ZFC alone. We also provide a…
We deal with the fragment of modal logic consisting of implications of formulas built up from the variables and the constant `true' by conjunction and diamonds only. The weaker language allows one to interpret the diamonds as the uniform…
Given a weakly compact cardinal $\kappa$, we give an axiomatization of intuitionistic first-order logic over $\mathcal{L}_{\kappa^+, \kappa}$ and prove it is sound and complete with respect to Kripke models. As a consequence we get the…
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…
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…
For which choices of $X,Y,Z\in\{\Sigma^1_1,\Pi^1_1\}$ does no sufficiently strong $X$-sound and $Y$-definable extension theory prove its own $Z$-soundness? We give a complete answer, thereby delimiting the generalizations of G\"odel's…
We introduce and study several notions of computability-theoretic reducibility between subsets of $\omega$ that are "robust" in the sense that if only partial information is available about the oracle, then partial information can be…
Let omega be the first infinite ordinal (or the set of all natural numbers) with the usual order <. In section 1 we show that, assuming the consistency of a supercompact cardinal, there may exist an ultrapower of omega, whose cardinality is…
It is well-known that natural axiomatic theories are pre-well-ordered by logical strength, according to various characterizations of logical strength such as consistency strength and inclusion of $\Pi^0_1$ theorems. Though these notions of…
$\Omega$-rule was introduced by W. Buchholz to give an ordinal-free cut-elimination proof for a subsystem of analysis with $\Pi^{1}_{1}$-comprehension. His proof provides cut-free derivations by familiar rules only for arithmetical…
In \cite{Ca2016} and \cite{Ca2018}, we introduced a notion of effective reducibility between set-theoretical $\Pi_{2}$-statements; in \cite{Ca2025}, this was extended to statements of arbitrary (potentially even infinite) quantifier…
This paper is an extended version of our work in \cite{Ca2025}. We extend the concept of effective reducibility between statements of set theory with ordinal Turing machines (OTMs) explored in \cite{Ca2018} for $\Pi_{2}$-statements to…