Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userOn Goodman realizability
86
0
0.0
(
0
)
Authors
Emanuele Frittaion
Ask ChatGPT about the research
No Arabic abstract
Goodmans 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.
rate research
Read More
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.
We first show that in the function realizability topos every metric space is separable, and every object with decidable equality is countable. More generally, working with synthetic topology, every $T_0$-space is separable and every discrete space is countable. It follows that intuitionistic logic does not show the existence of a non-separable metric space, or an uncountable set with decidable equality, even if we assume principles that are validated by function realizability, such as Dependent and Function choice, Markovs principle, and Brouwers continuity and fan principles.
In 1945, A. W. Goodman and R. E. Goodman proved the following conjecture by P. ErdH{o}s: Given a family of (round) disks of radii $r_1$, $ldots$, $r_n$ in the plane it is always possible to cover them by a disk of radius $R = sum r_i$, provided they cannot be separated into two subfamilies by a straight line disjoint from the disks. In this note we show that essentially the same idea may work for different analogues and generalizations of their result. In particular, we prove the following: Given a family of positive homothetic copies of a fixed convex body $K subset mathbb{R}^d$ with homothety coefficients $tau_1, ldots, tau_n > 0$ it is always possible to cover them by a translate of $frac{d+1}{2}left(sum tau_iright)K$, provided they cannot be separated into two subfamilies by a hyperplane disjoint from the homothets.
Quantum walks are a promising framework that can be used to both understand and implement quantum information processing tasks. The quantum stochastic walk is a recently developed framework that combines the concept of a quantum walk with that of a classical random walk, through open system evolution of a quantum system. Quantum stochastic walks have been shown to have applications in as far reaching fields as artificial intelligence. However, there are significant constraints on the kind of open system evolutions that can be realized in a physical experiment. In this work, we discuss the restrictions on the allowed open system evolution, and the physical assumptions underpinning them. We show that general implementations would require the complete solution of the underlying unitary dynamics, and sophisticated reservoir engineering, thus weakening the benefits of experimental investigations.
We use recent results by Bainbridge-Chen-Gendron-Grushevsky-Moeller on compactifications of strata of abelian differentials to give a comprehensive solution to the realizability problem for effective tropical canonical divisors in equicharacteristic zero. Given a pair $(Gamma, D)$ consisting of a stable tropical curve $Gamma$ and a divisor $D$ in the canonical linear system on $Gamma$, we give a purely combinatorial condition to decide whether there is a smooth curve $X$ over a non-Archimedean field whose stable reduction has $Gamma$ as its dual tropical curve together with a effective canonical divisor $K_X$ that specializes to $D$. Along the way, we develop a moduli-theoretic framework to understand Bakers specialization of divisors from algebraic to tropical curves as a natural toroidal tropicalization map in the sense of Abramovich-Caporaso-Payne.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
