Related papers: Arithmetical and Hyperarithmetical Worm Battles
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…
In a recent paper, Herbelin developed dPA${^\omega}$, a calculus in which constructive proofs for the axioms of countable and dependent choices could be derived via the memoization of choice functions. However, the property of normalization…
Markov logic uses weighted formulas to compactly encode a probability distribution over possible worlds. Despite the use of logical formulas, Markov logic networks (MLNs) can be difficult to interpret, due to the often counter-intuitive…
In 1933, G\"odel considered two modal approaches to describing provability. One captured formal provability and resulted in the logic GL and Solovay's Completeness Theorem. The other was based on the modal logic S4 and led to Artemov's…
The Logic of Proofs, LP, and its successor, Justification Logic, is a refinement of the modal logic approach to epistemology in which proofs/justifications are taken into account. In 2000 Kuznets showed that satisfiability for LP is in the…
The classical Goodstein process, defined via hereditary base-$k$ exponential normal form, is a well-known example of a principle unprovable in Peano Arithmetic. In this paper, we generalize this framework by constructing a new Goodstein…
We prove a variant of the multidimensional polynomial Szemer\'edi theorem of Bergelson and Leibman where one replaces polynomial sequences with other sparse sequences defined by functions that belong to some Hardy field and satisfy certain…
The correctness of most randomized distributed algorithms is expressed by a statement of the form ``some predicate of the executions holds with high probability, regardless of the order in which actions are scheduled''. In this paper, we…
We consider the thesis that an arithmetical relation, which holds for any, given, assignment of natural numbers to its free variables, is Turing-decidable if, and only if, it is the standard representation of a PA-provable formula. We show…
Generalized Discrete Logarithm Problem (GDLP) is an extension of the Discrete Logarithm Problem where the goal is to find $x\in\mathbb{Z}_s$ such $g^x\mod s=y$ for a given $g,y\in\mathbb{Z}_s$. Generalized discrete logarithm is similar but…
We offer a mathematical proof of consistency for Peano Arithmetic PA formalizable in PA. This result is compatible with Goedel's Second Incompleteness Theorem since our consistency proof does not rely on the representation of consistency as…
Let $E$ be a number field and $X$ a smooth geometrically connected variety defined over a characteristic $p$ finite field. Given an $n$-dimensional pure $E$-compatible system of semisimple $\lambda$-adic representations of the \'etale…
For each positive integer $n$, function $f$, and point $x$, the 1998 conjecture by Ghinchev, Guerragio, and Rocca states that the existence of the $n$-th Peano derivative $f_{(n)}(x)$ is equivalent to the existence of all $n(n+1)/2$…
The Lov\'asz Local Lemma is a classic result in probability theory that is often used to prove the existence of combinatorial objects via the probabilistic method. In its simplest form, it states that if we have $n$ `bad events', each of…
We study the problem of bounding the posterior distribution of discrete probabilistic programs with unbounded support, loops, and conditioning. Loops pose the main difficulty in this setting: even if exact Bayesian inference is possible,…
Heged\H{u}s's lemma is the following combinatorial statement regarding polynomials over finite fields. Over a field $\mathbb{F}$ of characteristic $p > 0$ and for $q$ a power of $p$, the lemma says that any multilinear polynomial $P\in…
G. Edelman, O. Sporns, and G. Tononi have introduced the neural complexity of a family of random variables, defining it as a specific average of mutual information over subfamilies. We show that their choice of weights satisfies two natural…
Pseudoentropy characterizations provide a quantitatively precise demonstration of the close relationship between computational hardness and computational randomness. We prove a unified pseudoentropy characterization that generalizes and…
Ordered logics and type systems have been used in a variety of applications including computational linguistics, memory allocation, stream processing, logical frameworks, parametricity, and enforcing security protocols. In most…
The Winner Determination Problem (WDP) in combinatorial auctions is NP-hard, and no existing method reliably predicts which instances will defeat fast greedy heuristics. The ML-for-combinatorial-optimization community has focused on…