\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.

翻译：**T-BAT**逻辑是一种旨在表达非形式可证性概念的形式系统。这类可证性与数学实践密切相关，且常与形式可证性（理解为在适当形式系统中的形式推导）形成对比。**T-BAT**是一种非确定性四值逻辑。其语义中的逻辑值不仅传递给定公式是否为真的信息，还揭示其可证性状态。本文的主要目标是研究所提出的四值非确定性语义。我们深入探究该语义的各种弱化与强化变体与其所导出公理之间相互作用的复杂性。通过将真值转换为语义对象语言内表述的特定表达式，我们证明了所有在该语义中可定义逻辑的完备性。此外，我们借助克里普克语义，通过提供这些公理所导出的框架条件，从模态视角审视这些公理。本文的次要目标是为**T-BAT**逻辑提供一种直观的公理化体系。