What question did this study set out to answer?

The goal is to create a first-order version of T-BAT logic to align with informal provability concepts.

May 16, 2026

Nondeterministic first-order T-BAT logic

Key Points

The goal is to create a first-order version of T-BAT logic to align with informal provability concepts.
Extending the existing T-BAT logic framework to a first-order system
Investigating the implications of this extension on provability
Analyzing the relationship between formal and informal provability
Establishes a new formal system that captures informal provability
Demonstrates the applicability of reflection schema in the new framework
Fills a critical gap in the existing literature on T-BAT logic

Abstract

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.

Bookmark

Nondeterministic first-order T-BAT logic

Key Points

Abstract

Cite This Study

Also Consider

Also Consider