T-BAT Semantics and Its Logics

Basic Information

• Paper ID: 2510.14361
• Title: T-BAT semantics and its logics
• Author: P. Pawlowski
• Classification: cs.LO (Computer Science - Logic)
• Publication Time/Venue: Logique et Analyse 264 (2023), 335–356
• Paper Link: https://arxiv.org/abs/2510.14361

Abstract

T-BAT logic is a formal system designed to express the concept of informal provability. This provability is closely related to mathematical practice and frequently contrasts with formal provability, understood as formal derivation in an appropriate formal system. T-BAT is a non-deterministic four-valued logic. The logical values in T-BAT semantics convey not only whether a given formula is true, but also its provability status. The primary objective of this paper is to investigate the proposed four-valued non-deterministic semantics, exploring in depth the complexities of interactions between various weakenings and strengthenings of the semantics and the axioms they induce. Completeness of all logics definable in this semantics is established by translating truth values into specific expressions formulated in the semantic object language. Furthermore, these axioms are examined from a modal perspective using Kripke semantics, providing the framework conditions they induce. A secondary objective of the paper is to provide an intuitive axiomatization of T-BAT logic.

Research Background and Motivation

Problem Definition

The core problem this research addresses is how to formally express the concept of "informal provability" in mathematics. Two distinct concepts of provability exist in mathematical practice:

1. Formal Provability: A strict syntactic concept based on specific formal languages and axiomatic frameworks, conducted through finite sequences of formulas via formal derivation.
2. Informal Provability: Closely related to mathematical practice, the manner of proof actually used by mathematicians, encompassing semantic and pragmatic components.

Problem Significance

The significance of this problem manifests in several aspects:

• Formal and informal provability exhibit essential differences in reasoning behavior
• The reflection schema □φ→φ is valid in informal provability but invalid in modal logic GL, which represents formal provability
• Directly combining all instances of the reflection schema with other intuitive provability principles leads to inconsistency in first-order arithmetic theories

Limitations of Existing Approaches

The principal limitations of existing approaches include:

• Traditional modal logic GL, while accurately characterizing formal provability, cannot handle the reflection principle of informal provability
• Simply adding the reflection schema leads to theoretical inconsistency
• Lack of a refined framework capable of simultaneously handling both truth values and provability status

Research Motivation

The research motivation is to develop a theory of informal provability analogous to Kripke's truth-theoretic methodology, addressing inconsistency problems through the use of well-motivated non-classical logic as background logic.

Core Contributions

1. Proposed T-BAT four-valued non-deterministic semantics: Separates the truth status of mathematical propositions from their provability status, creating a more refined logical framework.
2. Systematically investigated various strengthenings and weakenings of the semantics: Methodologically explored different interpretations of connectives and their induced axioms.
3. Established completeness of all definable logics: Achieved completeness proofs by translating truth values into specific expressions in the object language.
4. Established connections with Kripke semantics: Provided corresponding framework conditions for various axioms, analyzing these axioms from a modal logic perspective.
5. Provided an intuitive axiomatization of T-BAT logic: Corrected errors in previous literature and provided a correct axiomatization system.

Methodology in Detail

Task Definition

The task of this paper is to provide a complete logical framework for informal provability, including:

• Defining appropriate semantic structures
• Establishing correspondence between syntax and semantics
• Proving soundness and completeness of the system

Model Architecture

Four-Valued Semantics Design

T-BAT employs four logical values to represent different states of mathematical propositions:

• P: True and provable propositions
• t: True and independent propositions (neither provable nor refutable)
• f: False and independent propositions
• R: False and refutable propositions

The designated value set is specified as D = {P, t}, reflecting the intuition of truth preservation.

Non-Deterministic Matrix (Nmatrix)

The core of T-BAT is the non-deterministic matrix MT = (ValT, DT, OT), where:

Negation Truth Table:

¬(φ) | φ
-----|----
  R  | P
  f  | t  
  t  | f
  P  | R

Modal Operator Truth Table:

□(φ) | φ
-----|-------
  P  | P
{f,R}| t
{f,R}| f
  R  | R

Implication Truth Table:

→  | P | t     | f     | R
---|---|-------|-------|---
P  | P | t     | f     | R
t  | P |{P,t}  | f     | f
f  | P |{P,t}  |{P,t}  | t
R  | P | P     | P     | P

Technical Innovations

1. Separation of Truth and Provability

Unlike traditional three-valued logics (BAT, CABAT), T-BAT further subdivides propositions that are "neither provable nor refutable" into true and false categories, achieving finer-grained classification.

2. Non-Deterministic Semantics

Through non-deterministic truth functions, T-BAT can distinguish provably equivalent formulas, providing specialized tools for investigating hyper-intensionality.

3. Systematic Axiom Derivation Method

Axioms are systematically derived by directly translating the meaning of truth values into formulas in the object language. For example, for the first row of negation:

• If v(φ) = P, then v(¬φ) = R
• Translates to the axiom: □φ→□¬¬φ

Experimental Setup

Theoretical Verification Methods

The paper primarily employs theoretical proof methods, including:

1. Soundness Proofs: Established through induction on formula complexity
2. Completeness Proofs: Based on maximal consistent sets and valuation lemmas
3. Axiom Equivalence Proofs: Establishing equivalence relations between different axiom systems

