On Use of an Explicit Congruence Predicate in Bounded Arithmetic

TL;DR

This paper introduces a new bounded arithmetic system S^2_0E with an explicit existence predicate, demonstrating its properties and consistency, and exploring its interpretative power relative to other systems.

Contribution

The paper defines the system S^2_0E with an explicit existence predicate and proves its consistency within a stronger system, advancing the understanding of bounded arithmetic frameworks.

Findings

S^2_0E can define truthness in _2

Consistency of S^2_0E is provable in S^2_2

Conjecture: S^2_0E + _1-PIND interprets S^2_1

Abstract

We introduce system S^2_0E, a bounded arithmetic corresponding to Buss's S^2_0 with the predicate E which signifies the existence of the value. Then, we show that we can \Sigma^b_2-define truthness of S^2_0 E and therefore we can prove consistency of S^2_0 E in S^2_2. Finally, we conjecture that S^2_0 E + \Sigma^b_1-PIND interprets S^2_1.