Questions tagged [bounded-arithmetic]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
4 votes
1 answer
102 views

Does this hierarchy of fragments of $I \Sigma_1$ collapse?

Does anyone know whether the following hierarchy of fragments of $\mathrm{I} \Sigma_1$ (or rather $\mathrm{I} \Pi_1$) collapses or not? Let $\Sigma^b_n$ denote formulas in the language of arithmetic ...
Lukas Holter Melgaard's user avatar
1 vote
0 answers
162 views

Induction on open formulas vs. Induction on $\Pi_1$ formulas

There are infinitely many extension to Robinson's $Q$ arithmetic many of which are defined by adding an axiom schema of induction for particular set of formulas. I am confused about the theory $\text{...
Punga's user avatar
  • 173
5 votes
0 answers
249 views

Finite axiomatizability and $\mathrm{PA^{top}}$

Is $\mathrm{PA^{top}}$ finitely axiomatizable? If not, does it have a finitely axiomatizable extension (allowing new predicates but not new variable types) that has arbitrarily large finite models? $\...
Dmytro Taranovsky's user avatar
6 votes
1 answer
694 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 ...
Zuhair Al-Johar's user avatar
6 votes
1 answer
276 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 ...
Dmytro Taranovsky's user avatar
0 votes
0 answers
215 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 ...
Frode Alfson Bjørdal's user avatar
6 votes
1 answer
167 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 ...
Erfan Khaniki's user avatar
5 votes
0 answers
123 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 the ...
Erfan Khaniki's user avatar
3 votes
1 answer
121 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, ...
Erfan Khaniki's user avatar
2 votes
1 answer
214 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 ...
Erfan Khaniki's user avatar
2 votes
0 answers
191 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 ...
Erfan Khaniki's user avatar
10 votes
0 answers
255 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 ...
Erfan Khaniki's user avatar
3 votes
0 answers
62 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 $...
Erfan Khaniki's user avatar
10 votes
2 answers
596 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^...
John's user avatar
  • 103
4 votes
1 answer
279 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 \...
Erfan Khaniki's user avatar
13 votes
1 answer
661 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? ...
Erfan Khaniki's user avatar
1 vote
0 answers
87 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$ ...
Erfan Khaniki's user avatar
8 votes
0 answers
135 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 ...
Erfan Khaniki's user avatar
8 votes
0 answers
193 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\...
Erfan Khaniki's user avatar
4 votes
3 answers
347 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 ...
Erfan Khaniki's user avatar
9 votes
3 answers
596 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 ...
SiS's user avatar
  • 91
14 votes
2 answers
689 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 ...
shahram's user avatar
  • 1,438
8 votes
1 answer
417 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 ...
M Carl's user avatar
  • 521