Intuitionistic Implication in Elementary Team Logics
University of Gothenburg(哥德堡大学);University of Helsinki(赫尔辛基大学)
本文研究初等团队逻辑FOT的两种修改:其无包含原子片段的量词消去,以及添加直觉主义蕴涵后表达能力提升至全二阶逻辑,导致有效性等价。
2026-09-15 math.LO
The Propositional Logic of Team Properties
University of Gothenburg(哥德堡大学)
针对团队语义逻辑缺乏可替换性的问题,提出团队性质逻辑(LTP),通过布尔代数的幂集代数给出语义,并建立了一个可靠且完备的标记自然演绎系统。
2026-07-01 math.LO
Inclusion and Exclusion Dependencies in Team Semantics: On Some Logics of Imperfect Information
通过在一阶逻辑的语言中加入对应于包含依赖和排除依赖的原子公式,引入了一些新的不完全信息逻辑。然后研究了这些逻辑的性质及其与其他不完全信息逻辑的关系。此外,这些逻辑的博弈论语义的发展。作为这些结果的推论,我们描述了独立逻辑的表达能力,从而回答了(Grädel和Väänänen,2010)中提出的一个开放问题。
2011-06-11 math.LO
Convex Team Logics
University of Padua(帕多瓦大学);University of Amsterdam(阿姆斯特丹大学)
本文证明凸命题和模态团队逻辑的表达完备性,引入多种完备逻辑,并回答经典命题逻辑加非空原子NE的开放问题,推广统一定义性概念。
2026-10-15 math.LO
Expressibility and inexpressibility in propositional team logics
University of Helsinki(赫尔辛基大学);Leibniz University Hannover(汉诺威莱布尼茨大学)
本文研究命题团队逻辑中可表达性与不可表达性问题,通过维度理论方法分析原子表达的代价,提出新变种的原子和运算,揭示逻辑的范围与限制。
2026-02-26 math.LO
A Logic for Arguing About Probabilities in Measure Teams
University of Helsinki(赫尔辛基大学);Department of Mathematics and Statistics, University of Helsinki(赫尔辛基大学数学与统计系);Institute for logic, Language and Computation, University of Amsterdam(阿姆斯特丹大学逻辑、语言与计算研究所)
我们使用一组任务,也就是。团队,并对他们进行测量,以定义给定数据中一阶公式的概率。然后,我们axiomatise这样的概率的一阶属性,并证明了我们的axiomatisation的完整性定理。我们使用生物学的Hardy-Weinberg原理和量子物理学的Bell不等式作为例子。
2016-09-08 math.LO
On the Expressive Power of TeamLTL and First-Order Team Logic over Hyperproperties
在这篇文章中,我们研究线性时态逻辑与团队语义(TeamLTL),是新的逻辑定义超属性。我们将这些逻辑的坎普型翻译定义为一阶团队逻辑和二阶逻辑的片段。我们还描述了团队逻辑和二阶逻辑的模型检查和可满足性的表达能力和复杂性,将它们与二阶和三阶算术联系起来。我们的结果集在一个更大的背景下,最近的结果Lück表明,扩展TeamLTL的布尔否定是高度不可判定的下,所谓的同步语义。我们还研究了TeamLTL扩展的口吃不变片段。
2021-10-21 cs.LO math.LO
Two strong undefinability results in inquisitive and team semantics
本文针对基于探究语义和团队语义的逻辑,证明了直觉主义蕴涵在带张量的扩展命题探究逻辑中,以及全局析取在扩展命题依赖逻辑中均具有不可定义性。
2024-07-30 math.LO
Sahlqvist theory for impossible worlds
我们将统一对应论推广到不可能世界的Kripke框架及其相关的正则模态逻辑。这些逻辑的模态联结不需要是正规的:只需要较弱的可加性和乘法性。在概念上,有人认为,它们缺乏必要性,使得规则模态逻辑比正常的模态逻辑更适合在形式化的认识和道义设置。从技术的角度来看,正则性被证明是非常自然的,足以处理代数正规性约翰逊式。事实上,加法性和乘法性是将琼森最初的规范性证明扩展到某些正则分配模态逻辑的完整萨尔奎斯特类的关键,自然地概括了分配模态逻辑。最有趣的是,加性和乘性也是原始(即正常)DML中约翰逊式正规性的关键。我们的贡献包括:在分配格命题基上定义了正则模态逻辑的Sahlqvist不等式,证明了它们遵循Jónsson策略的规范性,并将ALBA算法应用于两个非经典的正则模态逻辑的构造(分配格和直觉)的基础,证明适应ALBA是保证成功的语法定义的类,其中适当地包括Sahlqvist一个;最后,应用前面的结果,代替Kripke的证明,证明了Lemmon的认知逻辑E2-E5关于具有不可能世界的Kripke框架的初等类的强完备性。
2016-03-27 math.LO
A Deep-Inference Sequent Calculus for Basic Propositional Team Logic (Without Delving Too Deep)
本文为包含分裂析取与探究析取的基础命题团队逻辑引入了一种深度推理矢列演算,证明了其保高度弱化、切消除等性质,并导出了新的Lyndon插值定理。
2025-08-10 math.LO
Characterizing Relative Frame Definability in Team Semantics via the Universal Modality
设ML(U^+)表示用普适模态扩展的模态逻辑的片段,其中普适模态只肯定地出现。我们在著名的Goldblatt-Schlason定理的精神下刻画了ML(U^+)相对于有限传递框架的相对可定义性。我们证明了一类Kripke框架在ML(U^+)中相对于有限传递框架是可定义的当且仅当F在取生成子帧和有界形态像下是闭的。此外,我们还研究了团队逻辑中的模态可定义性。我们研究(扩展)模态依赖逻辑,(扩展)模态包含逻辑和模态团队逻辑。关于全局模型的可定义性,我们得到一个二分法和相对于框架的可定义性。作为一个推论,我们得到了上面所列的每一个逻辑的相对戈德布拉特-卡森式定理.
2018-02-22 math.LO
Generalized quantifiers using team semantics
本文修改依赖逻辑的基本语义准则,构建了一个能同时处理单调与非单调广义量词的框架,证明其具有与存在性二阶逻辑相同的表达力并保持保守性。
2024-04-26 math.LO
Teams, Truthmakers, Translations
University of Amsterdam(阿姆斯特丹大学);Stanford University(斯坦福大学);Tsinghua University(清华大学)
该研究提出从BSL逻辑到半格上经典模态逻辑的忠实翻译方法,可推广至其他超内涵逻辑,还探讨了超内涵逻辑翻译为经典模态逻辑的应用与新挑战。
2026-10-14 math.LO
Team Semantics and Independence Notions in Quantum Physics
University College London(伦敦大学学院);University of Helsinki(赫尔辛基大学)
本文通过团队语义研究量子物理中的依赖性和独立性概念,提出新的独立逻辑和概率独立逻辑发展。
2025-01-17 math.LO
Capturing dual team properties with inclusion atoms
University of Helsinki(赫尔辛基大学)
本文提出了一种命题团队逻辑,通过包含原子的变体实现对准向下和准向上闭属性的表达性完备,并定义了相应的自然演绎系统。
2026-03-05 math.LO
On the Expressive Power of Inquisitive Team Logic and Inquisitive First-Order Logic
University of Helsinki(赫尔辛基大学);University of Padua(帕多瓦大学)
本文证明探究团队逻辑中开放公式的表达能力严格超越一阶逻辑,并扩展至探究一阶逻辑,解决了一个开放问题。
2026-07-01 cs.LO math.LO
Modal Dependence Logics: Axiomatizations and Model-theoretic Properties
模态依赖逻辑是基于团队语义定义的模态逻辑,具有向下封闭性。在本文中,我们介绍了健全的和完整的演绎系统的主要模态依赖逻辑,特别是那些在其语言中的直觉连接词。我们还建立了一个具体的团队语义和单世界语义之间的联系,并表明,模态依赖逻辑可以解释为直觉模态逻辑的变种。
2017-06-03 math.LO
Some observations about generalized quantifiers in logics of imperfect information
本文分析了F. Engström,将它们与更一般、更高阶的团队量词定义进行比较。我们表明,Engström的定义(和其他量词从文献中)可以识别,通过适当的电梯,特殊类的团队量词。我们指出,新的团队量化表达的定量和定性的组成部分,而Engström的量化范围只在后者。我们进一步认为,Engström的定义只是嵌入到团队语义的一阶广义量词,并没有捕捉到一个足够的概念团队理论的广义量词,除了在特殊情况下,量词适用于平面公式。我们还提出了几个疑问的意义的单调/非单调的区别在这种情况下。在附录中,我们为Engström的量词发展了一些证明论。
2019-05-16 math.LO
There are (other) ways to negate in propositional team semantics
本文研究命题团队语义中的否定机制,证明完全直觉主义否定不增加向下封闭逻辑的公理化复杂度,并证明同时含依赖原子与包含原子的命题逻辑具有表达完备性。
2024-10-10 cs.LO math.LO
Complexity of Propositional Logics in Team Semantics
我们分类的可满足性,有效性和模型检测问题的命题独立性,包含性和团队逻辑的计算复杂性。我们的主要结果表明,命题组逻辑的可满足性和有效性问题是完全的交替指数时间与多项式多交替。
2017-01-05 cs.CC cs.LO math.LO
Decidability of predicate logics with team semantics
我们研究了基于团队语义的谓词逻辑的复杂性。证明了二元独立逻辑和二元包含逻辑的可满足性问题都是NEXPTIME-完全的。此外,我们表明,两个变量的依赖逻辑的有效性问题是不可判定的,从而解决了一个开放的问题,从团队语义文献。我们还简要地分析了依赖逻辑的Bernays-Schönfinkel-Ramsey前缀类的复杂性。
2016-06-18 cs.CC cs.LO math.LO
Characterising Modal Definability of Team-Based Logics via the Universal Modality
我们研究了各种模态逻辑的模型和框架可定义性。设ML(A+)表示用普适模态扩展的模态逻辑的片段,其中普适模态只肯定地出现。我们证明了一类Kripke模型在ML(A+)中是可定义的当且仅当该类是初等的,并且在不相交的工会和满射互模拟下是封闭的。我们还讨论了ML(A+)的可定义性的精神,著名的Goldblatt-Maxason定理。我们证明了Kripke框架的一个初等类F在ML(A+)中是可定义的当且仅当F在取生成子帧和有界形态图像下是闭的,并且反映了超滤子扩展和超滤子帧生成.此外,我们还研究了相对于有限传递框架的框架可定义性,并给出了相对于有限传递框架的ML(A+)-可定义性的一个类似刻画。最后,我们在团队逻辑中开始了模型和框架可定义性的研究。我们研究(扩展)模态依赖逻辑,(扩展)模态包含逻辑和模态团队逻辑。我们建立严格的线性层次模型的可定义性和框架的可定义性,分别。我们表明,关于模型和框架的可定义性,前面提到的团队为基础的逻辑,除了模态依赖逻辑,要么符合ML(A+)或平原模态逻辑ML。因此,作为一个推论,我们得到的模型和框架可定义的团队为基础的逻辑的模型论特征。
2018-02-21 cs.LO math.LO
The Expressive Power of Modal Dependence Logic
我们研究了各种模态逻辑与团队语义的表达能力。我们表明,正是向下封闭和封闭下的团队k-互模拟的团队的属性,对于一些有限的k,是可定义的模态逻辑扩展与直觉析取。此外,我们还证明了直觉析取模态逻辑和扩展模态依赖逻辑的表达能力是一致的。最后,我们建立任何翻译从扩展模态依赖逻辑到模态逻辑与直觉析取增加一些公式的大小呈指数级。
2014-06-24 cs.LO math.LO
A Double Team Semantics for Generalized Quantifiers
我们定义了基于双队的广义量词一阶逻辑的语义。我们还定义和研究了广义原子的概念。这样的原子可以用来定义具有基于团队的语义的一阶逻辑的扩展。我们还定义了一个游戏语义,并将其与双队语义进行了比较。
2017-08-31 cs.LO math.LO
Strongly First Order Disjunctive Embedded Dependencies in Team Semantics
本文刻画了添加到一阶团队语义时不会增强其表达力的(域无关)析取嵌入依赖,为团队语义与数据库依赖理论提供联系。
2025-06-18 math.LO
The expressive power of modal logic with inclusion atoms
模态包含逻辑是基本模态逻辑的包含原子扩展,其语义定义在Kripke模型上。Kripke模型的团队只是其域的一个子集。本文给出了模态包含逻辑表达能力的一个完整刻画:一类带队的Kripke模型在模态包含逻辑中是可定义的当且仅当它在k-互模拟下是闭的,对于某个整数k,它在并下是闭的,并且它具有空队性质.我们还证明了同样的表达能力,可以通过添加一个单一的一元非空算子模态逻辑。此外,我们建立了一个指数下界的大小从模态包含逻辑到模态逻辑与非空算子的翻译。
2015-09-24 cs.LO math.LO
Complexity Results in Team Semantics: Nonemptiness Is Not So Complex
University of Helsinki(赫尔辛基大学);Utrecht University(乌得勒支大学)
研究团队语义中凸逻辑的复杂性,针对带非空原子NE的经典命题逻辑扩展,证明可满足性问题是NP完全的,有效问题是coNP完全的,模型检验问题属于P。
2026-02-26 cs.LO math.LO
Team Semantics and Recursive Enumerability
众所周知,依赖逻辑捕获复杂性类NP,最近已经表明,包含逻辑捕获有序模型上的P。这些结果表明,团队语义描述复杂性理论提供了有趣的新的可能性。为了正确理解团队语义和描述复杂性之间的联系,我们引入了依赖逻辑的扩展D*,它可以精确定义有限模型的所有递归可重复类。因此,D* 提供了一种替代图灵机的计算方法。D* 的基本新功能是一个运营商,可以扩展域所考虑的模型由有限数量的新鲜元素。由于广义量词与神谕之间的密切关系,我们也研究了广义量词在团队语义中的应用。我们证明了通过引入相应的广义依赖原子,可以从一阶逻辑的量词扩张中规范地消除(1)型单调量词。
2014-08-18 cs.LO math.LO
Dialetheism, Game Theoretic Semantics, and Paraconsistent Team Semantics
我们介绍了一个变体的依赖逻辑中的真理定义不存在的获胜策略的支持者(Eloise)在语义游戏中,但在缺乏获胜策略的对手(Abelard)。我们证明了这种语言是一阶逻辑的保守但次协调的扩展,它的有效性问题可以归结为一阶逻辑的有效性问题,它能够表达自己的真值和有效性谓词,并且它在表达上等价于通用二阶逻辑。此外,我们证明了一个次协调的非依赖逻辑公式是一致的当且仅当它是等价于一些一阶逻辑句子;另一方面,我们表明,所有的次协调依赖逻辑句子等价于一些一阶句子就真(但不一定就假)。
2014-03-14 cs.LO math.LO
Doubly Strongly First Order Dependencies
Team Semantics是Tarskian Semantics的一种推广,可用于向一阶逻辑添加原子和连接词,以表达变量的可能值之间的依赖关系。这些扩展中的一些比一阶逻辑更有表现力,而另一些则可还原为它。(可相对化的)原子和原子族,当它们和它们的否定单独或联合地添加到具有团队语义的一阶逻辑中时,它们不会增加该逻辑的表达能力(或者,等价地,当它们被添加到用仅适用于文字和依赖原子的矛盾否定连接符扩充的一阶逻辑时)。
2021-05-11 math.LO
Bicompleteness Theorems for Team Logics with the Dual Negation
University of Padua(帕多瓦大学)
研究独立友好逻辑和依赖逻辑中双重否定的语义不确定性,通过调整不相容概念,为多种模态和命题团队逻辑建立了类似结果,并提出了关于不相容性的表达完备性概念。
2026-06-23 cs.LO math.LO
Safe Dependency Atoms and Possibility Operators in Team Semantics
我考虑的问题是,哪些依赖关系是安全的一个团队语义为基础的逻辑FO(D),在这个意义上,他们不增加其表达能力的句子时,添加到它。我表明,一些依赖关系,如整体,非恒定性和非空性,是安全的所有逻辑FO(D),和其他依赖关系,如恒定性,尽管是强一阶的,但对于D的某些选择,对于FO(D)是不安全的。我还证明了可能性算子,它在一个团队中成立,当且仅当它的参数在一些非空的子团队中成立,可以添加到任何逻辑FO(D),而不增加其对句子的表达能力。
2018-09-11 cs.LO math.LO
The Logic of Approximate Dependence
我们扩展处理的函数相关,依赖逻辑的基本概念,包括依赖的可能性与有限数量的例外。我们称之为近似依赖。本文的主要结果是近似依赖原子的完备性定理。我们指出了一些有问题的特点,这表明我们应该考虑多个团队,而不仅仅是团队。
2014-08-19 cs.LO math.LO
A New Ehrenfeucht-Fraïssé Game for Dependence Logic
University College London(伦敦大学学院);University of Helsinki(赫尔辛基大学)
针对依赖逻辑,提出一种基于单元素移动的新Ehrenfeucht-Fraïssé游戏,并证明其刻画了依赖逻辑中的初等等价性。
2026-05-30 cs.LO math.LO
Facets of Distribution Identities in Probabilistic Team Semantics
我们研究概率团队语义,这是一个语义框架,允许同时研究逻辑和概率依赖关系。我们检查和分类的表达能力的逻辑形式主义所产生的不同的概率原子,如条件独立性和不同的变种的边际分布等价。我们还将框架的一阶理论的实数和应用我们的方法的开放问题的复杂性的蕴涵问题的条件独立性。
2019-02-25 cs.LO math.LO
Logics of Dependence and Independence: The Local Variants
现代的依赖和独立逻辑是基于团队语义的,这意味着公式的计算不是基于变量的单个赋值,而是基于一组这样的赋值,称为团队。这导致了存在二阶逻辑水平上的高表达能力。作为替代,Baltag和van Benthem提出了依赖逻辑的局部变体,称为函数依赖逻辑(logic of functional dependence,LFD)。虽然它的语义也是基于团队的,但公式只在其中一个分配上进行本地评估,并且团队只是作为评估过程中考虑的可能分配的供应。因此,这种逻辑依赖于广义赋值语义的模态视角,并且可以被看作是一阶逻辑的一个片段。对于不含等式的LFD变体,可满足性问题是可判定的。我们扩展了本地化逻辑的依赖和独立的想法,在一个系统的方式,考虑到本地变量的标准原子依赖属性:除了依赖和独立,还包括,排除和匿名。我们研究模型理论和算法问题的本地化逻辑,并解决了一些问题,已离开开放的巴尔塔格和范Benthem。特别地,我们研究了局部逻辑的可判定性问题,证明了等式可满足的LFD是不可判定的。此外,我们通过适当的互模拟的概念建立特征定理,并研究这些逻辑的模型检验问题的复杂性。
2021-02-20 cs.LO math.LO
Upwards Closed Dependencies in Team Semantics
我们证明了,向上封闭的一阶依赖原子与团队语义的一阶逻辑不增加其表达能力(相对于句子),这同样是真的,如果我们还添加恒定原子。因此,函数相关、条件独立、包含和排除原子的否定都可以加入到一阶逻辑中,而不增加它的表达能力。此外,我们定义了一类有界向上封闭的依赖关系,我们证明了无界的依赖关系不能定义在有界的。
2013-07-17 cs.LO math.LO
On the Model Theory of Second-Order Objects
University of Helsinki(赫尔辛基大学);University College London(伦敦大学学院);University of Torino(都灵大学);Istituto Nazionale di Alta Matematica “Francesco Severi”(弗朗切斯科·塞韦里国家高等数学研究所)
本文提出抽象初等团队范畴框架,用于研究集合和关系等二阶对象,并证明FOT逻辑满足林斯特罗姆定理,同时证明存在二阶逻辑中不同基数间分类性的转移结果。
2026-05-07 math.LO
Strongly First Order, Domain Independent Dependencies: the Union-Closed Case
团队语义学通过定义任务集而不是单个任务的满意度来概括塔斯基的语义学。因此,可以使用Team Semantics通过新的连接词或原子来扩展一阶逻辑-最重要的是,通过表示不同赋值之间的依赖关系的依赖关系原子。这些扩展中的一些比一阶逻辑本身更有表现力,而另一些则可还原为它。我为独立于域的依赖原子提供了充要条件(在这个意义上,它在一个关系中的真或假并不取决于在模型中不出现在关系中的元素的存在)和并集闭合(在这个意义上,只要它被一个关系族的所有成员所满足,它也被它们的并集所满足)是强一阶的,在这个意义上,通过将它们添加到一阶逻辑而获得的逻辑并不比一阶逻辑本身更有表现力。
2022-06-30 math.LO
Characterizing downwards closed, strongly first order, relativizable dependencies
在Team Semantics中,依赖概念是强一阶的,如果通过将相应的原子添加到一阶逻辑而获得的逻辑的每个句子等价于某个一阶句子。在这项工作中,它表明,所有非平凡的依赖原子,是强一阶,向下封闭,和相对化(在这个意义上,相对于一些一元谓词的相对化的相应原子是表达在他们)是可定义的恒定原子。此外,还证明了任何强一阶依赖对任何向下闭依赖族都是安全的,即把强一阶依赖和向下闭依赖都加到一阶逻辑上得到的逻辑的每个句子等价于只加向下闭依赖得到的逻辑的某个句子.
2019-02-22 math.LO