Related papers: Turing jumps through provability

This article establishes a real-variable argument for Zygmund's theorem on almost everywhere convergence of strong arithmetic means of partial sums of Fourier series on $\mathbb{T}$, up to passing to a subsequence. Our approach extends to,…

We consider two orthogonal points of view on finite permutations, seen as pairs of linear orders (corresponding to the usual one line representation of permutations as words) or seen as bijections (corresponding to the algebraic point of…

An a priori semimeasure (also known as "algorithmic probability" or "the Solomonoff prior" in the context of inductive inference) is defined as the transformation, by a given universal monotone Turing machine, of the uniform measure on the…

We consider a class of two-prover interactive proof systems where each prover returns a single bit to the verifier and the verifier's verdict is a function of the XOR of the two bits received. We show that, when the provers are allowed to…

This paper finally fully elaborates the tree pulldown method used by one of us (Harrington) to settle McLaughlin's conjecture. This method enables the construction of a computable tree $T_0$ whose paths are incomparable over $0^{(\alpha)}$…

Whilst mathematicians assume classical reasoning principles by default they often context switch when working, restricting themselves to various forms of subclassical reasoning. This pattern is especially common amongst logicians and set…

For each positive integer $n$, function $f$, and point $c$, the GGR Theorem states that $f$ is $n$ times Peano differentiable at $c$ if and only if $f$ is $n-1$ times Peano differentiable at $c$ and the following $n$-th generalized…

In this dissertation we provide mathematical evidence that the concept of learning can be used to give a new and intuitive computational semantics of classical proofs in various fragments of Predicative Arithmetic. First, we extend Kreisel…

We consider a sequence $\mathbf{T} = (\mathcal{T}_n : n \in \mathbb{N}^+)$ of trees $\mathcal{T}_n$ where, for some $\Delta \in \mathbb{N}^+$ every $\mathcal{T}_n$ has height at most $\Delta$ and as $n \to \infty$ the minimal number of…

A well-known theorem due to Fefferman provides a characterization of Fourier multipliers from $H^1(\mathbb{T})$ to $\ell^1$, i.e. sequences $\left(\lambda_n\right)_{n=0}^\infty$ such that \[\sum_{n=0}^\infty \left|\lambda_n…

We show that if A is a linear order then Th(A) is either $\aleph_0$-categorical or Borel complete (in the sense of Friedman and Stanley). We generalize this; if A has countably many unary predicates attached, then Th(A) is…

A new generalisation of Goldbach's conjecture (GGC) - also generalising that of Lemoine - is tested, introduced by the first author. It states that for every pair of positive integers $m_1, m_2$, every sufficiently large integer $n$…

Models of computation operating over the real numbers and computing a larger class of functions compared to the class of general recursive functions invariably introduce a non-finite element of infinite information encoded in an arbitrary…

We show that no total functional can uniformly transform $\Pi_1$ primality into explicit $\Sigma_1$ witnesses without violating normalization in $\mathsf{HA}$. The argument proceeds through three complementary translations: a geometric…

Toda proved in 1989 that the (discrete) polynomial time hierarchy, $\mathbf{PH}$, is contained in the class $\mathbf{P}^{#\mathbf{P}}$, namely the class of languages that can be decided by a Turing machine in polynomial time given access to…

This paper explores epistemic realizability, a form of realizability in which the property that a piece of data constitutes evidence for a logical proposition is semi-decidable. In this framework, each proposition A is assigned a verifier}…

Here several perfect simulation algorithms are brought under a single framework, and shown to derive from the same probabilistic result, called here the Fundamental Theorem of Perfect Simulation (FTPS). An exact simulation algorithm has…

We study the principle phi implies box phi, known as `Strength' or `the Completeness Principle', over the constructive version of L\"ob's Logic. We consider this principle both for the modal language with the necessity operator and for the…

We study Linear Temporal Logic Modulo Theories over Finite Traces (LTLfMT), a recently introduced extension of LTL over finite traces (LTLf) where propositions are replaced by first-order formulas and where first-order variables referring…

Erd\H{o}s first conjectured that infinitely often we have $\varphi(n) = \sigma(m)$, where $\varphi$ is the Euler totient function and $\sigma$ is the sum of divisor function. This was proven true by Ford, Luca and Pomerance in 2010. We ask…