Nondeterministic first-order T-BAT logic

Abstract The relationship between formal and informal provability has been a significant subject of philosophical and mathematical investigation. Formal systems such as Gödel-Löb logic (GL) capture formal provability but do not validate the reflection schema—a principle stating that if a statement is provable, it must be true. This schema is intuitively valid for the informal notion of provability as understood and used in mathematical practice. Several logical systems have been developed to capture this informal notion of provability, including BAT, CABAT, and T-BAT. However, a first-order version of T-BAT logic has not yet been developed. This paper aims to address this research gap by providing such an extension.