https://arxiv.org/api/Qd6D2VZJPU+jK2b8vzYKNC8mujE 2026-04-04T21:29:53Z 15337 360 15 http://arxiv.org/abs/2602.12131v1 2026-02-12T16:19:49Z

The primary aim of Hilbert's proof theory was to establish the consistency of classical mathematics using finitary means only. Hilbert's strategy for doing this was to eliminate the infinite (in the form of unbounded quantifiers) from formalized proofs using the so-called epsilon substitution method. The result is a formal proof which does not mention or appeal to infinite objects or "concept-formations." However, as later developments showed, the consistency proof itself lets the infinite back into proof theory, through a back door, so to speak. The paper outlines the epsilon substitution method as an example of how proof-theoretic constructions "eliminate the infinite" from formal proofs, and how they aim to establish conservativity and consistency. The proof also requires an argument that this proof theoretic construction always works. This second argument, however, requires possibly infinitary reasoning at the meta-level, using induction on ordinal notations.

2026-02-12T16:19:49Z Richard Zach http://arxiv.org/abs/2602.12054v1 2026-02-12T15:18:10Z

Cyclic proof theory breaks tradition by allowing certain infinite proofs: those that can be represented by a finite graph, while satisfying a soundness condition. We reconcile cyclic proofs with traditional finite proofs: we extend abstract cyclic proof systems with a well-founded induction principle, and transform any cyclic proof into a finite proof in the extended system. Moreover, this transformation preserves the structure of the cyclic proof. Our results leverage an annotated representation of cyclic proofs, which allows us to extract induction hypotheses and to determine their introduction order. The representation is essentially a reset proof with one key modification: names must be covered in a uniform way before a reset. This innovation allows us to handle cyclic proofs where the underlying inductive sort is non-linear. Our framework is general enough to cover recursive functions satisfying the size-change termination principle, which are viewed as cyclic proofs under the Curry-Howard correspondence.

2026-02-12T15:18:10Z 15 pages Lide Grotenhuis Daniël Otten http://arxiv.org/abs/2602.11848v1 2026-02-12T11:41:24Z

Here we show, in the second paper in a series of articles, methods to calculate propositional statements with algebraic polyno mials as symbols for the connectives, which here are named operators. In the first article, we explained this formulation of the Propositional Calculus. In short, we transform to a dual space, which we here refer to as a polynomial family, which is another shape of DBNF. We name the polynomial families as PBNF, which stands for Polynomial Boolean Normal Form. We just use the one law of inference, the rule of Substi tution. We can use different polynomial families in the House of PBNF, depending on the statement form, making it even simpler. It is also pos sible to find new theorems and generalize older ones, for example, those given by Church and Barkley Rosser (see follow-up article) concerning duality.

2026-02-12T11:41:24Z Pelle Brooke Borgeke http://arxiv.org/abs/2601.10231v2 2026-02-12T04:10:08Z

A proof will be presented that the existence of a non-trivial $Σ_1$-elementary embedding $j: V_{λ+3} \prec V_{λ+3}$ is inconsistent with $\textsf{ZF}$. Sections 1 and 2 shall review various important contributions from the literature, notably including \cite{Goldberg2020}, \cite{Schlutzenberg2020}, and \cite{Woodin2010}, the latter reference being where the crucial forcing construction is presented. Section 3 shall introduce some new large cardinal properties, of consistency strength intermediate between $\mathsf{I_3}$ and $\mathsf{I_2}$, and greater than $\mathsf{I_1}$, respectively. The proof of the inconsistency with $\mathsf{ZF}$ of the existence of a non-trivial $Σ_1$-elementary embedding $j:V_{λ+3} \prec V_{λ+3}$ shall be given in Section 4. The claims of Sections 2 and 4 are provable in $\textsf{ZF}$; those of Section 3, with the exception of the last two theorems, in $\textsf{ZFC}$.

2026-01-15T09:45:49Z Rupert McCallum http://arxiv.org/abs/2005.10080v15 2026-02-12T04:05:50Z

We show that it is provable in PA that there is an arithmetically definable sequence $\{φ_{n}:n \in ω\}$ of $Π^{0}_{2}$-sentences, such that - PRA+$\{φ_{n}:n \in ω\}$ is $Π^{0}_{2}$-sound and $Π^{0}_{1}$-complete - the length of $φ_{n}$ is bounded above by a polynomial function of $n$ with positive leading coefficient - PRA+$φ_{n+1}$ always proves 1-consistency of PRA+$φ_{n}$. One has that the growth in logical strength is in some sense "as fast as possible", manifested in the fact that the total general recursive functions whose totality is asserted by the true $Π^{0}_{2}$-sentences in the sequence are cofinal growth-rate-wise in the set of all total general recursive functions. We then develop an argument which makes use of a sequence of sentences constructed by an application of the diagonal lemma, which are generalisations in a broad sense of Hugh Woodin's "Tower of Hanoi" construction as outlined in his essay "Tower of Hanoi" in Chapter 18 of the anthology "Truth in Mathematics". The argument establishes the result that it is provable in PA that $P \neq NP$. We indicate how to pull the argument all the way down into SEFA.

