Positive model theory and infinitary logic
研究了h-归纳理论的正型空间上的对偶谱拓扑的基本性质及其与无穷逻辑的本质联系。拓扑是Hausdorff，具有Baire性质，其紧性表征正模型完全性;它也具有闭集的基，并由几何逻辑的公式描述。在无限逻辑的所有运算下，“几何类型”在类型空间中是封闭的，我们引入了存在泛结构的一个正模拟，通过它我们解释了正类型空间中的完全一阶逻辑.这表明如何“积极的$ω$ -饱和”是一个基本的正和无穷逻辑之间的联系，我们建议一个几何模拟的积极Morleyisation。
2015-01-05 math.LO
Infinitary first-order categorical logic
我们提出了一个统一的分类处理的几个经典和直觉无穷逻辑的完备性定理的建议公理化。这提供了新的完备性定理，并包含了Gödel，Kripke，Beth，Karp，Joyal，Makkai和Fourman/Grayson以前的定理。作为应用，我们利用大基数假设证明了无穷直觉一阶逻辑的析取性和存在性。
2017-01-05 math.CT math.LO
Algebraic Proof Theory for Infinitary Action Logic
本文提出一种统一方法，通过结合非良基证明理论与代数证明理论工具，为各类 *-连续作用代数构建可靠完备的无切序列式证明系统。
2025-01-30 cs.LO math.LO
Hyperarithmetical Complexity of Infinitary Action Logic with Multiplexing
本文针对带多路复用的无穷动作逻辑$!^m\nabla \mathrm{ACT}_\omega$的可推导性问题，证明其在图灵归约下为$\Delta^0_{\omega^\omega}$-完全，确定其闭包序数为$\omega^\omega$，并给出相关片段的复杂度结果。
2023-12-09 cs.LO math.LO
Expressive power of infinitary [0, 1]-valued logics
我们认为模型理论的性能有关的表达能力的三个类似物的$L_{ω_1, ω}$度量结构。我们给出了一个例子表明，这些无穷逻辑之一是严格的表达比其他两个，但也表明，所有三个具有相同的基本等价关系完全可分度量结构。证明了完备可分度量结构上的连续函数是自同构不变的当且仅当它在更有表现力的逻辑中是可定义的。我们的几个结果与完全可分度量结构的Scott句的存在性有关。
2017-08-09 math.LO
Infinitary logic and basically disconnected compact Hausdorff spaces
本文推广了Kukasiewicz逻辑，得到了以代数$C(X,[0,1])$为模型的无穷逻辑$\mathcal{IR}Ł$，其中$X$是基本不连通的紧T2空间.等价地，我们的模型是$σ$ -完备Riesz空间中的单位区间，具有强单位。$\mathcal{IR}Ł$的Lindenbaum-Tarski代数在同构下是$[0,1]$ -值Borel函数的代数。最后，我们的系统享有标准的完整性方面的实区间$[0,1]$。
2018-04-18 math.FA math.LO
Isomorphic limit ultrapowers for infinitary logic
在[Sh：797]中引入的逻辑L^1_θ;它是低于L_θ θ的极大逻辑，其中良序是不可定义的。我们研究它的θ一个紧凑的基数。我们证明了它满足一阶逻辑的几个平行的经典定理，加强了它是自然逻辑的论点。特别地，两个模型是L^1_θ等价的当且仅当对于θ-完全超滤子的某个ω-序列，这两个模型的迭代超幂是同构的。
2021-08-09 math.LO
Infinitary propositional relevant languages with absurdity
对无穷命题相关逻辑建立了Scott同构定理、Karp定理以及缺乏紧性和强完备性的类似结果。无限数量布尔逻辑$L_{\infty ω}$的一个“内插定理“（由Barwise和van Benthem引入的一种特殊类型）成立。这产生了一个保存结果，表征了表达能力的无穷相关语言的荒谬使用模型理论关系的相关定向互模拟以及贝丝可定义性属性。
2018-09-21 math.LO
Realisability for Infinitary Intuitionistic Set Theory
我们介绍了一个基于有序图灵机（OTM）的无穷直觉集合论的可实现性语义。我们表明，我们的OTM-可实现性的概念是健全的某些系统的无穷直觉主义逻辑，并实现了所有公理的无穷Kripke-Platek集合论。最后，我们使用我们的可实现性概念的一个变体来证明（有限）直觉Kripke-Platek集合论的命题容许规则正是直觉命题逻辑的容许规则。
2022-12-13 math.LO
On Some Infinitary Logics
本文定义了一类推广 Shelah 逻辑 $\mathbb L^1_κ$ 的无穷逻辑 $\mathscr L^1_{κ,α}$，研究不同参数下这些逻辑之间的关系，并给出可定义性例子及基于 $ϕ$-子模型关系的 Lindström 定理新版本。
2024-02-20 math.LO
Nice infinitary logics
普通无穷语言L_{lambda, kappa}仅在lambda <= {aleph_1}，kappa = {aleph_0}的情况下才满足内插定理，这当然包括一阶逻辑。也有一些这样的逻辑对满足插值，例如（L_{lambda^+，{aleph_0}}，L_{(2^lambda)^+, lambda^+}）。这是否来自一个满足它的中间逻辑？是不是很漂亮？独一无二？对于kappa = beth_kappa，我们定义了一个新的逻辑L^1_kappa，使得L_{kappa omega} < L^1_kappa LL_{kappa kappa}，并且L^1_kappa非常好，特别是满足内插定理。此外，L^1_kappa还具有Lindstrom定理形式的模型论特征，即良序的不可定义性。对于共尾性aleph_0的强极限kappa，我们定义了一个逻辑L^2_{kappa^+}，使得L^2_{kappa^+，{aleph_0}}<L^2_{kappa^+}< L_{kappa^+, kappa}且L^2_{kappa^+}满足内插定理.
2011-06-10 math.LO
Infinitary provability logic
Ghent University（根特大学）；Steklov Mathematical Institute of the Russian Academy of Sciences（俄罗斯科学院列别捷夫数学研究所）
本文研究Gödel-Löb可证性逻辑的无穷性对应物，提出非良基深层推理系统$\dgla$，证明其相对于良基传递Kripke框架的可靠性与完备性，并借助Kripke-Platek集合论建立无穷可证性解释，表明Hilbert式变体可靠，且在某些条件下无穷可证性逻辑介于两者之间。
2026-09-22 math.LO
Action Logic is Undecidable
作用逻辑是剩余Kleene格的代数逻辑（不等式理论）。这个逻辑涉及克莱因星，通过归纳方案公理化。对于使用$ω$ -规则的更强系统（无限动作逻辑），Buszkowski和Palka（2007）证明了$Π_1^0$ -完备性（因此，不可判定性）。行动逻辑本身的可判定性是一个开放性问题，由D. 1994年的Kozen。在这篇文章中，我们证明了它是不可判定的，更准确地说，是$Σ_1^0$ -完全的。我们还证明了相同的复杂性结果之间的所有递归可重复的逻辑动作逻辑和无穷动作逻辑;片段的那些只有一个的两个格（添加剂）连接;为行动逻辑扩展的分配律。
2019-12-24 cs.LO math.LO
On structural proof theory of the modal logic K+ extended with infinitary derivations
本文研究模态逻辑K+在加入无穷推导后的结构证明论，提出允许非良基证明的矢列演算，并利用连续切割消去方法证明切割消去定理，同时说明K+的普通证明可视为循环无切割证明。
2023-10-16 math.LO
A Note on Extensions of Infinitary Logic
我们发现，一个强形式的所谓的Lindstrom定理未能推广到扩展的L_{kappa,omega}和L_{kappa,kappa}：对于弱紧κ有没有最强的扩展L_{kappa,omega}与（κ，κ）-紧性和Lowenheim-Skolem定理到κ。在一个额外的集合论假设下，没有L_{kappa,kappa}的最强扩展具有（kappa，kappa）-紧性和Lowenheim-Skolem定理直到<kappa。
2000-09-07 math.LO
Completeness and interpolation for intuitionistic infinitary predicate logic, in connection to finitizing the class of representable Heyting polyadic algebras
研究了Heyting多进代数的各种约简的表示定理。超合并证明了几个（自然约简）和我们的结果进行了比较，在经典代数逻辑处理圆柱和polyadic（布尔代数）的有限性问题。我们还证明了几个新的整齐嵌入定理，并得到了基于（广义）Kripke语义的可表示代数类与具有整齐嵌入性质的代数类，即那些代数是具有$ω$额外维数的代数的次整齐约化.
2013-04-04 math.LO
Expressive Power of Infinitary Logic and Absolute co-Hopfianity
针对绝对余Hopf群，本文利用无穷逻辑证明第一个优美基数之上不存在绝对余Hopf阿贝尔群，且将结果推广到交换环模范畴，解决了其存在性与大小限制问题。
2024-11-27 math.AC math.GR math.LO
Infinitary Logics and Abstract Elementary Classes
本文证明了抽象初等类可以在特定无限逻辑中被公理化，并引入了canonical tree概念，探讨了其与新逻辑的关系。
2025-11-27 math.LO
Stationary sets and infinitary logic
设K^0_lambda为结构< lambda，<，A>的类，其中A subseteq lambda与俱乐部不相交，设K^1_lambda为结构< lambda，<，A>的类，其中A subseteq lambda包含俱乐部。我们证明了如果lambda = lambda^{< kappa}是正则的，那么L_{lambda^+ kappa}中没有一个句子能把K^0_lambda和K^1_lambda分开.另一方面，我们证明了如果lambda = mu^+，mu = mu^{< mu}，并且一个强制公理成立（并且如果mu = aleph_0，aleph_1^L= aleph_1），则存在一个L_{lambda lambda}的句子，它将K^0_lambda和K^1_lambda分开。
1997-06-15 math.LO
Complexity of the Infinitary Lambek Calculus with Kleene Star
本文证明了带 Kleene 星的无穷 Lambek 演算的可推导性问题是 $\Pi_1^0$-困难的，解决了 Buszkowski 的开放问题，并作为副产品证明了不含空词的上下文无关语言可由唯一类型赋值的 Lambek 文法生成。
2020-05-01 cs.LO math.LO
A complete axiomatization of infinitary first-order intuitionistic logic over $\mathcal{L}_{κ^+, κ}$
给定一个弱紧基数$κ$，给出了$\mathcal{L}_{κ^+, κ}$上直觉一阶逻辑的公理化，并证明了它对于Kripke模型是可靠的和完备的.因此，我们得到了该逻辑的析取和存在性质。这推广了Nadel关于$\mathcal{L}_{ω_1, ω}$上的直觉主义逻辑的工作。当$κ$是一个正则基数使得$κ^{<κ}=κ$时，我们通过一个简单的证明修改，推导出$\mathcal{L}_{κ^+, κ, κ}$上的直觉一阶逻辑的一个完全公理化，该语言具有至多$κ$公式的析取，小于$κ$公式的合取和小于$κ$许多变量的量化.特别地，这适用于广义连续统假设下的任何正则基数。
2020-12-28 math.LO
Infinitary Axiomatizability of Slender and Cotorsion-Free Groups
在无限逻辑L_{infty,omega_1}和L_{infty,omega}中，细长和无余挠阿贝尔群类分别是可公理化的. Baer-Specker群Z^ω不是L_{infty,omega_1} -等价于细长群。
1999-10-28 math.LO
Cartagena Logic
本文引入一种基于布尔扩张的新型无穷逻辑——卡塔赫纳逻辑，证明其模型论性质，并表明它是Shelah无穷逻辑的一个具有清晰生成语法的良好近似。
2024-02-07 math.LO
Boolean valued semantics for infinitary logics
本文利用力迫法改进Mansfield的布尔值完备性定理，针对无穷逻辑L∞ω建立更强完备性，并证明Craig插值性质与强省略类型定理，同时揭示L∞ω与力迫法的联系。
2023-05-12 math.LO
Categoricity and infinitary logics
我们指出了一个差距在Shelah的证明以下结果：$\mathbf{Claim}$让$K$是一个抽象的小学类范畴在unboundedly许多基数。则存在基数$λ$使得无论何时$M, N \in K$的大小至少为$λ$，$M \le N$当且仅当$M \preceq_{L_{\infty, \text{LS} (K)^+}} N$。这一主张的重要性在于以下定理，这一定理隐含在希拉的工作中：$\mathbf{Theorem}$假设这一主张。设$K$是一个抽象初等类，它在无限多基数中是范畴的。然后$λ$的类使得：1）$K$在$λ$中是范畴的; 2）$K$在$λ$中具有合并;以及3）存在好的$λ$ -框架，其基础类$K_λ$是平稳的。给出了一个证明，并讨论了相关问题.
2015-10-16 math.LO
Representation theorems in modal logic using algebraic logic
证明了无穷谓词模态逻辑的几个表示定理
2013-04-03 math.LO
Chain Logic and Shelah's Infinitary Logic
对于$κ=\beth_κ$形式的基数，Shelah的逻辑$L^1_κ$具有满足良序强不可定义性（SUDWO）的在$\bigcup_{λ<κ} L_{λ, ω}$之上的极大逻辑的特征。SUDWO强化了良好秩序的不可定义性（UDWO）。证明了当$κ$是可数共尾奇异时，Karp链逻辑\cite{Karpintroduceschain}在$L^1_κ$之上，而已知它满足UDWO和插值.此外，我们表明，在这些情况下，链逻辑是-在某种意义上-最大的逻辑链模型，以满足UDWO。然后，我们表明，链逻辑给出了问题1.4的部分解决方案。从Shelah的\cite{Sh797}，其中询问是否有一个严格的逻辑之间的$ L_{κ^+, ω}$和$L_{κ^+, κ^+}$具有插值的可数共尾性的$κ$单数。我们表明，模接受的上界模型类的$L_{κ, κ}$，卡普的链逻辑满足所需的属性。此外，我们表明，这个链逻辑是不是$κ$ -紧凑的，一个问题，我们问过在各种场合。我们通过证明并引理和识别链独立的逻辑片段，为链逻辑的进一步发展做出了贡献，表明它仍然具有相当的表达能力。最后，我们证明了简单定义的链逻辑在满足插值、良序不可定义性和极大性以及并引理方面模拟了逻辑$L^1_κ$。此外，它还有一个完备性定理。
2021-07-21 math.LO
Classifying toposes for non-geometric theories
该研究针对一阶、亚一阶、经典三种无穷逻辑的非几何理论，通过限制几何态射类型或限定布尔拓扑斯定义对应分类拓扑斯，证明了亚一阶与布尔情形下分类拓扑斯存在性的类似结论，并得到两类无穷逻辑相对于拓扑斯的完备性结果。
2023-12-14 math.CT math.LO
Pointed Modal Abelian Logic, Algebraically
Institute of Computer Science of the Czech Academy of Sciences（捷克科学院计算机研究所）；Department of Algebra, Faculty of Mathematics and Physics, Charles University（查理大学数学物理学院代数系）
本文研究实数的点态模态逻辑，通过有界赋值建立克里普克语义，并引入负点态模态阿贝尔l-群簇，利用无穷阿基米德规则证明无穷代数完备性。
2026-08-04 cs.LO math.LO
On logics extended with embedding-closed quantifiers
我们研究一阶以及无限逻辑扩展下嵌入封闭向上的量词。特别是，我们表明，如果一个链的准齐次结构是足够长的，那么一个给定的公式，这样的逻辑最终相当于一个量化器的自由公式在该链。我们利用这一事实产生了一些不可定义的结果与嵌入封闭量词的逻辑。在最后一节中，我们介绍了一个Escherichfeucht-Fraïssé博弈，它刻画了结构之间的$L$ -等价，其中$L$是用所有嵌入闭量词扩展的无限逻辑$L_{\infty ω}$。最后，我们提供了这个游戏的应用程序，说明其使用。
2014-07-03 math.LO
Completeness of infinitary heterogeneous logic
给定正则基数$κ$使得$κ^{<κ}=κ$（例如，如果广义连续统假设成立），我们开发了一个用于经典无穷逻辑的证明系统，该系统包括异构量化（即，量词的无限交替序列），其中存在至多$\mathcal{L}_{κ^+, κ}$的任何公式的合取和析取，并且量化（包括异构的）被应用于小于$κ$的许多变量。这种类型的量化在$\mathcal{S}et$中使用通常的二阶公式来解释游戏策略，并且公理基于游戏语义的确定性公理的更强变体。在这个公理系统中，我们证明了关于一类集值结构的可靠性和完备性定理，我们称之为良定的。虽然这个类比Takeuti的确定性逻辑中的确定性结构类更具限制性，但完备性定理在我们的情况下适用于更广泛的$\mathcal{L}_{κ^+, κ}$公式，并且异质理论的良好确定模型的范畴是可访问的。我们的系统是制定内的分类逻辑，我们不需要强加任何具体的要求，证明树，从而无视Takeuti的系统所需的特征变量条件。我们还调查了直觉系统的异构量词和证明类似的完备性定理，以及确定的结构在一般的类别，在$κ$ -Grothendieck toses特别是，当$κ^{<κ}=κ$，也在克里普克模型。最后，我们考虑了我们的系统中的异构量化与受囿量词是可表达的扩展，并扩展我们的完整性结果的情况下。
2019-01-31 math.CT math.LO
Internalising modified realisability in constructive type theory
一个修改后的可实现性解释的无穷逻辑形式化，并证明了健全的建设性类型理论（CTT）。所考虑的逻辑包括一阶逻辑。这种解释使得提取具有简化类型的程序并在CTT中对其进行合并和推理成为可能。
2005-10-05 cs.LO math.LO
Practical and Structural Infinitary Expansions
本文引入了无穷逻辑扩张，证明其保持并反映嵌入 Ramsey 性质和建模性质，去除了 Scow 定理的技术假设，并强化了 Kechris-Pestov-Todorcevic 对应。
2023-06-27 math.CO math.LO
A note on restriction rules
本文研究限制规则，证明在仅需推导给定模型完全理论时，可省略可数性假设，并将巴怀斯定理推广至任意基数词汇表及超紧基数下的无穷逻辑。
2023-12-28 math.LO
Reasoning in circles
循环证明，由Daniyar Shamkanov引入，是允许假设不是公理但沿着分支至少出现两次的证明。Shamkanov证明了一个公式完全属于可证明性逻辑GL，如果它在模态逻辑K4中有循环证明。Shamkanov使用Tait风格的证明系统和无穷证明。在本文中，我们证明了同样的结果，但然后对微积分和没有绕道通过无穷系统。我们还得到了一个温和的概括的结果，这意味着它的直观的模拟举行。
2021-12-30 math.LO
Modal Measurable Logics via a Modal Loomis-Sikorski Representation Theorem
University of Amsterdam（阿姆斯特丹大学）；University of Bern（伯尔尼大学）；Indiana University（印第安纳大学）
提出一种带模态的无穷可数合取与析取逻辑，用于动力系统和点自由遍历理论的测度论工作，并通过Jonsson-Tarski对偶和Loomis-Sikorski定理证明其相对于新Kripke语义的完备性。
2026-07-01 cs.LO math.LO
Dynamic Probability Logics: Axiomatization & Definability
本文引入动态概率逻辑DPL及其无穷扩张，给出希尔伯特式公理化并证明强完全性，进而研究保测、遍历、混合等性质的可定义性，并证明带初始分布的马尔可夫过程的平稳性、不变性、不可约性和常返性在无穷概率逻辑中可定义。
2024-01-14 math.LO
Commutative Action Logic
我们证明了不可判定性，并指出了交换动作逻辑，即交换剩余Kleene格（动作格）的方程理论，和无限交换动作逻辑，*-连续动作格的方程理论的算术层次的地方。即证明了前者是$Σ_1^0$ -完全的，后者是$Π_1^0$ -完全的.因此，情况与更好地研究的非对易情形相同。然而，使用的方法是不同的：我们编码计数器（明斯基）机器的无限和循环计算。
2021-02-23 math.LO
Beth definability and the Stone-Weierstrass Theorem
紧T2空间的Stone-Weierstrass定理是泛函分析的一个基本结果，具有深远的影响。我们介绍了一个方程逻辑$\vDash_Δ$与一个无限品种$Δ$和表明，斯通-维尔斯特拉斯定理是一个后果的贝思可定义性属性的$\vDash_Δ$，说明每一个隐式定义可以明确。进一步，我们定义了一个无穷命题逻辑$\vdash_Δ$，并证明了一个强完备性结果，由此与$\vdash_Δ$相关的结果的语义概念与$\vDash_Δ$一致.
2021-05-06 math.FA math.GN math.LO
Linear Logic via algebra I: Girard algebras
DIISM, Università di Siena（锡耶纳大学）；University of Priština in Kosovska Mitrovica（普里什蒂纳大学）
本文研究作为乘性加性线性逻辑等价代数语义的Girard代数，明确其代数结构、子簇格性质，构造多样原子并得到$\textsf{MALL}$的$2^{\boldsymbol{\text{aleph}_0}}$个Post完全扩张。
2026-10-14 math.LO
Reasoning from hypotheses in *-continuous action lattices
本文研究 ∗-连续动作格中带假设的 Horn 推理复杂性，通过翻译到带幂乘的无穷动作逻辑，证明不含 ∗ 假设片段为严格超算术，而仅含交换性假设时降至 Π^0_1。
2025-02-17 math.LO
Quantum Logic in Intuitionistic Perspective
在他们的开创性论文伯克霍夫和冯诺依曼揭示了以下困境：“.对于逻辑学家来说，否定的正交互补性质是最经不起批判性分析的性质，而力学的研究则指出，分配恒等式是逻辑代数中最薄弱的环节。“在本文中，我们消除了这种困境，提供了一种同时保持两者的方法。通过在物理系统的性质格中引入“缺失”的析取，同时将交作为合取继承，我们得到了一个关于物理性质的完备的Heyting命题命题代数代数.特别是有一个双射之间的对应关系的性质格和命题格配备了所谓的操作决议，一个操作，暴露的性质的水平上的命题。如果属性格配备了一个正交补，那么这个双射对应可以被细化为一个配备了运算补的命题格，这样就建立了上面的主张。从形式上讲，通过物理和逻辑上的考虑，我们分别重新发现了Bruns和Lakser（1970）关于交半格的内射壳的纯数学结果的一个规范和一个改进。从我们的表示，我们可以得到一个真正直观的功能性的影响，财产格，因此面对索赔在以前的著作就此事。我们还对析取性与分配性、有限与无限合取性作了详细的分析，简要地回顾了Bruns-Lakser构造并指出了一些有待解决的问题。
2002-04-22 math-ph math.LO math.MP
Set theory, logic, and homeomorphism groups of manifolds
Iowa State University（爱荷华州立大学）；University of Virginia（弗吉尼亚大学）；Korea Institute for Advanced Study (KIAS)（韩国高等研究院）；University of Maryland, College Park（马里兰大学帕克分校）
研究公理集合论与流形同胚群一阶理论的关系，通过构建性公理（V = L）证明同胚群的一阶刚性等，在正则假设下得出不同结论，还表明无穷公式可确定同胚类和流形类型。
2026-07-07 math.GR math.GT math.LO