Comparative Analysis

The paper compares T-BAT with the following systems:

• Modal logic GL (formal provability)
• Modal logics S4, S5
• Previous BAT and CABAT systems
• Omori and Skurt's S4⁻ system

Experimental Results

Main Theoretical Results

1. Completeness of Minimal Logic W

Theorem 1 (Soundness): For any Γ, φ, if Γ ⊢W φ, then Γ ⊨W φ.

Theorem 2 (Completeness): Γ ⊨W φ if and only if Γ ⊢W φ.

2. Axiomatization of T-BAT Logic

T-BAT logic is characterized as logic W plus the following axioms:

• N1: □φ→□¬¬φ
• N4: ¬□φ∧φ→¬□¬¬φ
• B1: □φ→□□φ
• B7: □¬φ→□¬□φ
• Multiple implication-related axioms (IPP,P, IPt,P, etc.)

3. Axiom Equivalence Results

Fact 2: Axiom ItP,t is equivalent to axiom K over W.

Framework Condition Analysis

The paper provides corresponding Kripke framework conditions for many axioms, for example:

• Axiom N3 corresponds to condition: ∀x,y xRy → x = y
• Axiom B1 corresponds to condition: transitivity
• Axiom B7 corresponds to condition: ∀x,y (xRy → ∃z (xRz ∧ yRz))

System Classification

The paper classifies the studied axioms into three categories:

1. Axioms provable in modal logic K
2. Axioms provable in T but not in K
3. Axioms not provable in S5

Related Work

History of Non-Deterministic Semantics

• 1930s: Zich and Zawirski independently developed non-deterministic semantics
• 1960s: Rescher employed non-deterministic truth functions to study implication in natural language
• Modern Development: Avron introduced the concept of non-deterministic matrices (Nmatrix), establishing a rigorous mathematical framework

Applications in Modal Logic

• Kearns and Ivlev applied non-deterministic semantics to modal logic
• Contemporary logicians further developed this theory, particularly in applications to non-normal modal logics

Research on Informal Provability

The paper builds on previous work on BAT and CABAT logical systems, particularly research by Pawlowski and Urbaniak.

Conclusions and Discussion

Main Conclusions

1. T-BAT logic provides a complete and consistent formal framework for informal provability
2. Four-valued non-deterministic semantics can precisely distinguish between truth status and provability status of mathematical propositions
3. The systematic axiom derivation method reveals deep connections between semantic strengthening and axioms
4. Not all relevant logics are sublogics of S4 or S5, which has important philosophical significance

Limitations

1. Philosophical Foundations: The concept of informal provability has not been fully operationalized, making it difficult to judge the correctness of various reasoning patterns
2. Practicality: Lack of standards for determining which T-BAT extensions apply to informal provability
3. Framework Conditions: For certain axioms, corresponding Kripke framework conditions cannot be found

Future Directions

1. Provide more substantive characterization of the concept of informal provability
2. Develop standards for judging the correctness of reasoning patterns
3. Explore the potential of T-BAT in other philosophical and mathematical applications
4. Investigate further developments of hyper-intensionality

In-Depth Evaluation

Strengths

1. Theoretical Innovation

• Proposed refined four-valued semantics, successfully separating truth values from provability status
• Developed systematic axiom derivation methodology
• Established a bridge between non-deterministic semantics and Kripke semantics

2. Mathematical Rigor

• Provided complete soundness and completeness proofs
• Systematically analyzed all possible semantic strengthenings
• Established precise mathematical correspondences

3. Philosophical Significance

• Provided new solutions to the long-standing problem of informal provability
• Revealed deep relationships between mathematical practice and formal systems

Shortcomings

1. Practical Limitations

• Limited operationalization of the concept of informal provability
• Lack of concrete guidance for practical applications

2. Technical Challenges

• Framework conditions for certain axioms remain unfound
• System complexity may limit practical application

3. Philosophical Controversy

• Philosophical debates regarding the nature of informal provability continue
• Different philosophical positions may evaluate the system differently

Impact

1. Academic Contribution

• Provided new research tools for logic and philosophy of mathematics
• Advanced the development of non-deterministic semantics theory
• Opened new directions for hyper-intensionality research

2. Theoretical Value

• Demonstrated the potential of non-classical logic in solving philosophical problems
• Provided new methods for addressing inconsistency problems

3. Reproducibility

• Provided complete mathematical definitions and proofs
• Clear methodology facilitates subsequent research

Applicable Scenarios

1. Philosophy of Mathematics Research: Particularly research on the concept of proof
2. Logic Theory: Further development of non-deterministic semantics and modal logic
3. Artificial Intelligence: Potential applications in knowledge representation and reasoning
4. Mathematics Education: Helping understand the relationship between formal and intuitive proofs

References

The paper cites 47 relevant references, covering important works in multiple fields including logic, philosophy of mathematics, and modal logic, particularly:

• Solovay's classical work on provability logic
• Theoretical developments by Avron and others on non-deterministic matrices
• Kripke's methodology on truth theory
• The author's previous research on BAT logical systems

This paper provides rigorous mathematical treatment of the important philosophical problem of informal provability. While further development is needed in terms of practicality, its theoretical contributions and methodological innovations possess significant academic value.