AI 中文总结
研究双直觉逻辑语言对框架和模型的表达能力，通过提供类似戈德布拉特 - 托马森定理的结果，结合先前成果，完整刻画了命题双直觉逻辑的表达能力。
AI 中文摘要
给定具有克里普克关系语义的逻辑语言的表达能力问题至少有两个维度：一是语言对框架能表达什么，二是对模型能表达什么。戈德布拉特 - 托马森定理给出了模态可公理化的模型理论特征。戈德布拉特也为模型类的直觉主义逻辑可公理化提供了类似特征。本文为双直觉逻辑提供了类似结果，双直觉逻辑是直觉主义逻辑通过添加二元连接词得到的自然表达扩展。结合先前结果，完整呈现了命题双直觉逻辑的表达能力。
英文摘要
The question of the expressive power of a given logical language with Kripke relational semantics has at least two dimensions: (1) what the language can say about frames, and (2) what it can say about models. The Goldblatt-Thomason theorem provides a model-theoretic characterisation of modal axiomatisability for elementary classes of frames in terms of closure under taking generated subframes, disjoint unions, bounded morphic images, and reflection of ultrafilter extensions. Goldblatt also provides a similar characterisation for axiomatisability in intuitionistic logic of classes of models rather than frames. In this article we provide analogous results for bi-intuitionistic logic, a natural expressive extension of intuitionistic logic obtained by adding a binary connective dual to the intuitionistic implication, introduced in the 1970s independently by Dieter Klemke and Cecylia Rauszer. Together with previous results, such as a van Benthem bisimulation characterisation theorem and a Lindstrom theorem, this provides a complete picture of the expressive power of propositional bi-intuitionistic logic.
Journal refJ. Appl. Logics 12 (2025), no. 5, 1125-1151