2020-05-19T08:56:15Z Rupert McCallum http://arxiv.org/abs/2602.11432v1 2026-02-11T23:16:20Z

Let $Γ\subset PSL_2(\mathbb{R})$ be a non-arithmetic Fuchsian group of the first kind with finite covolume, and let $j_Γ$ be a corresponding uniformizer. In this paper we introduce a natural $L_{ω_1,ω}$-axiomatization $T^{\infty}_{SF}$ of the theory of $j_Γ$ viewed as a covering map. We show that $T^{\infty}_{SF}$ is categorical in all infinite cardinalities, extending to the non-arithmetic setting earlier results of Daw and Harris obtained in the arithmetic case. We also show that the associated first-order theory $T_{j_Γ}$ is complete, admits elimination of quantifiers, and is $ω$-stable.

2026-02-11T23:16:20Z John Baldwin Joel Nagloo http://arxiv.org/abs/2602.11134v1 2026-02-11T18:45:05Z

Given partial information about a set, we are interested in fully recovering the original set from what is given. If a set encodes itself robustly, any partial information about the set suffices to fully recover the information about the original set. Jockusch defined a set $A$ to be introenumerable if each infinite subset of $A$ can enumerate $A$, and this is an example of a set which encodes itself. There are several other notions capturing self-encoding differently. We say $A$ is uniformly introenumerable if each infinite subset of $A$ can uniformly enumerate $A$, whereas $A$ is introreducible if each infinite subset of $A$ can compute $A$. We investigate properties of various notions of self-encoding and prove new results on their interactions. Greenberg, Harrison-Trainor, Patey, and Turetsky showed that we can always find some uniformity from an introenumerable set. We show that this can be reversed: we can construct an introenumerable set by patching up uniformity. This gives a rise to a new method of constructing a nontrivial introenumerable or introreducible set.

2026-02-11T18:45:05Z 33 pages, 1 figure (using tikz), submitted to Computability journal Taeyoung Em http://arxiv.org/abs/2601.04081v2 2026-02-11T15:33:46Z

A paradefinite logic is a logic that can serve as the underlying logic for theories that are inconsistent or incomplete. A well-known paradefinite logic is Belnap-Dunn logic. Various expansions of Belnap-Dunn logic have been studied in the literature. In this note, it is argued that the most natural paradefinite logic relative to classical logic is the expansion of Belnap-Dunn logic with a falsity connective and an implication connective for which the standard deduction theorem holds.

2026-01-07T16:48:47Z 8 pages; minor revision of v1: all incorrect occurrences of "reversible" changed into "invertible" C. A. Middelburg http://arxiv.org/abs/2602.10844v1 2026-02-11T13:31:03Z

In the setting of constructive mathematics, we suggest and study a framework for decidability of properties, which allows for finer distinctions than just "decidable, semidecidable, or undecidable". We work in homotopy type theory and use Brouwer ordinals to specify the level of decidability of a property. In this framework, we express the property that a proposition is $α$-decidable, for a Brouwer ordinal $α$, and show that it generalizes decidability and semidecidability. Further generalizing known results, we show that $α$-decidable propositions are closed under binary conjunction, and discuss for which $α$ they are closed under binary disjunction. We prove that if each $P(i)$ is semidecidable, then the countable meet $\forall i\in \mathbb N. P(i)$ is $ω^2$-decidable, and similar results for countable joins and iterated quantifiers. We also discuss the relationship with countable choice. All our results are formalized in Cubical Agda.

2026-02-11T13:31:03Z Tom de Jong Nicolai Kraus Aref Mohammadzadeh Fredrik Nordvall Forsberg http://arxiv.org/abs/2308.12195v4 2026-02-11T12:12:39Z

In this paper we prove motivic versions of the Langlands-Shelstad Fundamental Lemma and Ngô's Geometric Stabilization. To achieve this, we follow the strategy from the recent proof by Groechenig, Wyss and Ziegler which avoided the use of perverse sheaves using instead $p$-adic integration and Tate duality. We make a key use of a construction of Denef and Loeser which assigns a virtual motive to any definable set in the theory of pseudo-finite fields.

2023-08-23T15:35:22Z 58 pages Arthur Forey François Loeser Dimitri Wyss http://arxiv.org/abs/2212.02653v4 2026-02-10T23:56:55Z

