Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Löb-Safe Logics for Reflective Agents

Seth Ahrenbach

TL;DR

The paper investigates reflective agents within epistemic/doxastic logics and shows that standard logics such as $S5$ and $KD45$ crash under Löb's Obstacle when self-reference is expressible, formalized by $\Box(\Box\varphi \Rightarrow \varphi) \Rightarrow \Box\varphi$. It introduces two Löb-Safe multimodal systems, $LSED^R$ (Reasonable Löb-Safe Epistemic Doxastic logic) and $LSED^S$ (Supported Löb-Safe Epistemic Doxastic logic), which reconfigure belief and knowledge modalities to avoid deriving Löb's Theorem while preserving truth-entailing knowledge and evidence-based belief. The authors prove soundness and completeness for these logics via the Sahlqvist correspondence and argue their suitability for human-like agents facing real-world uncertainty, with potential implications for AI foundations and game-theoretic modeling. They also discuss alternative approaches, such as Critch's bounded Löb in provability logic, as complementary directions for enabling cooperation without sacrificing safety in reflective reasoning.

Abstract

Epistemic and doxastic logics are modal logics for knowledge and belief, and serve as foundational models for rational agents in game theory, philosophy, and computer science. We examine the consequences of modeling agents capable of a certain sort of reflection. Such agents face a formal difficulty due to Löb's Theorem, called Löb's Obstacle in the literature. We show how the most popular axiom schemes of epistemic and doxastic logics suffer from Löb's Obstacle, and present two axiom schemes that that avoid Löb's Obstacle, which we call Reasonable Löb-Safe Epistemic Doxastic logic (${LSED}^R$) and Supported Löb-Safe Epistemic Doxastic logic (${LSED}^S$).

Löb-Safe Logics for Reflective Agents

TL;DR

The paper investigates reflective agents within epistemic/doxastic logics and shows that standard logics such as and crash under Löb's Obstacle when self-reference is expressible, formalized by . It introduces two Löb-Safe multimodal systems, (Reasonable Löb-Safe Epistemic Doxastic logic) and (Supported Löb-Safe Epistemic Doxastic logic), which reconfigure belief and knowledge modalities to avoid deriving Löb's Theorem while preserving truth-entailing knowledge and evidence-based belief. The authors prove soundness and completeness for these logics via the Sahlqvist correspondence and argue their suitability for human-like agents facing real-world uncertainty, with potential implications for AI foundations and game-theoretic modeling. They also discuss alternative approaches, such as Critch's bounded Löb in provability logic, as complementary directions for enabling cooperation without sacrificing safety in reflective reasoning.

Abstract

Epistemic and doxastic logics are modal logics for knowledge and belief, and serve as foundational models for rational agents in game theory, philosophy, and computer science. We examine the consequences of modeling agents capable of a certain sort of reflection. Such agents face a formal difficulty due to Löb's Theorem, called Löb's Obstacle in the literature. We show how the most popular axiom schemes of epistemic and doxastic logics suffer from Löb's Obstacle, and present two axiom schemes that that avoid Löb's Obstacle, which we call Reasonable Löb-Safe Epistemic Doxastic logic () and Supported Löb-Safe Epistemic Doxastic logic ().
Paper Structure (11 sections, 7 theorems, 4 equations, 2 figures, 5 tables)

This paper contains 11 sections, 7 theorems, 4 equations, 2 figures, 5 tables.

Table of Contents

  1. Introduction
  2. Löb's Theorem
  3. Epistemic Logics that Crash
  4. $\mathcal{S}$5 Epistemic Logic
  5. Hintikka's S4 Epistemic Logic
  6. Kraus and Lehmann System
  7. $\mathcal{KD}$45 Doxastic Logic
  8. Analysis
  9. Avoiding Löb
  10. An Alternative Approach
  11. Conclusion

Key Result

theorem 1

A logic $\mathcal{L}$ that crashes is unsound.

Figures (2)

  • Figure 1: A counterexample to $\mathbf{B}_{\mathbf{i}}\,\varphi{\ \Rightarrow \ }\mathbf{B}_{\mathbf{i}}\,\mathbf{B}_{\mathbf{i}}\,\varphi$.
  • Figure 2: A counterexample to $\mathbf{B}_{\mathbf{i}}\,(\mathbf{B}_{\mathbf{i}}\,\varphi {\ \Rightarrow \ } \varphi) {\ \Rightarrow \ } \mathbf{B}_{\mathbf{i}}\,\varphi$.

Theorems & Definitions (15)

  • definition thmcounterdefinition
  • theorem 1
  • proof : Proof.
  • theorem 2
  • proof : Proof.
  • theorem 3
  • proof : Proof.
  • theorem 4: Consistency Disaster
  • definition thmcounterdefinition
  • theorem 5
  • ...and 5 more