Searcharxiv⌕ Search

arXiv subjects

Emanuele Frittaion

Publications and source records attributed to Emanuele Frittaion.

16 recordsLinked to original sources
arXiv2026

Axiom Beta Implies Elementary Transfinite Recursion

We show that $\mathbf{C}$, a weak theory of sets with Axiom Beta, proves the scheme of Elementary, or $Δ_0$ Transfinite Recursion and can generate, for every set, the corresponding relativized constructible hierarchy. We show that the theory $\mathbf{C}$ corresponds to Simpson's system $\mathbf{ATR}_0^\text{set}$ without the Axiom of Countability. In fact, $\mathbf{C}$ proves the totality of the Veblen function and of all primitive recursive set functions. In particular, this means our system $\mathbf{C}$ is equivalent to $\mathbf{PRS}ω+\text{Axiom Beta}$. We also establish an upper bound, though not a sharp one, for the $Σ_1$-definable functions of $\mathbf{C}$. Finally, we show that the variant of $\mathbf{C}$ in which the Finite Powerset Axiom is replaced by the closure under the rudimentary functions is a strictly weaker theory and no longer ensures the existence of the relativized constructible hierarchy.

math.LO↗
arXiv2025

Iterating reflection over intuitionistic arithmetic

In this note, we investigate iterations of consistency, local and uniform reflection over $\mathbf{HA}$ (Heyting Arithmetic). In the case of uniform reflection, we give a new proof of Dragalin's extension of Feferman's completeness theorem to $\mathbf{HA}$, drawing on Rathjen's proof of Feferman's classical result.

math.LO↗
arXiv2024

Extensional realizability and choice for dependent types in intuitionistic set theory

In "Extensional realizability for intuitionistic set theory", we introduced an extensional variant of generic realizability, where realizers act extensionally on realizers, and showed that this form of realizability provides "inner" models of $\sf CZF$ (constructive Zermelo-Fraenkel set theory) and $\sf IZF$ (intuitionistic Zermelo-Fraenkel set theory), that further validate ${\sf AC}_{\sf FT}$ (the axiom of choice in all finite types). In this paper, we show that extensional generic realizability validates several choice principles for dependent types, all exceeding ${\sf AC}_{\sf FT}$. We then show that adding such choice principles does not change the arithmetic part of either $\sf CZF$ or $\sf IZF$.

math.LO↗
arXiv2024

Peano Arithmetic, games and descent recursion

We analyze Coquand's game-theoretic interpretation of Peano Arithmetic through the lens of elementary descent recursion. In Coquand's game semantics, winning strategies correspond to infinitary cut-free proofs and cut elimination corresponds to debates between these winning strategies. The proof of cut elimination, i.e., the proof that such debates eventually terminate, is by transfinite induction on certain interaction sequences of ordinals. In this paper, we provide a direct implementation of Coquand's proof, one that allows us to describe winning strategies by descent recursive functions. As a byproduct, we obtain yet another proof of well-known results about provably recursive functions and functionals.

math.LO↗
arXiv2024

Choice and independence of premise rules in intuitionistic set theory

Choice and independence of premise principles play an important role in characterizing Kreisel's modified realizability and Gödel's Dialectica interpretation. In this paper we show that a great many intuitionistic set theories are closed under the corresponding rules for finite types over $\mathbb{N}$. It is also shown that the existence property (or existential definability property) holds for statements of the form $\exists y^σ\, φ(y)$, where the variable $y$ ranges over objects of finite type $σ$. This applies in particular to ${\sf CZF}$ (Constructive Zermelo-Fraenkel set theory) and ${\sf IZF}$ (Intuitionistic Zermelo-Fraenkel set theory), two systems known not to have the general existence property. On the technical side, the paper uses a method that amalgamates generic realizability for set theory with truth, whereby the underlying partial combinatory algebra is required to contain all objects of finite type.

math.LO↗
arXiv2022

A note on fragments of uniform reflection in second order arithmetic

We consider fragments of uniform reflection for formulas in the analytic hierarchy over theories of second order arithmetic. The main result is that for any second order arithmetic theory $T_0$ extending ${\sf RCA}_0$ and axiomatizable by a $Π^1_{k+2}$ sentence, and for any $n\geq k+1$, \[ T_0+ \mathrm{RFN}_{\varPi^1_{n+2}}(T) \ = \ T_0 + \mathrm{TI}_{\varPi^1_n}(\varepsilon_0), \] \[ T_0+ \mathrm{RFN}_{\varSigma^1_{n+1}}(T) \ = \ T_0+ \mathrm{TI}_{\varPi^1_n}(\varepsilon_0)^{-}, \] where $T$ is $T_0$ augmented with full induction, and $\mathrm{TI}_{\varPi^1_n}(\varepsilon_0)^{-}$ denotes the schema of transfinite induction up to $\varepsilon_0$ for $\varPi^1_n$ formulas without set parameters.

math.LO↗
arXiv2021

Completeness of the primitive recursive $ω$-rule

