We consider a minimal extension of the language of arithmetic, such that the bounded formulas provably total in a suitably-defined theory \`a la Buss (expressed in this new language) precisely capture polytime random functions. Then, we provide two new characterizations of the semantic class BPP obtained by internalizing the error-bound check within a logical system: the first relies on measure-sensitive quantifiers, while the second is based on standard first-order quantification. This leads us to introduce a family of effectively enumerable subclasses of BPP, called BPP_T and consisting of languages captured by those probabilistic Turing machines whose underlying error can be proved bounded in the theory T. As a paradigmatic example of this approach, we establish that polynomial identity testing is in BPP_T where T=$\mathrm{I}\Delta_0+\mathrm{Exp}$ is a well-studied theory based on bounded induction.

翻译：我们考虑算术语言的最小扩展，使得在适当定义的Buss风格理论（用这种新语言表达）中可证明全称的有界公式精确地刻画了多项式时间随机函数。然后，我们提供了语义类BPP的两种新刻画，通过将误差有界检查内化到逻辑系统中实现：第一种依赖于测度敏感量词，而第二种基于标准一阶量化。这促使我们引入BPP的一个有效可枚举子类族，称为BPP_T，它由那些其底层误差可在理论T中被证明有界的概率图灵机所识别的语言构成。作为该方法的一个范例，我们证明多项式恒等式判定属于BPP_T，其中T=$\mathrm{I}\Delta_0+\mathrm{Exp}$是一个基于有界归纳的深入研究的理论。