We explore new interactions between finite model theory and classical streams of universal algebra and semigroup theory. A key result is an example of finite algebras whose variety is not finitely axiomatisable in first order logic, but where the class of finite members are finitely axiomatisable amongst finite algebras. These algebras present a negative solution to a first order formulation of the Eilenberg-Schützenberger problem, and witness the simultaneous failure of the Łos-Tarski Theorem, the SP-Preservation Theorem and Birkhoff's HSP-Preservation Theorem at the finite level. The examples also show that a pseudovariety without any finite pseudoequational basis may be finitely axiomatisable in first order logic amongst finite algebras. Other results include the undecidability of deciding first order definability of the pseudovariety of a finite algebra, and a mapping from any fixed finite template constraint satisfaction problem to a first order equivalent variety membership problem.

2022-12-05T23:21:04Z Lucy Ham Marcel Jackson http://arxiv.org/abs/1512.03127v4 2026-02-10T23:50:09Z

We examine some flexible notions of constraint satisfaction, observing some relationships between model theoretic notions of universal Horn class membership and robust satisfiability. We show the \texttt{NP}-completeness of $2$-robust monotone 1-in-3 3SAT in order to give very small examples of finite algebras with \texttt{NP}-hard variety membership problem. In particular we give a $3$-element algebra with this property, and solve a widely stated problem by showing that the $6$-element Brandt monoid has \texttt{NP}-hard variety membership problem. These are the smallest possible sizes for a general algebra and a semigroup to exhibit \texttt{NP}-hardness for the membership problem of finite algebras in finitely generated varieties.

2015-12-10T02:31:37Z International Journal of Algebra and ComputationVol. 35, No. 06, pp. 771-821 (2025) Marcel Jackson 10.1142/S0218196725500225 http://arxiv.org/abs/2512.15391v2 2026-02-10T15:29:04Z

Uniform interpolation is a strengthening of interpolation that holds for certain propositional logics. The starting point of this chapter is a theorem of A. Pitts, which shows that uniform interpolation holds for intuitionistic propositional logic. We outline how this theorem may be proved semantically via the definability of bisimulation quantifiers, and how it generalizes to an open mapping theorem between Esakia spaces. We also discuss connections between uniform interpolation and research in categorical logic, algebra, and model theory.

2025-12-17T12:41:27Z To appear as chapter 9 in: B. ten Cate, J. C. Jung, P. Koopmann, C. Wernhard, F. Wolter (eds), Theory and Applications of Craig Interpolation. Ubiquity Press (2026) Sam van Gool http://arxiv.org/abs/2602.08852v2 2026-02-10T14:54:32Z

This paper defines a Mitchell rank for supercompact cardinals. If $κ$ is a $θ$-supercompact cardinal then $o_{θ-sc}(κ) = \sup \{ o_{θ-sc}(μ) + 1 \ | \ μ\in m(κ)\}$, where $m(κ)$ is the collection of normal fine measures on $P_κθ$. We show how to force to kill the degree of a measurable cardinal $κ$ to any specified degree which is less than or equal to the degree of $κ$ in the ground model. We will also show how to softly kill the Mitchell rank for supercompactness of any supercompact cardinal so that in the forcing extension it is any desired degree less than or equal to its degree in the ground model, along with some results concerning strongly compact cardinals.

2026-02-09T16:17:50Z arXiv admin note: substantial text overlap with arXiv:1506.03432 Erin Carmody http://arxiv.org/abs/2601.18863v2 2026-02-10T14:53:10Z

Effective field theories consistent with quantum gravity obey surprising finiteness constraints, appearing in several distinct but interconnected forms. In this work we develop a framework that unifies these observations by proposing that the defining data of such theories, as well as the landscape of effective field theories that are valid at least up to a fixed cutoff, admit descriptions with a uniform bound on complexity. To make this precise, we use tame geometry and work in sharply o-minimal structures, in which tame sets and functions come with two integer parameters that quantify their information content; we call this pair their tame complexity. Our Finite Complexity Conjectures are supported by controlled examples in which an infinite Wilsonian expansion nevertheless admits an equivalent finite-complexity description, typically through hidden rigidity conditions such as differential or recursion relations. We further assemble evidence from string compactifications, highlighting the constraining role of moduli space geometry and the importance of dualities. This perspective also yields mathematically well-defined notions of counting and volume measures on the space of effective theories, formulated in terms of effective field theory domains and coverings, whose finiteness is naturally enforced by the conjectures.

2026-01-26T19:00:00Z 49 pages, 7 figures; v2: minor corrections Thomas W. Grimm David Prieto Mick van Vliet