Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Guarded Successor: A Novel Temporal Logic

Ohad Asor

TL;DR

This work introduces Guarded Successor (GS), a decidable temporal logic that operates over infinite data values from the theory of atomless Boolean algebras and distinguishes inputs from outputs, with a decision procedure for a universal-to-existential property at every time step. It develops NSO, a non-temporal fragment that can internalize sentences as BA elements, enabling self-referential reasoning while preserving decidability via Lindenbaum–Tarski algebra techniques. A comprehensive theory of atomless Boolean algebras is built, including quantifier elimination, minterm normal forms, and Boole–Hall machinery, to support recurrence-augmented reasoning and the new temporal framework. The paper then defines GSSOTC, a time-compatible, guarded-succesor temporal logic that supports bounded lookback via recurrence relations, and demonstrates a decidable procedure for Satisfiability and execution that directly applies to software specification and AI safety, with complexity bounded by triple-exponential factors in the number of free variables. Overall, the combination of atomless-BA theory, NSO, and GSSOTC yields a novel, executable, and safety-oriented logical framework for reasoning about programs and updates that can reason about its own sentences and iterations over time.

Abstract

We present GS (Guarded Successor), a novel decidable temporal logic with several unique distinctive features. Among those, it allows infinitely many data values that come not only with equality but with a somehow rich theory too: the first-order theory of atomless Boolean algebras. The language also distinguishes between inputs and outputs, and has a decision procedure for determining whether for all inputs exist outputs, at each point of time. Moreover, and maybe most surprisingly, the data values can be nothing but sentences in GS itself. We also present a non-temporal fragment called NSO (Nullary Second Order) that enjoys merely this last property. These results are crucial necessary ingredients in any meaningful design of safe AI. Finally, all those results are obtained from a novel treatment of the first-order theory of atomless Boolean algebras.

Guarded Successor: A Novel Temporal Logic

TL;DR

This work introduces Guarded Successor (GS), a decidable temporal logic that operates over infinite data values from the theory of atomless Boolean algebras and distinguishes inputs from outputs, with a decision procedure for a universal-to-existential property at every time step. It develops NSO, a non-temporal fragment that can internalize sentences as BA elements, enabling self-referential reasoning while preserving decidability via Lindenbaum–Tarski algebra techniques. A comprehensive theory of atomless Boolean algebras is built, including quantifier elimination, minterm normal forms, and Boole–Hall machinery, to support recurrence-augmented reasoning and the new temporal framework. The paper then defines GSSOTC, a time-compatible, guarded-succesor temporal logic that supports bounded lookback via recurrence relations, and demonstrates a decidable procedure for Satisfiability and execution that directly applies to software specification and AI safety, with complexity bounded by triple-exponential factors in the number of free variables. Overall, the combination of atomless-BA theory, NSO, and GSSOTC yields a novel, executable, and safety-oriented logical framework for reasoning about programs and updates that can reason about its own sentences and iterations over time.

Abstract

We present GS (Guarded Successor), a novel decidable temporal logic with several unique distinctive features. Among those, it allows infinitely many data values that come not only with equality but with a somehow rich theory too: the first-order theory of atomless Boolean algebras. The language also distinguishes between inputs and outputs, and has a decision procedure for determining whether for all inputs exist outputs, at each point of time. Moreover, and maybe most surprisingly, the data values can be nothing but sentences in GS itself. We also present a non-temporal fragment called NSO (Nullary Second Order) that enjoys merely this last property. These results are crucial necessary ingredients in any meaningful design of safe AI. Finally, all those results are obtained from a novel treatment of the first-order theory of atomless Boolean algebras.
Paper Structure (16 sections, 21 theorems, 10 equations)

This paper contains 16 sections, 21 theorems, 10 equations.

Table of Contents

  1. Introduction
  2. NSO
  3. GS
  4. The Theory of Atomless Boolean Algebras
  5. Boolean Functions and Equations
  6. Quantifier Elimination in Atomless BAs
  7. Number of Formulas
  8. Recurrence Relations
  9. NSO: Nullary Second Order Logic
  10. GSSOTC: A Temporal Logic
  11. Time-Compatible Structures
  12. Bounded Lookback and Recurrence Relations
  13. Guarded Successor
  14. Decision Methods and Execution
  15. Complexity
  16. ...and 1 more sections

Key Result

Theorem 4

A function $\mathcal{B}^{n}\rightarrow\mathcal{B}$ is a BF iff it can be written in minterm normal form $f\left(X\right)=\bigcup_{A\in\left\{ 0,1\right\} ^{n}}f\left(A\right)X^{A}$.

Theorems & Definitions (46)

  • Definition 1
  • Definition 2
  • Definition 3
  • Theorem 4
  • Corollary 5
  • Theorem 6
  • Theorem 7
  • Definition 8
  • Theorem 9
  • Remark 10
  • ...and 36 more