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.

翻译：本文提出GS（受保护的后续），一种具有若干独特特征的新型可判定时序逻辑。该逻辑不仅允许使用无限多数据值，且这些数据值不仅支持相等性比较，还具备较为丰富的理论结构：即无原子布尔代数的一阶理论。该语言同时区分输入与输出，并提供了决策过程以判定在每个时间点上是否对所有输入均存在相应输出。此外，或许最令人惊讶的是，数据值本身可以完全由GS语言中的语句构成。我们还提出一种称为NSO（零元二阶逻辑）的非时序逻辑片段，该片段仅具备最后这一特性。这些成果对于任何具有实际意义的安全人工智能设计而言都是不可或缺的关键要素。最后，所有结论均源于对无原子布尔代数一阶理论的全新处理方法。