T-BAT semantics and its logics
Pawel Pawlowski
TL;DR
The paper addresses the distinction between formal provability and informal mathematical practice, proposing $T$-BAT as a four-valued non-deterministic semantics to capture truth and provability status. It develops the four-valued framework for the language $\mathcal{L}=\{Var,\neg,\rightarrow,\Box\}$ using Nmatrices, and analyzes the definable logics around $T$-BAT through both semantic (Nmatrix and Kripke frame) and syntactic (axiomatization) methods. A key contribution is the completeness result achieved by translating truth values into object-language expressions and by establishing corresponding frame conditions, including a detailed exploration of axiom schemes and their modal implications. The paper also provides an explicit axiomatization of $T$-BAT distinct from $\mathsf{S4}^-$, clarifying the landscape of logics near informal provability and outlining open questions about a robust characterization of informal provability and its possible relationship to sublogics of $S5$. Overall, it advances a principled, semantically rich approach to modeling informal mathematical reasoning within modal and non-deterministic frameworks, with potential implications for the analysis of informal provability in arithmetic and logic.
Abstract
\textbf{T-BAT} logic is a formal system designed to express the notion of informal provability. This type of provability is closely related to mathematical practice and is quite often contrasted with formal provability, understood as a formal derivation in an appropriate formal system. \textbf{T-BAT} is a non-deterministic four-valued logic. The logical values in \textbf{T-BAT} semantics convey not only the information whether a given formula is true but also about its provability status. The primary aim of our paper is to study the proposed four-valued non-deterministic semantics. We look into the intricacies of the interactions between various weakenings and strengthenings of the semantics with axioms that they induce. We prove the completeness of all the logics that are definable in this semantics by transforming truth values into specific expressions formulated within the object language of the semantics. Additionally, we utilize Kripke semantics to examine these axioms from a modal perspective by providing a frame condition that they induce. The secondary aim of this paper is to provide an intuitive axiomatization of \textbf{T-BAT} logic.