Monadic Second Order Logic with Measure and Category Quantifiers
本文研究了在无限词和树上,将一元二阶逻辑扩展为带有基于贝尔范畴和勒贝格测度的广义“几乎全部”量词,探讨其表达能力和性质。
2018-04-09 cs.FL cs.LO math.LO
Coalgebraic Geometric Logic: Basic Theory
本文利用余代数理论,为命题几何逻辑引入模态词,构建统一框架,研究推导系统、可靠性与完备性,并比较模态等价、行为等价与互模拟,提供终对象。
2022-12-07 math.LO
Multialgebras and Non-Deterministic Semantics applied to Paraconsistent Logics
本文的工作主要分为两个方面:在多重代数理论中,我们主要关注自由生成对象在其范畴中的新定义,以及这个范畴如何等价于另一个以偏序代数为对象的范畴;然后,我们使用非确定性语义,特别是那些我们命名为限制N矩阵,关于次协调逻辑和处理不相容性的自然概念的新表示的一些系统,它概括了不一致性。
2022-06-21 math.LO
Category theory, logic and formal linguistics: some connections, old and new
Université de Bordeaux(波尔多大学)
我们抓住出版的机会,从\emph{Logic, categories, semantics}研讨会在\emph{Journal of Applied Logic}调查一些当前的趋势,在逻辑,即直觉和线性类型的理论,交织分类,几何和计算的考虑。此后,我们提出如何这些丰富的逻辑框架可以模拟语言传达意义的方式。
2014-01-25 cs.CL cs.LO math.CT
Categorical semantics of metric spaces and continuous logic
使用范畴的度量空间作为模板,我们开发了一个度量模拟的范畴语义的经典/直觉主义逻辑,并表明,自然概念的谓词在这个“连续语义”是等价的一个先验的单独概念的谓词在连续逻辑,这是独立的模型理论家研究,并发现各种应用。我们通过把度量空间范畴中的实区间[0,1]表示为一个“连续子对象分类器”来证明这一等价性,它不仅给出了两个谓词概念之间的对应关系,而且给出了连续语义中的自然量化概念与连续逻辑中已有的量化概念之间的对应关系。一路上,我们制定了它的意思是一个给定的范畴表现得像度量空间的范畴,然后表明,任何这样的类别支持上述连续语义。作为一个应用,我们表明,范畴的预层的度量空间的例子,事实上,甚至拥有连续的子对象分类。
2019-01-25 math.CT math.LO
Logic Without Syntax
本文提出了一个抽象的,数学公式的经典命题逻辑。它一层一层地进行:(1)抽象的、无语法的命题;(2)抽象的、无语法的收缩弱化证明;(3)分布;(4)公理(p或非p)。抽象命题对应于范畴G(Rel^L)的对象,其中G是Hyland-Tan双胶合构造,Rel是集合和关系的标准集范畴,L是文字的集合。抽象证明是Gl(Rel^L)的一个紧正交子范畴的态射,其中我们定义Gl为G的一个松弛变体。证明了L上的自由二元积和范畴(收缩弱化逻辑)是Gl(Rel^L)的一个满子范畴,自由分配格范畴(收缩弱化分配逻辑)是Gl(Rel^L)的一个满子范畴.我们探讨一般的结构,增加公理,这是不是雷尔特定的或(p或不p)特定的。
2005-04-04 math.CT math.LO
Logic and Concepts in the 2-category of Topoi
该研究在topoi 2-范畴中用Kan内射性公理化概念,引入几何逻辑片段并建立对应松弛幂等伪单子,证明其代数有分类topos且给出Diaconescu型结果,定义了概念完全的几何逻辑片段。
2025-05-21 cs.LO math.CT math.LO
Omitting Types and the Baire Category Theorem
模型论中的省略类型定理和拓扑学中的Baire范畴定理是紧密联系在一起的。我们研究这两个定理之间的精确关系。工作的一般概念的逻辑,我们表明,经典的省略型定理成立的逻辑,如果一个特定的相关拓扑空间的所有封闭的子空间Baire。我们还考虑更强的Baire类别条件,因此更强的省略类型定理,包括一个游戏版本。我们使用的例子,以前研究的空间集理论的拓扑产生抽象逻辑表明,游戏省略类型的声明是一贯不等同于经典的。
2017-10-16 math.GN math.LO
A topos for continuous logic
我们建议在连续逻辑中的谓词的顺序,使连续逻辑的语义可以制定为一个hyperdoctrine。我们表明,这种hyperdoctrine可以嵌入到hyperdoctrine的subobobian一个合适的Grothendieck拓扑。对于这种嵌入,我们使用连续逻辑的超理论的简化,其等价关系的范畴等价于完全度量空间和一致连续映射的范畴。
2021-07-22 math.CT math.LO
Logics of formal inconsistency arising from systems of fuzzy logic
Artificial Intelligence Research Institute (IIIA), CSIC(西班牙科学研究理事会人工智能研究所)
本文提出了模糊逻辑与次协调的一种非常精确和基础性的相遇。具体而言,在本文中,我们介绍了扩展的模糊逻辑MTL的原始运营商的一致性和不一致的风格,所谓的逻辑形式不一致(LFIs)。本方法的主要新颖之处在于定义了MTL-代数上这类算子的公设,从而定义和公理化了一族逻辑,扩展了MTL,其度保持对应物是次协调的,而且是LFI。
2014-03-08 cs.AI cs.LO math.LO
Graphical Regular Logic
正则逻辑可以被看作是正则范畴的内部语言,但逻辑本身一般不被给予范畴化的处理。本文从集合$\mathrm{T}$上的自由正则范畴$\mathsf{FRg}(\mathrm{T})$的角度来理解正则逻辑的语法和证明规则。从这个观点来看,正则理论是从一个合适的2-范畴的上下文-$\mathsf{FRg}(\mathrm{T})$中的2-范畴的关系-到2-范畴的偏序集的某些monoidal 2-函子。这样的函子给每个上下文中的公式集赋值,并按蕴涵排序。我们把这样一个2-函子称为一个正则演算,因为它自然地产生了一个图形化的弦图演算的精神Joyal和街。我们的主要目的是证明正则范畴的范畴本质上是正则演算的范畴的反射。一路上,我们演示了如何使用这种图形演算。
2019-06-20 cs.LO math.CT math.LO
Quantifiers for quantum logic
我们考虑希尔伯特空间范畴上的范畴逻辑。更一般地说,事实上,任何前希尔伯特范畴都足够了。我们证明了闭子代数构成正交模格。这说明量子逻辑只是范畴逻辑的一个具体化,使我们能够为量子逻辑建立一个存在量词,并得出不存在全称量词的结论。
2009-04-23 math.CT math.LO quant-ph
Axiomatizing Category Theory in Free Logic
University of Luxemburg(卢森堡大学);Freie Universität Berlin(柏林自由大学)
从推广的标准公理的幺半群,我们提出了一个逐步发展的各种,相互等价的基本公理系统的范畴论。我们的公理集已经在Isabelle/HOL交互式证明助手中进行了形式化,这种形式化利用了经典高阶逻辑中自由逻辑的语义正确嵌入。我们的公理集的建模和形式化分析已显着支持一系列的实验与自动推理工具集成Isabelle/HOL。我们还解决了我们的公理系统的关系,从文献中的替代建议,包括一个公理集提出的Freyd和Scedrov,我们揭示了一个技术问题(当编码在自由逻辑的自由变量范围内定义和未定义的对象):无论是所有的操作,例如态射组合,是总的或其公理系统是不一致的。然而,这个问题的修复是非常简单的。
2018-10-12 cs.AI cs.LO math.CT
Tense distributive lattices: algebra, logic and topology
本文研究了配备Prior时态算子的有界分配格范畴tdlat,建立了其与Kripke框架和Priestley空间的范畴对偶性,刻画了同余格与次直不可约成员,并定义了保持真值度的逻辑。
2023-09-09 math.LO
On the lack of colimits in various categories arising in pointfree topology and algebraic logic
University of Birmingham(伯明翰大学);New Mexico State University(新墨西哥州立大学);University of Milan(米兰大学)
研究证明McKinsey-Tarski代数范畴不等价于代数品种,反驳了Peter Jipsen的问题。各类BAO、Heyting代数及框架的范畴不完整,因此不等价于预品种。
2026-03-14 math.CT math.LO
A categorical equivalence for monadic algebras of first-order substructural logics motivated by Kalman's construction
School of Science, Xi’an Shiyou University(西安石油大学理学院);School of Science, Xi Hang University(西安航天大学理学院);CONICET and Departamento de Matematica, Facultad de Ciencias Exactas, Universidad Nacional del Centro de la Provincia de Buenos Aires(阿根廷布宜诺斯艾利斯省中部国立大学精确科学学院数学系与阿根廷国家科学研究委员会)
本文通过卡曼构造,研究单子余分配格的范畴等价性,并扩展了相关领域的研究成果。
2026-01-29 math.LO
Interaction Systems and Linear Logic, a different games semantics
我们定义了一个模型的线性逻辑的基础上两个众所周知的成分:游戏和模拟。这个模型在以下方面很有趣:虽然很明显,解释公式的对象是游戏,并且一切都是在考虑交互的直觉的情况下开发的,但态射的概念与游戏语义中的传统态射非常不同。特别是,我们没有使用战略的概念!由此产生的结构与通常在游戏类别中发现的结构非常不同。我们首先定义了几个结构,这些游戏和显示,使用基本的考虑,他们享有适当的代数属性,使这一类的指称模型的直觉线性逻辑。有趣的一点是,张量积对应于游戏上的强同步操作。使用传统的翻译,这个范畴也可以作为简单类型演算的模型.我们使用范畴的一些附加结构将其扩展到简单类型的微分模型。一旦完成了这一步,我们再进一步,在这个范畴中构造一个自反对象,从而得到一个非类型化微分的具体的非平凡模型。然后,我们使用高度非构造性的原则表明,该类别实际上是完全经典线性逻辑的模型;最后,我们简要介绍了谓词Transformers和容器的相关概念。
2009-05-25 cs.LO math.LO
Classical linear logic, cobordisms and categorical semantics of categorial grammars
National Research University Higher School of Economics(俄罗斯国立高等经济大学)
我们提出了一个基于经典乘法线性逻辑的范畴文法。这可以被看作是抽象范畴语法(ACG)的扩展,并且至少具有同样的表达能力。然而,{ \it线性逻辑文法(LLG)}的组成部分不是抽象的$λ$ -项,而是简单的带有标记端点的词元组,我们称它们为{ \it多词}。至少,这给出了ACG的具体和直观的表示。一个关键的观察是,类的多字有一个基本的代数结构。也就是说,多词可以被组织在一个类别中,非常类似于拓扑配边的类别。该范畴是对称的monoidal闭的和紧的闭的,因此是线性$λ$ -微积分和经典线性逻辑的模型。我们认为这一类别本身就很有趣。特别是,它可以为其他形式主义提供分类表示。另一方面,语言语义的许多模型是基于交换逻辑,或者更一般地,基于对称monoidal闭范畴。但{ \it word cobordisms}范畴是一个语言元素范畴,它本身是对称的么半群闭的,独立于任何文法。因此,它可能被证明在理解语言语义方面也很有用。
2019-02-09 cs.CL cs.LO math.LO
On the completeness of the countable fragment of geometric logic
Graduate School of Human and Environmental Studies Kyoto University(京都大学人类与环境学研究科)
研究几何逻辑可数片段(σ-相干逻辑)中可数σ-相干理论完备性,在命题和谓词逻辑下分别确定模型的拟波兰空间和范畴,公式解释为连续函数与函子,还通过研究“清醒性”概念扩展类比。
2026-07-27 math.CT math.LO
The Kim-Pillay theorem for Abstract Elementary Categories
我们介绍了AECats(抽象基本范畴)的框架,概括了某些一阶理论的模型范畴和模型子集范畴。任何AEC和任何紧凑抽象理论(“猫”,由本-雅科夫介绍)形成一个AECat。特别是,我们发现应用程序在积极的逻辑和连续逻辑:一类(子集)模型的积极或连续的理论是一个AECat。一阶逻辑的Kim-Pillay定理通过划分独立性的性质来表征简单的理论。我们证明了一个版本的金-皮莱定理AECats的合并属性,推广一阶版本和现有的版本的积极逻辑。
2020-10-29 math.CT math.LO
Regular Calculi I: Graphical Regular Logic
关系的人机工程学语法是什么?在这第一个文件在一系列的两个,回答这个问题,我们定义定期演算:一个适当结构的函子从一个类别表示语法的正规逻辑的类别偏序集,这需要每个对象的偏序集的关系,该类型。我们介绍了两个主要类别的例子,经常演算对应于经常理论,经常演算对应于经常类别。工作在经常演算,我们提出了一个图形框架,作为原始的各种移动的经常逻辑。正则演算的主要定理是正则范畴的语法语义$2$维附加。
2021-09-29 math.CT math.LO
Undecidability and non-axiomatizability of modal many-valued logics
在这项工作中,我们研究了一类全球模态逻辑所产生的Kripke框架评估某些剩余格,在文献中称为模态多值逻辑的可判定性。我们展示了一个大的家庭,这些模态逻辑是不可判定的,与经典的模态逻辑和命题逻辑定义在同一类代数。这个家族包括了在标准Lukasiewicz代数和乘积代数上计算的Kripke框架所产生的全局模态逻辑。我们改进了前面的结果,证明了全局模态Lukasiewicz和乘积逻辑甚至不能递归可公理化。我们的结论是否定地解决了开放的问题,即每个全局模态逻辑是否与它的局部模态逻辑在无限制必然规则下是封闭的。
2022-04-15 cs.LO math.LO
Topological representation of intuitionistic and distributive abstract logics
我们继续我们早期论文的工作(Lewitzka和Brunner:Minimally generated abstract logics,Logica Universalis 3(2),2009),其中研究了抽象逻辑,特别是直觉抽象逻辑。抽象逻辑可以直接自然地拓扑化。这有利于拓扑研究类的具体逻辑时,他们给出了抽象的形式。此外,这种直接的拓扑方法避免了通常用于表示逻辑的复杂的代数和格论机器。基于这一观点,本文定义了以稳定逻辑映射为态射的直觉抽象逻辑范畴和以谱映射为态射的蕴涵谱空间范畴。我们证明了这些范畴的等价性,并得出结论,分配抽象逻辑和分配清醒空间的更大的范畴是等价的。
2015-08-18 cs.LO math.LO
Elementary topoi
作为原型范畴,$\mathbf{Set}$具有许多性质,使其在范畴中具有特殊性。从数理逻辑的观点来看,其中一个性质是$\mathbf{Set}$有足够的结构来“适当地”形式化逻辑。然而,我们可以问,在另一个范畴$\mathbf{C}$中形式化逻辑可能意味着什么。一个(基本的)topos的概念提炼了$\mathbf{Set}$的基本特征,这些特征使我们能够这样做。本报告定义了topoi,并描述了topos中一阶逻辑和集合论的发展。
2020-11-26 math.CT math.LO
Classical linear logic, cobordisms and categorial grammars
National Research University Higher School of Economics(国立研究大学高等经济学院)
我们提出了一个基于经典乘法线性逻辑的范畴文法。这可以被看作是抽象范畴语法(ACG)的扩展,并且至少具有同样的表达能力。然而,{\it线性逻辑语法(LLG)}的组成部分不是抽象的$λ$-项,而是简单的带有标记端点的单词元组,并提供有特定的{\it插入指令}:端点集合被细分为{\it传入}和{\it传出}部分。我们称这种对象为{\it word cobordisms}。一个关键的观察是,词配边可以组织在一个类别中,非常类似于熟悉的拓扑配边类别。这个范畴是对称monoidal闭的和紧闭的,因此是线性$λ$-演算和经典的,以及直觉主义线性逻辑的模型。这允许我们使用线性逻辑作为单词配边的打字系统。至少,这给出了ACG的具体和直观的表示。然而,我们认为,具有丰富结构并且独立于任何语法的词配边范畴本身可能是有趣的。
2020-07-31 cs.CL cs.LO math.LO
Categories for Dynamic Epistemic Logic
本文的主要目标是用范畴理论的术语来重铸模态逻辑,特别是动态认知逻辑(DEL)的语义。我们首先回顾范畴的关系和范畴的克里普克框架,特别强调的对偶关系和伴随同态。使用这些类别,然后我们重新制定DEL的语义在一个更明确的和代数的形式。新提法的几个优点将得到证明:DEL将一个模型更新为另一个模型的思想自然地被范畴视角捕捉到--它强调一个对象族和它们之间的结构关系,而不是单个对象和它上面的结构。此外,DEL的范畴语义可以直接与一阶逻辑的标准范畴语义合并,为一阶DEL提供语义。
2017-07-27 cs.LO math.LO
Homotopy type theory: the logic of space
这是从范畴论和拓扑学的角度对类型论、合成拓扑学和同伦类型论的介绍,作为《数学和物理的新空间》(Gabriel Catren和Mathieu Anel编)一书的一章。
2017-03-08 math.CT math.LO
Intuitionistic Linear Logic with Subexponentials: Type Theory, Categorical Models and Realisability
本文提出了一种带有子指数的直觉线性逻辑类型论,并探讨了其范畴模型和可实现性理论。
2026-10-09 math.CT math.LO
Set theory for category theory
集合论的大小问题在范畴论中扮演着重要的角色,特别是集合和真类(或小集合和大集合)之间的区别。有许多不同的方法来形式化这一点,而做出哪种选择会对允许什么样的范畴结构产生明显的影响。在这篇简要的论文中,我们总结和比较了一些这样的“范畴论的集合论基础”,并描述了它们对范畴论的日常使用的影响。我们假设读者有一些范畴论的基础知识,但很少或没有形式逻辑或集合论的经验。
2008-10-07 math.CT math.LO
On Banach spaces of sequences and free linear logic exponential modality
我们引入一类向量空间建模完整的命题线性逻辑,类似于概率相干空间和Koethe序列空间。它的对象是{ \it操纵的序列空间}、序列的Banach空间,其范数是根据与有限序列的配对定义的,而态射是有界线性映射,在适当的拓扑中连续。工作的主要兴趣是,我们的模型给出了一个实现的自由线性逻辑指数的建设。
2016-11-23 cs.LO math.LO
Predicate Transformers and Linear Logic, yet another denotational model
在精化演算中,单调谓词Transformers被用来为(命令式)程序建模。与模拟的自然概念一起,它们形成了一个具有许多代数性质的范畴。我们建立在这个结构上,使谓词Transformers成为一个完整的线性逻辑的描述模型:所有的逻辑结构都有一个自然的解释谓词Transformers器(即在规范方面)。然后,我们解释证明的一个公式的安全性为相应的规格。
2009-05-25 cs.LO math.LO