时间逻辑（二）_数学联邦政治世界观

3.2 TL的语义

TL的标准语义基本上是克里普基风格的语义，熟悉模态逻辑。在模态逻辑中，句子通过由所谓的kripke帧进行评估，包括非空组可能的世界和它们之间的可访问性关系。在时间逻辑中，可能的世界是时间瞬间，并且可访问性关系在时间优先级方面具有具体的解释。换句话说，句子通过基于即时的时间t =⟨t，≺⟩，下文称为时间帧。请注意，到目前为止，没有条件，如传递性，反叛性等，对优先关系施加了≺。

给定一组原子命题支柱，T1的时间模型是三重M =⟨t，≺，v⟩，其中t =⟨t，≺⟩是时间帧，v：prop→p（t）是分配给每个原子的估值函数命题p∈prop这组时间瞬间v（p）⊆t，其中p被认为是真的。（等效地，估值可以通过函数i：t×prop→{true，false}，它在时间帧中的每次时刻为每个时间分配真实值，或者通过标记或状态描述l：t→p（prop），每次分配到每次即时都瞬间被认为是真实的集合。）

然后，在时间模型M（表示的M，t⊨φ）中的给定时间T处T1的任意式φ的真实性如下定义如下：

m，t⊨pifft∈v（p），用于p∈prop;

m，t⊨¬φm，t⊭φ（即，不是m，t⊨φ）的情况;

m，t⊨φ∧ψm，t⊨φ和m，t⊨ψ;

m，t⊨pφm，t'νφ一段时间即时t'这样t'ət;

m，t⊨fφm，t'əφ一段时间即时t'这样t≺t'。

也就是说，在瞬时Tφ处于某些早期的即时T'时，表单pφ的公式是真的，而Fφ在T IFFφ处为真，则在一些稍后的时刻t'是真的。因此，对于Duals H和G，我们在T IFFφ处具有真实的Hφ在所有早期瞬间T'时是真的，而Gφ在T IFFφ处于真实的瞬间t'是真的。

m，t⊨hφm，t'⊨φ，所有时间瞬间t'这样t'ət;

m，təgφffm，t'νφ，所有时间瞬间t'这样t≺t'。

请注意，从模态逻辑的角度来看，这里涉及两个不同的可访问关系：在过去的运算符的情况下，在过去的运算符和“后续关系”的情况下，“早期关系”。在时间逻辑中，这两个关系由单一优先关系涵盖; 毕竟，“早期”和“后来”只是彼此的对话（即，T比T'IFF T'早于T）。

TL的公式φ在时间模型M（表示的m⊨φ）IFF中有效，IFF在该模型中的每次时都是如此。此外，我们说φ在时间帧T（表示为t⊨φ）IFF中有效，它在该帧上的每个模型中有效。因此，公式φ有效（表示⊨φ）IFF在所有时间帧中有效，即所有时间模型的所有时间瞬间都是真实的。公式φ是满足的，IFF其否定无效，即，如果在某些时间模型中的某些时间瞬时φ是真的。

3.3 TL分为一阶逻辑的标准转换

如在模态逻辑的情况下，TL的语言和语义可以转化为经典的一阶逻辑（参见例如VAN BENTHEM 1983）。

假设TL的原子原子命题由PROP = {P0，P1，...}给出，并且L1是一种具有可降价一组的一组Unary谓词符号P = {P0，P1，...}的一阶语言，一个用于用于优先关系的TL的每个原子命题和二进制谓词符号R. T1中的标准转换ST为L1定义如下，其中θ[y / x]是替换θ的所有自由出现的结果：

圣（PI的）=的PI（x）;

圣（¬φ）=¬st（φ）;

圣（φ∧ψ）=圣（φ）∧st（ψ）;

st（pφ）=∃y（yrx∧st（φst（φ）[y / x]），其中y是一个新变量（即到目前为止一个未使用）;

ST（fφ）=∃y（xry∧st（φ）[y / x]），其中y是一个新变量。

然后跟着

圣（hφ）=∀y（yrx→圣（φ）[y / x]）;

圣（gφ）=∀y（xry→圣（φ）[y / x]）。

例如：

