动态拓扑逻辑的非有限公理化
逻辑
2012-07-24 v1 计算机科学中的逻辑
摘要
动态拓扑逻辑（DTL）是一种多模态逻辑，旨在对{\em 动态拓扑系统}进行推理。这些系统是序对 ，其中 是一个拓扑空间， 是连续映射。DTL 使用的语言 结合了拓扑 S4 模态 与来自线性时序逻辑的时序算子。最近，我为该逻辑扩展到语言 给出了一个可靠且完备的公理化系统 DTL*，其中 允许作用于公式的有限集，并被解释为纠缠闭包算子（tangled closure operator）。目前尚不知晓针对 的完备公理化，尽管 Kremer 和 Mints 曾猜想一个称为 的证明系统是完备的。在本文中，我们表明，对于 和 之间的任何语言 ， 的有效公式集都不是有限公理化的。由此特别可知， 是不完备的。
引用
@article{arxiv.1207.5140,
title = {Non-finite axiomatizability of Dynamic Topological Logic},
author = {David Fernández-Duque},
journal= {arXiv preprint arXiv:1207.5140},
year = {2012}
}
备注
arXiv admin note: text overlap with arXiv:1201.5162 by other authors