Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [bounded-arithmetic]

The tag has no usage guidance.

5
votes
1answer
331 views

What is the consistency strength of this theory?

Language: first-order logic Primitives: $=, S, \in $ (the first denotes identity, the second denotes “is a successor of”, and the third denotes membership relation). Axioms: those of identity ...
-1
votes
0answers
80 views

Upper bound on the spectral radius of summation of two matrices one symmetric one diagonal

I am looking for an upper bound for the largest absolute value of eigenvalues of the summation of two matrices $\underset{i}\max{|λi(A+K)|}$ where $A$ is symmetric with real nonnegative eigenvalues ...
6
votes
1answer
211 views

Provability in $S^1_2$

What are some examples of natural true statements of the form $∀n φ(n)$ ($φ$ is a polynomial time computation/test) that are unprovable in $S^1_2$? Examples may be unconditional or dependent on ...
0
votes
0answers
152 views

Does Bounded Arithmetic, $I\Delta_0$, prove the Recursion Theorem?

Compare my question Does Robinson Arithmetic already entail the Recursion Theorem. I would find it desirable and interesting if $I\Delta_0$ could be extended with a comprehension principle CP stating ...
6
votes
1answer
153 views

Logical complexity of hard functions conjectures

Let $\phi_1$ and $\phi_2$ be the following statements: $\phi_1:$ There is a function $f:\{0,1\}^*\to\{0,1\}$ computable in $E$ that has circuit complexity $2^{\Omega(n)}$. $\phi_2:$ There is a ...
3
votes
0answers
98 views

Collapsing the Intuitionistic Bounded Arithmetics Hierarchy

Let $iT$ be the intuitionistic first order theory with non-logical axioms of classical first order theory $T$. Theorem1. If $\mathsf{T^i_2}\vdash \mathsf{T_2}$, then $\mathsf{T^i_2}$ proves that ...
3
votes
1answer
103 views

On subtheories of $\mathsf{T_2+EXP}$

By famous KPT theorem, if $\mathsf{T^i_2}\vdash \mathsf{T^j_2}$ for some $0<i<j$, then the polynomial hierarchy collapses. So it seems this bounded arithmetic hierarchy does not collapse. Also, ...
2
votes
1answer
189 views

Bounded Arithmetic and Counting

Let $\mathcal{L}=\{0,S,+,\cdot,=,<,X,R,S\}$ be the language of arithmetic with three additional predicate symbols $X(v)$, $R(v,u)$ and $S(v,u)$. Let $\phi(x),\psi(x,y)$ and $\eta(x,y)$ be formulas ...
2
votes
0answers
176 views

$P=NP$ and provability of family of propositional formulas

Let $\mathcal{L}'=\{+,\cdot,0,S,=,<,||,\#,R\}$ be the lanugage of bounded arithmetic with a $k$-ary relation $R$. For every bounded sentence $\phi({\bf\bar{n}})$ in $\mathcal{L}'$ define ...
10
votes
0answers
188 views

Collapsing the Linear Time Hierarchy and finite axiomatizability of bounded arithmetic

It is well known that if ${\bf T_2}$ (or $I\Delta_0+\Omega_1$) is finitely axiomatizable, then the Polynomial Hierarchy collapses. Q. Is there any similar relation between $I\Delta_0$ and Linear ...
3
votes
0answers
54 views

Equational theory for resolution proof system

Is there any equational theory $T$ like $PV$ with following properties: If $T\vdash f=g$ for terms $f$ and $g$, translation of $f=g$ to propositional formulas has polynomial resolution proof.(like $...
10
votes
2answers
473 views

Bounded Arithmetic vs Complexity Theory

In this post, when I talk about bounded arithmetic theories, I mean the theories of arithmetic according to "Logical Foundations of Proof Complexity", which capture the complexity classes between $AC^...
4
votes
1answer
217 views

Weak Bounded Arithmetics

Let $\Sigma^b_i$ and $\Pi^b_i$ formulas be bounded formulas defined by Buss in language of $L_b$. $PIND(\phi(x))$ is the formula: $$\phi(0)\land \forall x(\phi(\left \lfloor \frac{x}{2} \right \...
12
votes
1answer
480 views

Intutionistic Robinson Arithmetic

By Friedman translation $HA$ and $PA$ prove the same $\Pi_2$ formulas. Is it true for Intutionistic Robinson arithmetic(Robinson axioms with intutionistic logic) and classic Robinson arithmetic? ...
1
vote
0answers
82 views

models of $I\exists^+_1$

$\phi$ is a $\exists^+_1$ formula iff it is in language of arithmetic and does not have $\forall$,$\neg$ and $\rightarrow$, therefore $I\exists^+_1$ is theory of $Q$+induction axioms for $\exists^+_1$ ...
7
votes
0answers
120 views

Does every model of $I\Delta_0$ has an end extension to a model of $I\Delta_0+\Omega_1$?

Does every model of $I\Delta_0$ has an end extension to a model of $I\Delta_0+\Omega_1$? In End extensions of models of linearly bounded arithmetic paper the author said this problem is open. I want ...
8
votes
0answers
160 views

Kripke models of $HA$

Let $K$ be a kripke model and $k$ be one of its node, then $\mathcal{M}_k$ is classical structure of $k$. What is the strongest theory of arithmetic like $T$ such that for every kripke model $K\...
4
votes
3answers
281 views

End Extension models of $I\Delta_0$

Recently I'm thinking about question below, but I can not prove or disprove it. Is it true that for every model $M\models I\Delta_0$ there exists a model $M'\models PA$ such that $M'$ is end ...
9
votes
3answers
458 views

Model-theoretic accounts of feasibility in bounded arithmetic and related systems

Various weak theories of arithmetic have been partially motivated by a concern with numbers (or functions/proofs) that are feasible. This concern is sometimes connected to an interest in strictly ...
14
votes
2answers
630 views

Unboundedness of primes in bounded arithmetic

Wilkie's well known question asks whether $I\Delta_{0}$ proves the unboundedness of primes. We know that by adding a sentence to $I\Delta_{0}$ which says "the exponential function is total", it is ...
6
votes
1answer
323 views

Is there exponentiation in “sufficiently large” models of $I\Delta_{0}$?

Let $L_{E}$ be the language of discretely ordered rings together with an extra predicate symbol $E$. The system $A$ consists of the axioms of $I\Delta_{0}$ (basic arithmetic plus induction for bounded ...