Related papers: Short Proofs for Slow Consistency

It was shown by Visser that Peano Arithmetic has the property that any two bi-interpretable extensions of it (in the same language) are equivalent. Enayat proposed to refer to this property of a theory as tightness and to carry out a more…

We prove that, for low-order (n < 5) stable polynomial segments or interval polynomials, there always exists a fixed polynomial such that their ratio is SPR-invariant, thereby providing a rigorous proof of Anderson's claim on SPR synthesis…

We analyse how the standard reductions between constraint satisfaction problems affect their proof complexity. We show that, for the most studied propositional, algebraic, and semi-algebraic proof systems, the classical constructions of…

The arithmetic regularity lemma for $\mathbb{F}_p^n$, proved by Green in 2005, states that given a subset $A\subseteq \mathbb{F}_p^n$, there exists a subspace $H\leq \mathbb{F}_p^n$ of bounded codimension such that $A$ is Fourier-uniform…

In this paper, the Pazy's Fixed Point Theorems of monotone $\alpha-$nonexpansive mapping $T$ are proved in a uniformly convex Banach space $E$ with the partial order "$\leq$". That is, we obtain that the fixed point set of $T$ with respect…

Most state-of-the-art satisfiability algorithms today are variants of the DPLL procedure augmented with clause learning. The main bottleneck for such algorithms, other than the obvious one of time, is the amount of memory used. In the field…

Consider a homogeneous polynomial $p(z_1,...,z_n)$ of degree $n$ in $n$ complex variables . Assume that this polynomial satisfies the property : \\ $|p(z_1,...,z_n)| \geq \prod_{1 \leq i \leq n} Re(z_i)$ on the domain $\{(z_1,...,z_n) :…

We construct here an iterative evaluation of all PR map codes: progress of this iteration is measured by descending complexity within "Ordinal" O := N[\omega] of polynomials in one indeterminate, ordered lexicographically. Non-infinit…

We consolidate two widely believed conjectures about tautologies -- no optimal proof system exists, and most require superpolynomial size proofs in any system -- into a $p$-isomorphism-invariant condition satisfied by all paddable…

It is a well known empirical observation that natural axiomatic theories are pre-well-ordered by consistency strength. For any natural theory $T$, the next strongest natural theory is $T+\mathsf{Con}_T$. We formulate and prove a statement…

In the paper we introduce a weak set theory $\mathsf{H}_{<\omega}$ . A formalization of arithmetic on finite von Neumann ordinals gives an embedding of arithmetical language into this theory. We show that $\mathsf{H}_{<\omega}$ proves a…

G\"odel's second incompleteness theorem is standardly understood as showing that no sufficiently strong, consistent theory of arithmetic can prove its own consistency, a result typically interpreted against a model-theoretic background in…

We make two contributions to the study of theory combination in satisfiability modulo theories. The first is a table of examples for the combinations of the most common model-theoretic properties in theory combination, namely stable…

Inconsistency Robustness is performance of information systems with pervasively inconsistent information. Inconsistency Robustness of the community of professional mathematicians is their performance repeatedly repairing contradictions over…

We introduce a notion of \emph{efficient stability} for finite presentations of groups. Informally, a finite presentation using generators $S$ and relations $R$ is \emph{stable} if any map from $S$ to unitaries that approximately satisfies…

We prove that, unless $\mathrm{P}=\mathrm{NP}$, no polynomial algorithm can approximate the minimum length of \sws for a given \san within a constant factor.

We consider pure equational theories that allow substitution but disallow induction, which we denote as PETS, based on recursive definition of their function symbols. We show that the Bounded Arithmetic theory $S^1_2$ proves the consistency…

The framework of algebraically natural proofs was independently introduced in the works of Forbes, Shpilka and Volk (2018), and Grochow, Kumar, Saks and Saraf (2017), to study the efficacy of commonly used techniques for proving lower…

We show that "The product of consecutive integers is never a power" and several results by Schinzel and Tijdeman on the solutions of the equation $y^m=P(x)$, for $m>1$, $y>1$, and $P(x)$ a polynomial with rational coefficients and with at…

We study reflection principles of Peano Arithmetic PA which are based on both proof and provability. Any such reflection principle in PA is equivalent to either $\Box P\!\rightarrow\! P$ ($\Box P$ stands for `$P$ is provable') or $\Box^k…