初等团队逻辑中的直觉主义蕴涵
Intuitionistic Implication in Elementary Team Logics
浏览论文内容
中文总结 AI 辅助
本文研究初等团队逻辑FOT的两种修改：其无包含原子片段的量词消去，以及添加直觉主义蕴涵后表达能力提升至全二阶逻辑，导致有效性等价。
中文摘要 AI 辅助
逻辑FOT是一种基于团队的逻辑，其表达能力在句子和开放公式两个层面上都与一阶逻辑一致。与能够定义更强的二阶团队性质的相关依赖逻辑和独立逻辑不同，FOT旨在精确捕获初等团队性质，模去空团队。在本文中，我们考虑FOT的两种修改。首先，我们研究了FOT本质上不含包含原子的片段。我们的主要结果是在空签名下为该片段建立了量词消去。其次，我们研究了FOT通过直觉主义蕴涵的扩展。主要结论是，添加这一单一连接词增强了表达能力，使得每个二阶句子都可以通过在全团队上求值的开放公式来编码。因此，公式的有效性等价于全二阶逻辑的有效性。
英文摘要
The logic FOT is a team-based logic whose expressive power coincides with first-order logic at the level of both sentences and open formulas. In contrast to dependence and independence logics, which can define stronger second-order team properties, FOT is designed to capture exactly elementary team properties, modulo the empty team. In this paper we consider two modifications of FOT. First, we investigate essentially the inclusion atom free fragment of FOT. Our main result establishes quantifier elimination for the fragment in the empty signature. Second, we study an extension of FOT by the intuitionistic implication. The main conclusion is that adding this single connective increases the expressive strength so that every second-order sentence can be encoded by an open formula evaluated on the full team. Consequently, validity of formulas is equivalent to validity of full second-order logic.
发表机构
- University of Gothenburg（哥德堡大学）
- University of Helsinki（赫尔辛基大学）
机构由 AI 辅助整理，请以论文原文为准。