Shoenfield's completeness theorem (1959) states that every true first order arithmetical sentence has a recursive $ω$-proof encodable by using recursive applications of the $ω$-rule. For a suitable encoding of Gentzen style $ω$-proofs, we show that Shoenfield's completeness theorem applies to cut free $ω$-proofs encodable by using primitive recursive applications of the $ω$-rule. We also show that the set of codes of $ω$-proofs, whether it is based on recursive or primitive recursive applications of the $ω$-rule, is $Π^1_1$ complete. The same $Π^1_1$ completeness results apply to codes of cut free $ω$-proofs.

math.LO↗
arXiv2020

Extensional realizability for intuitionistic set theory

In generic realizability for set theories, realizers treat unbounded quantifiers generically. To this form of realizability, we add another layer of extensionality by requiring that realizers ought to act extensionally on realizers, giving rise to a realizability universe $\mathrm{V_{ex}}(A)$ in which the axiom of choice in all finite types ${\sf AC}_{\sf FT}$ is realized, where $A$ stands for an arbitrary partial combinatory algebra. This construction furnishes 'inner models' of many set theories that additionally validate ${\sf AC}_{\sf FT}$, in particular it provides a self-validating semantics for $\sf CZF$ (Constructive Zermelo-Fraenkel set theory) and $\sf IZF$ (Intuitionistic Zermelo-Fraenkel set theory). One can also add large set axioms and many other principles.

math.LO↗
arXiv2018

On Goodman realizability

Goodman's theorem (1976) states that intuitionistic finite-type arithmetic plus the axiom of choice plus the axiom of relativized dependent choice is conservative over Heyting arithmetic. The same result applies to the extensional variant. This is due to Beeson (1979). In this paper we modify Goodman realizability (1978) and provide a new proof of the extensional case.

math.LO↗
arXiv2017

The strength of SCT soundness

In this paper we continue the study, from Frittaion, Steila and Yokoyama (2017), on size-change termination in the context of Reverse Mathematics. We analyze the soundness of the SCT method. In particular, we prove that the statement "any program which satisfies the combinatorial condition provided by the SCT criterion is terminating" is equivalent to $\mathrm{WO}(ω_3)$ over $\mathsf{RCA_0}$

math.LO↗
arXiv2016

The strength of the SCT criterion

We undertake the study of size-change analysis in the context of Reverse Mathematics. In particular, we prove that the SCT criterion is equivalent to $Σ^0_2$-induction over RCA$_0$.

math.LO↗
arXiv2016

Coloring the rationals in reverse mathematics

Ramsey's theorem for pairs asserts that every 2-coloring of the pairs of integers has an infinite monochromatic subset. In this paper, we study a strengthening of Ramsey's theorem for pairs due to Erdos and Rado, which states that every 2-coloring of the pairs of rationals has either an infinite 0-homogeneous set or a 1-homogeneous set of order type eta, where eta is the order type of the rationals. This theorem is a natural candidate to lie strictly between the arithmetic comprehension axiom and Ramsey's theorem for pairs. This Erdos-Rado theorem, like the tree theorem for pairs, belongs to a family of Ramsey-type statements whose logical strength remains a challenge.

math.LO↗
arXiv2015

Reverse mathematics, well-quasi-orders, and Noetherian spaces

A quasi-order $Q$ induces two natural quasi-orders on $P(Q)$, but if $Q$ is a well-quasi-order, then these quasi-orders need not necessarily be well-quasi-orders. Nevertheless, Goubault-Larrecq showed that moving from a well-quasi-order $Q$ to the quasi-orders on $P(Q)$ preserves well-quasi-orderedness in a topological sense. Specifically, Goubault-Larrecq proved that the upper topologies of the induced quasi-orders on $P(Q)$ are Noetherian, which means that they contain no infinite strictly descending sequences of closed sets. We analyze various theorems of the form "if $Q$ is a well-quasi-order then a certain topology on (a subset of) $P(Q)$ is Noetherian" in the style of reverse mathematics, proving that these theorems are equivalent to ACA_0 over RCA_0. To state these theorems in RCA_0 we introduce a new framework for dealing with second-countable topological spaces.

math.LO↗
arXiv2013

Reverse Mathematics and initial intervals

In this paper we study the reverse mathematics of two theorems by Bonnet about partial orders. These results concern the structure and cardinality of the collection of the initial intervals. The first theorem states that a partial order has no infinite antichains if and only if its initial intervals are finite unions of ideals. The second one asserts that a countable partial order is scattered and does not contain infinite antichains if and only if it has countably many initial intervals. We show that the left to right directions of these theorems are equivalent to ACA_0 and ATR_0, respectively. On the other hand, the opposite directions are both provable in WKL_0, but not in RCA_0. We also prove the equivalence with ACA_0 of the following result of Erdös and Tarski: a partial order with no infinite strong antichains has no arbitrarily large finite strong antichains.

math.LO↗
arXiv2012

Linear extensions of partial orders and Reverse Mathematics

We introduce the notion of τ-like partial order, where τis one of the linear order types ω, ω*, ω+ω*, and ζ. For example, being ω-like means that every element has finitely many predecessors, while being ζ-like means that every interval is finite. We consider statements of the form "any τ-like partial order has a τ-like linear extension" and "any τ-like partial order is embeddable into τ" (when τ is ζ this result appears to be new). Working in the framework of reverse mathematics, we show that these statements are equivalent either to BΣ^0_2 or to ACA_0 over the usual base system RCA_0.

math.LO↗