圣（gp1∨fhp2）=∀y（xry→p1的（y））∨∃y（xry∧∀z（zry→p2的（z）））。

不是每个一阶公式都有TL的通讯员。实际上，通过仔细重新使用变量，TL可以转换为一阶逻辑的双变量片段FO2，最终暗示可解锁性（因为FO2中的有效性是可译任的，如Grädel和奥托1999所示）。例如，上面的示例可以重写为

圣（gp1∨fhp2）=∀y（xry→p1的（y））∨∃y（xry∧∀x（xry→p2的（x）））。

鉴于标准翻译，每个时间模型M =⟨t，≺，v⟩可以被视为L1模型，其中R由v（pi）解释为≺和每个pi。然后：

m，t⊨φ。iffm⊨st（φ）[x：= t]，

m⊨φ。IFFm⊨∀xst（φ）。

因此，时间模型中TL公式的有效性是一阶属性。另一方面，时间框架中的有效性将成为二阶属性，因为它涉及估值的通用量化。如果我们从P作为谓词变量对P的二阶语言L2的谓词变量进行治疗，则每个临时帧T =⟨t，≺⟩可以被视为L2模型。我们有：

t⊨φ。ifftəp0əp1...∀xst（φ），

⊨φ。⊨∀p0∀p1...∀xst（φ）。

TL转化为一阶逻辑的标准转换使得能够通过经典逻辑的工具和技术来系统地处理时间逻辑的各个方面（参见例如Van Benthem 2001; Blackburn等，2007）。但是，由于TL有效性基本上是二阶，因此在框架可定定程度方面，也存在有趣的分歧。正如我们将在第3.6节中看到的那样，并非颞架的所有一阶属性都是可定义的时间公式; 反之亦然，并非可以由TL公式表达的时间帧的所有属性是一阶可定义。作为用于描述时间属性的替代语言，时间逻辑和一阶逻辑之间的非普通对应关系出现，请参阅例如 van Benthem（1995）。

3.4时态逻辑，一阶逻辑和MCTAGGART的时间序列

上一节中讨论的标准翻译将先前的基本时态逻辑的语义链接到一阶逻辑。然而，两种方法之间存在至关重要的差异。事实上，在颞逻辑的早期，先前的方法被认为是使用一阶逻辑的更传统方法的竞争力。时态逻辑和一阶逻辑之间的竞争可以被视为反映了关于时间性质的基本区别，即A系列与MCTAGGART引入的B系列时间之间的区别（1908）。

粗略地说，A系列在过去，现在和未来的条件下表征时间和时间顺序。相比之下，B系列基于“早期”和“后来”的概念。 MCTAGGART认为B系列不足，因为它缺乏适当的变化概念，他拒绝了一个系列，因为未来现在的未来将过去，这需要一个和同一时间即时的特性。从他那里得出结论，时间是虚幻的。有关MCTAGGART的账户及其哲学相关性的详细讨论，请参阅Ingthorsson（2016）和准时入境。

在一方面以及B系列概念和一阶逻辑之间，在另一方面和B系列概念和一阶逻辑之间，可以说是可以说的一系列密切对应，另一方面，如先前（1967，第1章）所示。考虑，例如，句子“它很亮，它很黑，它会再次光明。” 这句话可以在TL中正式化

p（光）∧dark∧f（光）

虽然它的一阶制定读

∃t0（t0≺t1∧light（t0））∧dark（t1的）∧∃t2（t1≺t2∧light（t2的））。

TL配方包括加强的命题，它调用了本地的局部视角。因此，公式的真实值随时间而变化。相比之下，一阶公式从不确的命题建立，并为所有人都有一个固定的真相价值。在这里，我们提供了时间瞬间而不是时态的谓词，并且所涉及的角度来看是一个总体，全局。事先认为，并非所有可以以趋势语言表达的一切都可以在不朽的一个中表达，他的经典举例如下：“谢天谢地，结束了！” （事先1959年）。

3.5用于TL的公理系统KT

与每个正式的逻辑系统一样，时间逻辑有两个主要方面：语义和演绎的一个。在本节中，我们为TL，VIZ提供了一项演绎系统。最小的时间逻辑Kt。我们提供的系统是Hilbert风格的公理之一，即，它包括公理列表和推理规则。该系统首先是由LEMMON研究的，遵循Hamblin和之前提出的早期公正性（参见Rescher和Urquhart 1971，第六章）。

