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
An Internal Logic of Virtual Double Categories
本文提出纤维化虚拟双范畴类型论（FVDblTT），作为形式范畴论的内在语言，通过语法-语义对偶性（双伴随）验证其与虚拟双范畴的等价性，从而支持范畴论中的同构推理。
2025-01-23 cs.LO math.CT
Monoidal category of operad of graphs
通常，类别的名称是从对象的名称继承而来的。然而，与对象和态射范畴更相关的是态射代数。因此，如果每个态射都是一个图，我们更愿意称之为一类图。在一个幺半范畴中，每个态射都可以看作是一个图，并且态射的部分代数具有一个运算数的结构，图的运算数。本文考虑图运算的一个幺半范畴，它具有图演算的基础。特别是，如果有一个生成对象，那么每个态射都是一个二元图。图形演算，多嫁接的态射，是自卵发展。我们解释代数逻辑和谓词演算在一个幺半范畴的operad的图，这导致了图形逻辑。基于辫状幺半范畴范畴的逻辑称为辫状逻辑。考虑由一个对象生成的辫状幺半范畴范畴。我们证明了编织逻辑是如何与蕴涵代数和海廷代数（与布尔代数相反）相关的，因此必须与拟群比与格更相关。一些应用到经典逻辑，模态逻辑和Lukasiewicz三值逻辑考虑。
2011-03-26 math.CT math.LO
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
Formal P-Category Theory and Normalization by Evaluation in Rocq
本文在 Rocq 中形式化 P-范畴论，并据此证明纯范畴式 NbE 算法的可靠性与强完备性，支持提取计算 β-η-正规形及转换推导的程序。
2025-05-12 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
Classical Control, Quantum Circuits and Linear Logic in Enriched Category Theory
本文通过富范畴理论为基于电路的量子函数式编程语言建立范畴模型，将电路语言嵌入宿主语言，并利用W*-代数范畴的dcpo-富结构扩展递归类型。
2020-03-09 cs.LO cs.PL math.CT
Quantifiers for quantum logic
我们考虑希尔伯特空间范畴上的范畴逻辑。更一般地说，事实上，任何前希尔伯特范畴都足够了。我们证明了闭子代数构成正交模格。这说明量子逻辑只是范畴逻辑的一个具体化，使我们能够为量子逻辑建立一个存在量词，并得出不存在全称量词的结论。
2009-04-23 math.CT math.LO quant-ph
A topos for continuous logic
我们建议在连续逻辑中的谓词的顺序，使连续逻辑的语义可以制定为一个hyperdoctrine。我们表明，这种hyperdoctrine可以嵌入到hyperdoctrine的subobobian一个合适的Grothendieck拓扑。对于这种嵌入，我们使用连续逻辑的超理论的简化，其等价关系的范畴等价于完全度量空间和一致连续映射的范畴。
2021-07-22 math.CT math.LO
Semantic Proof of Confluence of the Categorical Reduction System for Linear Logic
我们验证了我们以前的论文中介绍的线性范畴的重写演算的汇合结果。结合其中证明的终止性结果，建立了线性范畴的广义凝聚定理。也就是说，我们得到了一个方法来确定是否两个态射是相等的，直到一定的等价。
2021-05-02 cs.PL math.CT
On the sphere spectrum from the viewpoint of linear logic
本研究从线性逻辑视角，证明带有球谱、smash积和替换积的Γ集合范畴构成等混线性分配范畴，还指出Lydakis的装配映射对应混子，为线性逻辑乘法片段提供范畴语义。
2026-10-14 math.AT math.CT
Combinatorial skeletons of 2-cobordism and annular categories with applications to equational logic
Universität Wien（维也纳大学）
本文提出编码所有2-cobordism类的组合数据，并证明其局部monoids无有限公理化等式理论，同时构造了该范畴的von-Neumann-正则扩展。
2026-03-14 math.CT math.GR math.GT
The formal theory of monoidal monads
我们给出了一个3-范畴的，纯粹形式化的参数解释为什么在Kleisli代数的范畴上的宽松monoidal单子，和对偶的Eilenberg-Moore代数的范畴上的oplax monoidal单子，我们总是有一个自然的monoidal结构。关键的观察是，任何具有有限乘积的2-范畴D中的2-范畴的Lax monoidal monad同构于D中具有Lax态射的2-范畴中的2-范畴的具有oplax态射的monoidal对象。正如我们在文章结尾所解释的那样，类似的现象也发生在许多其他情况下。
2010-12-02 math.CT
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
Formal completion of a category along a subcategory
根据Kontsevich的思想，我们引入并研究了紧生成（由一组对象）增强的三角范畴沿着一个完整的厚本质上小的三角子范畴的形式完成的概念。特别是，我们证明（回答一个问题的Kontsevich），使用范畴的正式完成，可以得到普通的正式完成诺特计划沿闭子概形。此外，我们表明，Beilinson-Parshin adeles也可以得到使用范畴形式完成。
2010-08-12 math.AG math.CT
On the existence of a compact generator on the derived category of a noetherian formal scheme
本文证明了对于Noether形式概形X，它的具有拟凝聚扭同调的模层的导出范畴D_qct（X）是由单个紧对象生成的.在附录中我们证明了D_qct（X）中的紧对象范畴是拓扑小的。
2009-05-13 math.AG math.CT
The Kim-Pillay theorem for Abstract Elementary Categories
我们介绍了AECats（抽象基本范畴）的框架，概括了某些一阶理论的模型范畴和模型子集范畴。任何AEC和任何紧凑抽象理论（“猫”，由本-雅科夫介绍）形成一个AECat。特别是，我们发现应用程序在积极的逻辑和连续逻辑：一类（子集）模型的积极或连续的理论是一个AECat。一阶逻辑的Kim-Pillay定理通过划分独立性的性质来表征简单的理论。我们证明了一个版本的金-皮莱定理AECats的合并属性，推广一阶版本和现有的版本的积极逻辑。
2020-10-29 math.CT math.LO
Formalizing the $\infty$-Categorical Yoneda Lemma
本研究借助支持合成∞-范畴理论的新型证明助手Rzk，首次实现∞-范畴理论结论的形式化，核心成果包括范畴论基本定理米田引理的形式化，且框架内构造自动具备自然性或函子性。
2023-12-13 cs.LO math.AT math.CT
Regular and relational categories: Revisiting 'Cartesian bicategories I'
正则逻辑是由$=$、$\top$、$\wedge$和$\exists$生成的一阶逻辑的片段。这种逻辑的一个关键特征是，它是表达二元关系的组合所需的最小片段;另一个特征是，它是正则范畴的内部逻辑。这两个事实之间的联系是，在任何正则范畴中，人们都可以用联合一元跨度来构造二元关系的概念;这导致了所谓的正则范畴的关系的二元范畴。在本文中，我们提供了一个直接的公理化的双范畴的关系，我们称之为关系PO范畴，重新解释早期的工作，卡尔博尼和沃尔特斯沿着这些路线。我们的主要贡献是一个明确的证明，2范畴的正则范畴是等价的关系PO范畴。贯穿全文，我们强调关系po范畴的图形本质。
2019-08-30 math.CT
Logic and Categories As Tools For Building Theories
我们给一个简短的介绍范畴论针对哲学家。我们强调方法问题和哲学影响。
2012-01-25 math.CT
Regular Calculi I: Graphical Regular Logic
关系的人机工程学语法是什么？在这第一个文件在一系列的两个，回答这个问题，我们定义定期演算：一个适当结构的函子从一个类别表示语法的正规逻辑的类别偏序集，这需要每个对象的偏序集的关系，该类型。我们介绍了两个主要类别的例子，经常演算对应于经常理论，经常演算对应于经常类别。工作在经常演算，我们提出了一个图形框架，作为原始的各种移动的经常逻辑。正则演算的主要定理是正则范畴的语法语义$2$维附加。
2021-09-29 math.CT math.LO
Elementary topoi
作为原型范畴，$\mathbf{Set}$具有许多性质，使其在范畴中具有特殊性。从数理逻辑的观点来看，其中一个性质是$\mathbf{Set}$有足够的结构来“适当地”形式化逻辑。然而，我们可以问，在另一个范畴$\mathbf{C}$中形式化逻辑可能意味着什么。一个（基本的）topos的概念提炼了$\mathbf{Set}$的基本特征，这些特征使我们能够这样做。本报告定义了topoi，并描述了topos中一阶逻辑和集合论的发展。
2020-11-26 math.CT math.LO
On the unicity of formal category theories
证明了2-范畴$\mathcal K$上的余完备Yoneda结构与某些前箭头设备之间的等价性.为了做到这一点，我们认识到预层建设的共同完成Yoneda结构作为一个相对的，宽松的幂等单子发送每个容许1-细胞$f :A \to B$的一个附件$\boldsymbol{P}_!f\dashv\boldsymbol{P}^*f$。$\mathcal K$上的每一个余完全Yoneda结构都以这种方式产生于一个相对宽松的“具有足够伴随1-胞元”的幂等单子，其定义域生成可容许的理想，并且这样一个单子的Kleisli范畴为其定义域配备了前箭头。我们称这些结构为“yosegi”。通常，与yosegi相关联的预层构造会产生一个ambientus Yoneda结构;在这样的设置中，存在一个完全形式化的伊斯贝尔对偶。
2019-01-06 math.CT
Presheaves and cocompletions in formal category theory
Tallinn University of Technology（塔林科技大学）；University of Oxford（牛津大学）
本文研究了在形式范畴论中，陪射构造与自由陪集完成之间的关系，揭示了在熟悉场景中两者概念的重合，并扩展了富集范畴论中加权余极限的理论，提供了对陪射对象、自由陪集完成和完备对象的认识定理。
2026-07-28 math.CT
The topology of syntax relations of a formal language
本文描述了在语法图范畴上定义的邻域文法的基础上构造Grothendieck拓扑的方法。一个形式语言的符号图是带有节点的多重图，用语言字母表的符号来表示。邻域语法允许从给定字母表上的所有语法图的集合中选择正确的语法图，通过将每个正确的图映射到由语法的邻域组成的覆盖。这样的覆盖产生了Grothendieck的拓扑上的范畴的正确语法图扩展的邻域图。范畴的每个对象可以映射到该句法结构的含义（抽象意义）集合。从而定义了从正确语法图范畴到集合集范畴的反变函子。给定的反变函子范畴喜欢被看作是思考形式语言的语法和语义之间关系的方便手段。定义在反变函子范畴上的集合层是满足语义分析中定义的组合性原则的对象。
2008-02-28 math.CT
Polynomials in homotopy type theory as a Kleisli category
该研究将同伦类型论中的多项式构造推广至任意宇宙，扩展为跨距范畴上的单子及余单子，证明其Kleisli范畴等价于传统多项式范畴，并建立其与线性逻辑及微分线性逻辑模型的联系。
2024-12-07 math.CT
Implications of a Quillen Model Structures-Based Framework for Locality under Logical Equivalence
在[15]中，对于每个量词秩$k$的连续肯定句，给出了逻辑局部性的一个同伦变分，即逻辑等价下局部性的一个基于Quillen模型范畴的框架.在本文中，我们将提出一些影响和可能的主题，从上述框架中产生的调查。
2020-05-22 math.CT
Coherence of Proof-Net Categories
本文定义的证明网范畴的概念与线性逻辑中无常数命题的乘法片段的证明网中隐含的图密切相关。类似的图形出现在凯利和麦克莱恩的相干定理对称monoidal闭范畴。证明了证明网范畴的相干定理。这种一致性定理也证明了相应的线性逻辑的混合原则的箭头的存在。证明网范畴的概念抓住了星自治范畴概念的单位自由片段，星自治范畴是一类特殊的对称monoidal闭范畴。
2005-10-04 math.CT math.LO
The formal theory of Tannaka duality
Tannakian范畴是一个阿贝尔张量范畴，它配备了一个纤维函子和额外的结构，这些结构确保它等价于作用在域扩张的谱上的某个仿射广群概型的表示范畴。如果我们研究的是任意的交换环而不是域，则表示范畴不再是阿贝尔的。我们提供了一个充分条件的列表，以确保添加剂张量范畴是等价的仿射广群计划的表示的范畴上的仿射计划，或更一般地说，在一个对称的幺半范畴范畴的Hopf代数体的表示范畴。为了做到这一点，我们开发了一个“Tannaka二元性的形式理论”的启发罗斯街的“单子的形式理论。”“我们将我们的结果应用于某些类别的过滤模块，用于研究p-adic伽罗瓦表示。
2011-12-22 math.AG math.CT
On the equivalence invariance of formal category theory
本研究证明形式范畴论对可在equipment内表述命题的等价不变性，借助FOLDS与抽象同伦论的关联，在DblCat上构建了特定模型结构，明确其平凡纤维化与纤性对象的特征。
2025-09-04 math.AT math.CT
Formal category theory in $\infty$-equipments II: Lax functors, monoidality and fibrations
本文研究了$\infty$-装备框架，探讨了装备间的lax函子、闭幺半结构和内部纤维化概念，并证明该形式化方法可轻松建立内部$\infty$-范畴论的基础。
2024-08-27 math.AT math.CT
Homotopy type theory: the logic of space
这是从范畴论和拓扑学的角度对类型论、合成拓扑学和同伦类型论的介绍，作为《数学和物理的新空间》（Gabriel Catren和Mathieu Anel编）一书的一章。
2017-03-08 math.CT math.LO
Formal weakly enriched category theory
Masaryk University（马萨里克大学）；University of Milan（米兰大学）
本文构造了编码弱充实的形式范畴论，证明其与拟范畴的无穷宇宙等价，并导出充实版Quillen定理A。
2026-10-08 math.AT math.CT
Formal category theory in $\infty$-equipments I
本文将proarrow equipments推广至$\infty$-范畴，定义$\infty$-equipments，并研究其例子及内部范畴论基本概念如余极限和Kan扩张。
2025-09-25 math.AT math.CT
Towards 2-derivators for formal $\infty$-category theory
本文提出2-导出量的公理，用于形式∞-范畴理论，展示其在多种模型中的适用性及位移操作下的稳定性。
2025-11-30 math.AT math.CT
Type space functors and interpretations in positive logic
我们构造了一个2-等价的$\mathfrak{CohTheory}^\text{op} \simeq \mathfrak{TypeSpaceFunc}$。这里$\mathfrak{CohTheory}$是实证理论的2-范畴，而$\mathfrak{TypeSpaceFunc}$是型空间函子的2-范畴。我们给出了一个精确的定义解释的积极逻辑，这将是1细胞的$\mathfrak{CohTheory}$。2-胞腔是可定义的同态。2-等价限制于范畴的对偶性，使得理论与其类型空间的集合（即其类型空间函子）“相同”的哲学变得精确。在刻画那些作为类型空间函子出现的函子时，我们发现它们是（连贯的）超论的具体实例。这就连接了关于一个理论的逻辑结构的两个不同的思想流派。其中的关键成分，德利涅完备性定理，来自拓扑理论，其中的积极理论已被研究的名义下的连贯的理论。
2022-03-04 math.CT math.LO
The formal spectrum of a tensor-triangulated category
Norwegian University of Science and Technology（挪威科技大学）
本文提出并研究了张量三角范畴的正式谱概念，并在多个数学领域中计算了其示例。
2026-09-14 math.AG math.AT math.CT
