One of the elegant achievements in the history of proof theory is the characterization of the provably total recursive functions of an arithmetical theory by its proof-theoretic ordinal as a way to measure the time complexity of the functions. Unfortunately, the machinery is not sufficiently fine-grained to be applicable on the weak theories, on the one hand and to capture the bounded functions with bounded definitions of strong theories, on the other. In this paper, we develop such a machinery to address the bounded theorems of both strong and weak theories of arithmetic. In the first part, we provide a refined version of ordinal analysis to capture the feasibly definable and bounded functions that are provably total in $\textrm{PA}+\bigcup _{\beta \prec \alpha } \textrm{TI}({\prec_{\beta}})$, the extension of Peano arithmetic by transfinite induction up to the ordinals below $\alpha$. Roughly speaking, we identify the functions as the ones that are computable by a sequence of $\textrm{PV}$-provable polynomial time modifications on an initial polynomial time value, where the computational steps are indexed by the ordinals below $\alpha$, decreasing by the modifications. In the second part, and choosing $l \leq k$, we use similar technique to capture the functions with bounded definitions in the theory $T^k_2$ (resp. $S^k_2$) as the functions computable by exponentially (resp. polynomially) long sequence of $\textrm{PV}_{k-l +1}$-provable reductions between $l$-turn games starting with an explicit $\textrm{PV}_{k-l +1}$-provable winning strategy for the first game.

Cook and Reckhow [5] pointed out that $\mathcal {N}\mathcal {P} \neq co\mathcal {N}\mathcal {P}$ iff there is no propositional proof system that admits polynomial size proofs of all tautologies. The theory of proof complexity generators aims at constructing sets of tautologies hard for strong and possibly for all proof systems. We focus on a conjecture from [16] in foundations of the theory that there is a proof complexity generator hard for all proof systems. This can be equivalently formulated (for p-time generators) without a reference to proof complexity notions as follows:

• • There exists a p-time function g stretching each input by one bit such that its range $rng(g)$ intersects all infinite $\mathcal {N}\mathcal {P}$ sets.

$\bigvee $

$\bigvee $

$\mathcal {N}\mathcal {P}$

$\mathcal {N}\mathcal {P}$

This article presents a proof that Buss’s $S_2^2$ can prove the consistency of a fragment of Cook and Urquhart’s PV from which induction has been removed but substitution has been retained. This result improves Beckmann’s result, which proves the consistency of such a system without substitution in bounded arithmetic $S_2^1$.

Our proof relies on the notion of “computation” of the terms of PV. In our work, we first prove that, in the system under consideration, if an equation is proved and either its left- or right-hand side is computed, then there is a corresponding computation for its right- or left-hand side, respectively. By carefully computing the bound of the size of the computation, the proof of this theorem inside a bounded arithmetic is obtained, from which the consistency of the system is readily proven.

This result apparently implies the separation of bounded arithmetic because Buss and Ignjatović stated that it is not possible to prove the consistency of a fragment of PV without induction but with substitution in Buss’s $S_2^1$. However, their proof actually shows that it is not possible to prove the consistency of the system, which is obtained by the addition of propositional logic and other axioms to a system such as ours. On the other hand, the system that we have considered is strictly equational, which is a property on which our proof relies.

This article bears on four topics: observational predicates and phenomenal properties, vagueness, strict finitism as a philosophy of mathematics, and the analysis of feasible computability. It is argued that reactions to strict finitism point towards a semantics for vague predicates in the form of nonstandard models of weak arithmetical theories of the sort originally introduced to characterize the notion of feasibility as understood in computational complexity theory. The approach described eschews the use of nonclassical logic and related devices like degrees of truth or supervaluation. Like epistemic approaches to vagueness, it may thus be smoothly integrated with the use of classical model theory as widely employed in natural language semantics. But unlike epistemicism, the described approach fails to imply either the existence of sharp boundaries or the failure of tolerance for soritical predicates. Applications of measurement theory (in the sense of Krantz, Luce, Suppes, & Tversky (1971)) to vagueness in the nonstandard setting are also explored.

The relativized weak pigeonhole principle states that if at least 2n out of n2 pigeons fly into n holes, then some hole must be doubly occupied. We prove that every DNF-refutation of the CNF encoding of this principle requires size $2^{\left( {{\rm{log\ }}n} \right)^{3/2 - \varepsilon } } $ for every ε﹥0 and every sufficiently large n. By reducing it to the standard weak pigeonhole principle with 2n pigeons and n holes, we also show that this lower bound is essentially tight in that there exist DNF-refutations of size $2^{\left( {{\rm{log\ }}n} \right)^{O\left( 1 \right)} } $ even in R(log). For the lower bound proof we need to discuss the existence of unbalanced low-degree bipartite expanders satisfying a certain robustness condition.

We study the long-standing open problem of giving $\forall {\rm{\Sigma }}_1^b$ separations for fragments of bounded arithmetic in the relativized setting. Rather than considering the usual fragments defined by the amount of induction they allow, we study Jeřábek’s theories for approximate counting and their subtheories. We show that the $\forall {\rm{\Sigma }}_1^b$ Herbrandized ordering principle is unprovable in a fragment of bounded arithmetic that includes the injective weak pigeonhole principle for polynomial time functions, and also in a fragment that includes the surjective weak pigeonhole principle for FPNP functions. We further give new propositional translations, in terms of random resolution refutations, for the consequences of $T_2^1$ augmented with the surjective weak pigeonhole principle for polynomial time functions.

We show how to formalize approximate counting via hash functions in subsystems of bounded arithmetic, using variants of the weak pigeonhole principle. We discuss several applications, including a proof of the tournament principle, and an improvement on the known relationship of the collapse of the bounded arithmetic hierarchy to the collapse of the polynomial-time hierarchy.

We develop approximate counting of sets definable by Boolean circuits in bounded arithmetic using the dual weak pigeonhole principle (dWPHP(PV)), as a generalization of results from [15]. We discuss applications to formalization of randomized complexity classes (such as BPP, APP, MA, AM) in PV1 + dWPHP(PV).

The use of Nepomnjaščiǐ's Theorem in the proofs of independence results for bounded arithmetic theories is investigated. Using this result and similar ideas, it is shown that at least one of S1 or TLS does not prove the Matiyasevich-Robinson-Davis-Putnam Theorem. It is also established that TLS does not prove a statement that roughly means nondeterministic linear time is equal to co-nondeterministic linear time. Here S1 is a conservative extension of the well-studied theory IΔ0 and TLS is a theory for LOGSPACE reasoning.