最小时间逻辑KT的公理列表通过以下四个Axiom Schemata扩展了经典命题逻辑：

（kh）h（φ→ψ）→（hφ→hψ）

（公斤）g（φ→ψ）→（gφ→gψ）

（gp）φ→gpφ

（hf）φ→hfφ

前两个Axiom图案是模态逻辑的所谓的K-Axiom的时间记者，因此是术语Kt。第三和第四AXIOM图中捕获过去和未来运营商的互动。他们保证这些运营商利用逆转时间关系viz。早些时候分别。

除了经典的Modus Ponens之外，推理规则还包括，时间运算符的两个必要规则（其中⊢是指deftuical“）：

（MP）如果⊢φ→ψ和⊢φ，那么⊢ψ。

（Nech）如果⊢φ，那么⊢hφ。

（NECG）如果⊢φ，那么⊢gφ。

Saniomatic System Kt是Sound并完成TL的有效性：所有和只能根据规则从公理推断出TL中有效的那些公式。对于证据，见图。 Rescher和Urquhart（1971）; Mcarthur 1976; 戈尔博特（1992）; 和Gabbay等人。（1994）。

3.6表达TL和KT的延伸中的时间特性

最小的时间逻辑KT捕获TL的那些有效性，这些有效性不依赖于关于时间优先关系的属性的任何特定假设。在本节中，我们将看到时间帧的许多自然属性可以由时间公式表达，并且作为附加公式表示，这些公式通常可以用于定义时间帧相关子类上的逻辑。

如果公式中的所有帧有效，则TL表示（定义或对应于）TL表示（定义或对应）的时间公式。时间帧属性之间最重要的对应关系（见第2.1节中的列表）和TL公式包括：

（参考）任何Hφ→φ，gφ→φ，φ→pφ，或φ→fφ

（自反）

（Tran）Hφ→Hhφ，Gφ→GGφ，PPφ→Pφ，或FFφ→Fφ

（传递性）

（林-f）pfφ→（pφ∨φ∨fφ）或

fφ∧fψ→（f（φ∧ψ）∨f（fφ∧ψ）∨f（φ∧fψ））

（向前线性）

（林P）fpφ→（pφ∨φ∨fφ）或

pφ∧pψ→（p（φ∧ψ）∨p（pφ∧ψ）∨p（φ∧pψ））

（向后线性）

（林）（pfφ∨fpφ）→（pφ∨φ∨fφ）

（性度）

（求）h⊥∨ph⊥

（假设逆反射性和传递性的时间有一个开始，

（完）g⊥∨fg⊥

（时间有一端，假设逆反射和传递率）

（Nobeg）p⊤或hφ→pφ

（时间没有开始）

（正常）f⊤或gφ→fφ

（时间没有结束）

（致密）Hhφ→Hφ，GGφ→Gφ，Pφ→PPφ，或Fφ→FFφ

（密度）

（discr-f）（f⊤∧φ∧hφ）→fhφ

（前瞻性，假设前线线性）

（discr-p）（p⊤∧φ∧gφ）→pgφ

（向后离散，假设后线性度）

（成功）（fg¬φ∧fφ）→f（g¬φəhfφ）或

一个（hφ→fhφ）→（hφ→gφ）

（Defekind完整性，召回AΦ=hφ∧φ∧gφ）

（wellord）h（hφ→φ）→hφ

（与传递次数齐全）

（Fin-int）（g（gφ→φ）→（fgφ→gφ））∧（h（hφ→φ）→（phφ→hφ））

（有限间隔）

（indg）fφ∧g（φ→fφ）→gfφ

（前向诱导）

（indh）pφ∧h（φ→pφ）→hpφ

（向后诱导）

原理（LIN）在单个条件下将前线性（LIN-F）和向后线性（LIN-P）结合在一起。然而，所得到的公式是不足以保证时间框架的连接性的。换句话说，它不能排除不相交的线性时间线。此外，（Fin-int）相当于（Indh）和（Indg）的结合。注意（Indh）暗示前瞻性，（Indg）意味着向后离散，但不相反。例如，由自然数的副本组成的时间流，后跟整数副本是向后离散的，但不满足（Indg）。要查看此项，假设φ在自然数的副本上是真的，但不是在整数的副本上并在结构的初始点评估。

