U-S时态逻辑

通过引入二元时态算子U(直至)和S(自从)以及相应的公理和规则对经典逻辑进行扩充所得到的时态逻辑系统。对U-S系统的研究源自于对一元时态算子G-H表达能力的考察。在经典逻辑中，联结词和→构成一完备集，而在时态逻辑中｛G，H｝却不具备表达完全性。研究表明，｛U，S｝是表达能力更强的算子集。1968年，J．凯普证明：在连续的时间结构中，｛U，S｝表达完全。1982年，J．P．波杰斯发表著名论文《时态逻辑公理I，“自从”和“直至”》，提出了一系列关于线性时间的U-S时态逻辑，并且证明了所建立的诸U-S时态逻辑的完全性。后来，还建立了极小的US时态逻辑。

U-S时态逻辑系统U-S时态公式(简称公式)是由命题变项p，q，r，s，……使用联结词、→以及二元时态算子U，S构成。其中，U(p，q)读作“直至p，q”，S(p，q)读作“自从p，q”。(常项真)，⊥(常项假)，∨，∧，和一元时态算子F、P、G、H可以作为缩写引入。α，β，γ，……是以公式为辖域的元变项。

一个U-S时态逻辑是满足下述两个条件的公式集TL：①包含所有经典逻辑的重言式以及公式

1．G(p→q)→(U(p，r)→U(q，r))∧(U(r，p)→U(r，q))

2．H(p→q)→(S(p，r)→S(q，r))∧(S(r，p)→S(r，q))

3．p∧U(q，r)→U(q∧S(p，r)，r)

4．p∧S(q，r)→S(q∧U(p，r)，r)

②在代入规则、分离规则和时间概括规则(即从┝α推出┝Ga，┝Ha)下封闭。每一U-S时态逻辑也在等值置换规则下封闭。

U-S时态逻辑语义 框架J是一有序偶(T，＜)，其中T是时间点的非空集，＜是T上的二元关系即通常的先后关系。框架J上的一个赋值是给每一命题变项指派T的子集的任何函项V。对于框架J上的赋值V、公式α和T的元素t，(J，V)α［t］(读作“α在模型(J，V)中的t上真”)可递归定义如下：

①(J，V)p［t］当且仅当，对于每一命题变项p，t∈V(p)

②(J，V)β［t］当且仅当(．J，V)β［t］(即并非(J，V)β［t］)

③(J，V)β→γ［t］当且仅当，若(J，V)β［t］则(J，V)γ［t］

④(J，V)U(β，γ)［t］当且仅当，对于某些t'∈T且t＜t＇，(J，V)β［t'］；并且对于每一t″∈T且t＜t″且t″＜t'，(J，V)γ［t″］

⑤(J，V)S(β，γ)［t］当且仅当，对于某些t＇∈T且t＇＜t，(J，V)β［t'］；并且对于每一t″∈T且t'＜t″且t″＜t，(J，V)γ［t″］

如果(J，V)α［t］对于每一t∈T且．J上的每一赋值V成立，则称α对于J是有效的，用Jα表示。令∑是一公式集，J∑则表示Jα对于每一α∈∑成立。如果对于每一个J，只有Jα，才J∑，则称α是∑的语义后承。令TL(∑)表示包含公式集∑的最小US时态逻辑，对于任意公式集∑，对于每－公式α，若∑α当且仅当α∈TL(∑)，则称TL(∑)是完全的。