Awodey 和 Forssell 的另一种近路则更加靠近我们原本拓扑的想法。由于对于一阶的情形(如我们前面所说,他们实际考虑的是等号可判定的连贯逻辑,但所有的经典一阶逻辑系统都可以通过某种构造转化成一个这样的连贯逻辑系统使得它们的模型等价)Mod(𝕋) 的信息包含模型和它们之间的态射两部分,Awodey 和 Forssell 便使用了拓扑广群 [topological groupoid] 的方式,在所有的模型和模型之间的同构(这里由于他们考虑的是广群,因此只考虑了模型之间的同构而没有考虑更为一般的态射)上都赋予了拓扑使得它们称为两个拓扑空间,同时同构构成的空间对模型空间有两个连续作用 [continuous action] 使得它们构成拓扑空间这个范畴内的内涵广群 [internal groupoid]。但他们的工作显示即使有这样拓扑广群的信息仍是无法重构出语形范畴的信息,还必须考虑其上的等变层 [equivalent sheaf]。最终,他们依据这两部分的信息还原的并不是原本的语形范畴 C𝕋,而是 𝕋 的分类拓扑斯 [classifying topos] Set[𝕋] 。 Set[𝕋] 是 𝕋 在拓扑斯中的对应:即任意具有一定结构的范畴 D 中的 𝕋 模型等价于 C𝕋 到 D 的保持某种结构的函子, 𝕋 在任意拓扑斯 ε 中的模型等价于从 ε 到 Set(𝕋) 的几何函子 [geometric morphism](这里之所以方向反过来了是因为我们采用了几何函子来描述)。Awodey 和 Forssell 所得到的对偶也就和一般拓扑斯的拓扑广群表示具有很深的联系。
在最后我们不过多地介绍拓扑斯的理论和其与逻辑紧密的联系了,感兴趣的读者可以参考[10][11],仅仅简单地说一说拓扑斯是什么。如果用一句话简单地概括,拓扑斯是那些可以在其中解释构造集合论 [constructive set theory] 的范畴;换而言之,拓扑斯是一类具有非常丰富结构的范畴使得所有集合论中构造性的原则和操作都能在其中实现。一个较为粗略的直观是,拓扑斯描述的是时态的集合,即其中的对象是随时间变动的集合,而在我们一般的 Set 中可以理解为是静态的集合。当然,这里的时间显然不是仅仅指物理中用实数指代的时间;任何一个图甚至任何一个范畴都可以作为此处广义的“时间”。如果读者熟悉直觉主义逻辑的模态语义,想必不会对在时态集合上的逻辑是直觉主义的而不是经典的感到惊讶;事实上,拓扑斯的结构正是 Kripke 所采用的构造主义数学的语义结构。
结语
在考虑一阶逻辑的语形语义对偶时,所用到的数学理论和工具已经非常的艰深了,想要读懂与理解目前已有的文献已经不是一件容易的事,并且根据上面的描述可见,对于一阶情形对偶的研究并不只有一种进路和描述方式,且就目前来看,在笔者有限的认识下并没有唯一一种描述方式得到了大家普遍的认可。但对于笔者而言,语形与语义对偶的这个观念一定是一个非常深刻的指导原则,目前已有的结论也可以看作对这个观念很大程度的印证。我们需要的或许是找到更好的语言和描述方式来看待模型层面的结构,最终使得在一阶的情形下也和命题逻辑中的 Stone 对偶一样清晰、简洁、自然。完成这个目标自然是需要大家共同的努力了!
参考:
1. Johnstone, P. T. (1982). Stone spaces (Vol. 3). Cambridge university press.
数学联邦政治世界观提示您:看后求收藏(同人小说网http://tongren.me),接着再看更方便。