回想一下，上面提到的最后五个属性 - Defekind完整性，顺序齐全，有限间隔属性和前进/后向感应 - 是一阶句子的可定义。然而，它们可以用时间公式表达。另一方面，TL中的一些非常简单的一定的一阶定期属性，例如逆合尺寸或不对称，在TL中不可表示。上面列出的一些通信要求的证据可以在Goranko（2023）中找到。有关时间框架属性表现的更多结果和细节，请参阅Segerberg（1970）; Rescher和Urquhart（1971）; Burgess（1979）; 梵洁（1983; 1995年）; 戈尔博特（1992）; 和霍奇森森和雷诺兹（2007年）。

通过将KT的公理列表扩展到上述原理中的一个或几个原则，可以将各种天然模型的逻辑公开为; 也就是说，存在声音的公理扩展，并且在相关的时间帧上有效性地完成。在时间逻辑的早期已经研究了这些延伸中的一些。之前（1967）讨论了由不同组合的公理组合产生的各种系统。我们提供以下一些重要的：

K4t =。KT +（TRAN）：所有传递框架。

s4t =。KT +（REF）+（TRAN）：所有部分排序。

lt =。KT +（TRAN）+（LIN）：所有严格的线性排序。

nt =。LT +（neend）+（indg）+（wellord）或

LT +（乞求）+（neend）+（Fin-int）：⟨n，＜⟩。

zt =。LT +（NOBEG）+（neend）+（Indh）+（Indg）或

LT +（NOBEG）+（neend）+（Fin-int）：⟨z，＜⟩。

Qt =。LT +（Nobeg）+（neend）+（密集）：⟨q，＜⟩。

RT =。LT +（Nobeg）+（neend）+（致密）+（符合）：⟨r，＜⟩。

由于数字系统的公理化所示，（LIN）不足以保证连接，或者在TL中不定义不可能，不妨碍公正性（即使它需要一些操纵，参见例如Blackburn等人2001，第4章）。实际上，关联和反叛性不会产生任何新的有效性。

上述每一个逻辑都会删除可判定（即，它具有可判定的一组有效性）。通常通过证明有限型号特性显示这一点：“每个可满足的公式在有限型号中是满意的。在大多数情况下，这种证明涉及非标准型号。有关这些公理系统的（变体）的完整性以及可拆解性证明，请参阅Segerberg（1970）; Rescher和Urquhart（1971）; Burgess（1979）; Burgess和Gurevich（1985）; 戈尔博特（1992）; 和Gabbay等人。（1994）。

4.线性时间的TL扩展

基于即时的时间的自然阶级的时间是线性模型的类，并且在前面的注意力逻辑的发明内容之后，已经提出了在线性时间的若干TL的若干延伸。在本节中，我们讨论了两个这样的扩展：下一个时间运算符和运营商直到直到。然后，我们介绍了基于这些操作员的线性时间yearal逻辑LTL，并在计算机科学中具有重要应用。

4.1添加下一个时间运算符

在前行离散的线性时间模型M =⟨t，≺，v⟩没有终点，其中每个即时t都有一个唯一的立即的继承者s（t），它是自然的，添加一个新的时间运算符x（“下次”或“明天”），其中包含以下语义：[2]

m，t⊨xφiff m，s（t）⊨φ。

也就是说，Xφ在TimeT T IFFφ处于True，在T的立即继承人S（t）中是真的。下次执行操作员（1967年第IV.3章）已经提及，但在LTL的背景下首先完全赞赏其重要性。

操作员x满足K-Axiom

（kx）x（φ→ψ）→（xφ→xψ）;

和功能公理

（功能）x¬φ↔¬xφ。

它还可以实现G的递归固定点定义，并且在自然数的排序上，操作员X和G满足感应原理。假设优先关系的反身闭合≺，在计算机科学中常见，这些属性可以表示如下：

（空腹血糖）gφ↔（φ∧xgφ）;