Logic Blog 2023-2024
该文合并2023至2024年的逻辑博客，汇集特定群类与逻辑关系、遍历理论、数学基础及AI定理证明等条目。
2025-03-16 math.LO
Logic Blog 2013
2013年的逻辑博客主要关注以下几点：1.更高的随机性。其中，确定了$Π^1_1$随机性和更高的弱2随机性的Borel复杂度。2.逆向数学及其与随机性的关系。例如，乔丹定理在分析中的力量是什么？(His定理指出，每个有界变差函数是两个非减函数的差。3.随机性和可计算分析。这集中在一个真正的$z$的随机性和勒贝格密度的有效封闭集在$z$的连接。4.探索波兰度量空间的相似关系，如等距，或具有Gromov-Hausdorff距离$0$。特别是他们的复杂性进行了研究。5.可计算性理论和随机性之间的各种联系。
2014-06-19 math.LO
Logic Blog 2018
算法随机性的一些概念被扩展到测量和量子态。有很多关于群论及其与逻辑的关系。这包括了一些关于寡纯群的新结果。还有度量空间和斯科特秩，以及可解释性。
2019-03-14 math.LO
Logic Blog 2014
2014年逻辑博客从新加坡五月IMS计划的开放性问题开始。它包含随机性的结果，包括一些开放性问题的答案。在等价关系和度量空间上有结构性的结果。最后20页包含Bienvenu和Shen关于K-平凡和低K的重合以及相关结果的教程[arXiv：1407.4259]。他们用博弈论的语言阐述了黄金运行。
2015-04-30 math.LO
Logic Blog 2016
今年的逻辑博客包含了各种各样的结果，其中一些只能在这里找到。亮点包括决议的伽马问题的莫宁，和一些条目的拓扑群理论及其连接逻辑。对于Harrington在1978年的一个结果，Yu也给出了一个新的证明：一个具有完美子集的Pi-11超度集包含一个上锥。还有相当多的逆向数学，包括它与随机性的联系，以及在这种情况下Hindman定理的变体。
2017-03-09 math.LO
Logic Blog 2022
2022逻辑博客集中在群论和逻辑的联系上。它讨论了Gardam在2021年对Higman/ Kaplansky单位猜想的反驳，以及它与逻辑和计算的联系。其余的是关于拓扑群的各种，特别是计算理论的tdlc群，和对偶之间的局部Roelcke预紧群和某些可数结构称为满足groupoid。
2023-02-23 math.GR math.LO
A new face of the branching recurrence of computability logic
这封信介绍了可计算性逻辑的分支递归操作的一个新的、实质上简化的版本（见http：//www.cis.upenn.edu/casigiorgi/cl.html），并证明了它与旧的“规范”版本的等价性。
2011-11-21 cs.LO math.LO
Propositional computability logic I
与经典逻辑是真的形式理论一样，最近提出的可计算性逻辑也是可计算性的形式理论。它将（交互式）计算问题理解为机器与环境的博弈，将其可计算性理解为总是赢得博弈的机器的存在，将逻辑运算符理解为计算问题的运算，将逻辑公式的有效性理解为“总是可计算”问题的方案。目前的贡献给出了一个最基本的片段的可计算性逻辑的公理化的合理性和完整性证明的详细阐述。这个片段的逻辑词汇表包含所谓的并行和选择操作的操作符，它的原子代表基本问题，即标准意义上的谓词。这篇文章是自成一体的，因为它解释了所有相关的概念。虽然在技术上没有必要，但是，熟悉基础论文“Introduction to computability logic”[Annals of Pure and Applied Logic 123（2003），pp.1-99]将极大地帮助读者理解可计算性逻辑的哲学，潜在的动机，潜力和实用性，--决定当前结果价值的背景。有关该主题的在线介绍可在http://www.cis.upenn.edu/~giorgi/cl.html和http://www.csc.villanova.edu/~japaridz/CL/gsoll.html上查阅。
2004-06-21 cs.LO math.LO
A propositional cirquent calculus for computability logic
本文提出CL18公理化系统，用于可计算性逻辑的基本命题片段，并证明其相对于该逻辑博弈语义的可靠性与完备性。
2024-11-09 cs.LO math.LO
Computability Logic: a formal theory of interaction
可计算性逻辑是（交互式）可计算性的形式理论，就像经典逻辑是真理的形式理论一样。这种方法最近在“可计算性逻辑导论”（《纯粹与应用逻辑年鉴》123（2003），第1 -99页）中提出。本文重新介绍了可计算性逻辑在一个更紧凑和更少的技术方式。它是写在一个semitutorial风格与一般计算机科学，逻辑或数学观众铭记。关于这一主题的因特网资料可在http：//www.cis.upenn.edu/paggiorgi/cl.html上查阅，其他材料可在http://www.csc.villanova.edu/~japaridz/CL/gsoll.html上查阅。
2004-12-10 cs.AI cs.LO math.LO
Extending and Automating Basic Probability Theory with Propositional Computability Logic
DongA University（东亚大学）
经典概率论是用集合来表述的。本文用命题可计算性逻辑扩展了经典概率论。与其他形式主义不同，可计算性逻辑建立在事件/博弈的概念上，这是概率论的核心。因此，基于CoL的概率理论是有用的{ \it自动化}不确定性推理。我们描述了这个新的概率论的一些基本性质。我们还讨论了一种新的集合运算和可计算性逻辑运算之间的同构。
2020-06-22 cs.AI math.LO math.PR
The taming of recurrences in computability logic through cirquent calculus, Part I
本文构造了一个相应的演算系统，并从可计算性逻辑的语义角度证明了它的可靠性和完备性（见http：//www.cis.upenn.edu/paggiorgi/cl.html）.该系统的逻辑词汇包括否定、平行合取、平行析取、分支递归和分支共递归。这篇文章分两部分发表，（现在的）第一部分包含了一个完整性证明和一个可靠性证明，（即将出版的）第二部分包含了一个完整性证明。
2012-09-19 cs.LO math.LO
The taming of recurrences in computability logic through cirquent calculus, Part II
本文构造了一个相应的演算系统，并从可计算性逻辑的语义角度证明了它的可靠性和完备性（见http：//www.cis.upenn.edu/paggiorgi/cl.html）.该系统的逻辑词汇包括否定、平行合取、平行析取、分支递归和分支共递归。这篇文章分两部分发表，（前）第一部分包含了一个完整性证明，（现在）第二部分包含了一个完整性证明。
2011-06-19 cs.LO math.LO
On the system CL12 of computability logic
可计算性逻辑（参见http：//www.csc.villanova.edu/cnjaparidz/CL/）是一个长期的项目，用于在建设性游戏语义的基础上重新开发逻辑，将游戏视为交互式计算问题的抽象模型。CL 12是经典一阶逻辑的一个保守扩展，它的语言用量词和连接词的所谓选择类扩充了经典逻辑的语言。这个系统已经发现富有成效的应用程序作为皮亚诺算术的建设性和复杂性为导向的版本，如多项式时间可计算性，多项式空间可计算性，和超越算术的逻辑基础。本文介绍了第三个，必不可少的复杂性措施的互动计算称为振幅复杂性，并建立了适当的CL 12相对于A-振幅，S-空间和T-时间的可计算性在一定的最小条件下的三元组（A，S，T）的功能类。这一结果极大地拓宽了CL 12的潜在应用领域。该文件是独立的，目标读者事先不熟悉的主题。
2015-07-25 cs.LO math.LO
Dynamic Probability Logic: Decidability & Computability
本文针对动态概率逻辑（DPL）的可判定性与可计算性展开研究，构建了弱完备且具有限模型性质（可判定）的证明系统$\u001b[1mH\u001b[0m_{DPL}$，还提出强完备证明系统HDPL并证明其典范模型为可计算结构。
2024-06-24 cs.LO math.LO
The intuitionistic fragment of computability logic at the propositional level
从可计算性逻辑的语义出发，给出命题直觉演算的可靠性和完备性证明。后者将公式解释为交互式计算问题，形式化为机器与其环境之间的游戏。直觉主义蕴涵被理解为在最弱的可能性-因此最自然-意义上的算法还原，析取和合取作为问题的确定性选择组合（析取=机器的选择，合取=环境的选择），而“荒谬”作为普遍力量的计算问题。请访问http://www.cis.upenn.edu/~giorgi/cl.html以获得关于可计算性逻辑的全面在线资源。
2006-02-11 cs.AI cs.LO math.LO
Propositional Computability Logic II
可计算性逻辑是关于计算任务和资源的形式化理论。它的公式代表交互式计算问题，逻辑运算符代表计算问题的运算，公式的有效性被理解为总是有算法解决方案的问题的方案。关于这一主题的全面在线资源可在http://www.cis.upenn.edu/~giorgi/cl.html上查阅。早期的文章“命题可计算性逻辑I”证明了可计算性逻辑的最小非平凡片段CL1的可靠性和完备性。本文将这一结果扩展到更有表现力的命题系统CL2。使CL2比CL1更具表达力的是其语言中存在两种原子：基本原子，表示基本计算问题（即谓词），以及一般原子，表示任意计算问题。CL2保守地扩展了CL1，后者只是前者的一般无原子片段。
2004-06-20 cs.GT cs.LO math.LO
Intuitionistic computability logic
可计算性逻辑（Computability Logic，CL）是关于计算任务和资源的系统形式化理论，在某种意义上，它可以被看作是线性逻辑的一种基于语义的替代。凭借其富有表现力和灵活的语言，其中公式表示计算问题，“真理”被理解为算法可解性，CL可能为建设性应用理论和计算系统提供全面的逻辑基础，这些理论和系统本质上需要建设性和计算意义的底层逻辑。其中最著名的构造主义逻辑是海廷的直觉演算INT，其语言可以被看作是CL语言的一个特殊片段。然而，INT的建构主义哲学从来没有真正找到一个直观上令人信服的和数学上严格的语义证明。CL有很好的索赔提供这样一个理由，因此实现了哥洛夫的著名论文“INT =逻辑问题”。本文包含了一个可靠性证明INT的CL语义。有关CL的全面在线资源，请访问http://www.cis.upenn.edu/~giorgi/cl.html
2006-06-14 cs.AI cs.LO math.LO
Toggling operators in computability logic
Shandong University（山东大学）；Villanova University（维拉诺瓦大学）
可计算性逻辑（Computability Logic，CL）（参见http://www.cis.upenn.edu/~giorgi/cl.html）是一个将逻辑重新发展为可计算性的形式理论的研究项目，与传统上的形式真理论相反。CL中的公式代表交互式计算问题，被视为机器与其环境之间的游戏;逻辑运算符代表对这些实体的操作;“真理”被理解为有效解决方案的存在。合作语言的形式是开放的，并可能会经历一系列的扩展，随着研究的进展。到目前为止，已经研究了三种类型的合取和析取：平行的，顺序的和选择的。本文件增加了一个更自然的类型，这个集合，称为切换。切换操作可以被描述为选择操作的宽松版本，其中选择是可伸缩的，允许重新考虑任何有限次数。通过这种方式，他们在交互式计算中模拟试错式决策步骤。本文的主要技术成果是为可计算性逻辑的命题片断构造了一个合理而完整的公理化，它的词汇表和否定一起包括所有四种合取和析取：平行的、切换的、顺序的和选择的。除了切换合取和析取之外，本文还介绍了量词和递归运算的切换版本。
2010-05-01 cs.AI cs.LO math.LO
Towards applied theories based on computability logic
可计算性逻辑（Computability Logic，CL）（见http：//www.cis.upenn.edu/linggiorgi/cl.html）是一个最近启动的程序，用于将逻辑重新发展为可计算性的形式理论，而不是逻辑更传统的形式真值理论。其中的公式代表计算问题，“真理”意味着算法解决方案的存在，而证明则对这些解决方案进行编码。在致力于寻找公理化的CL更有表现力的片段的研究路线，本文介绍了一个新的演绎系统CL 12，并证明了其可靠性和完整性方面的语义CL。保守地扩展了经典谓词演算，并提供了相当多的额外的表达和演绎能力，CL 12提出了一个合理的，计算上有意义的，建设性的替代经典逻辑作为应用理论的基础。为了获得这种理论的模型实例，本文将传统的基于经典逻辑的Peano算法重建为基于可计算性逻辑的Peano算法。本贡献的目的之一是提供一个起点，作者希望，可能成为一个新的研究路线与潜在的有趣的发现-一个探索的可能是相当不寻常的元理论CL为基础的算术和其他CL为基础的应用系统。
2009-11-17 cs.AI cs.LO math.LO
From truth to computability II
可计算性逻辑是关于计算任务和资源的形式化理论。其中的公式代表交互式计算问题，而“真理”被理解为算法的可解性。交互式计算问题，反过来，被定义为某种类型的游戏之间的机器和它的环境，与逻辑运算符代表这种游戏的操作。在为这个语义引入逻辑的增量丰富片段寻找公理化的雄心勃勃的计划中，早期的文章“从真理到可计算性I”证明了系统CL3的可靠性和完备性，其语言具有所谓的平行连接词（包括否定），选择连接词，选择量词和盲量词。本文将这一结果扩展到具有相同逻辑运算符集合的更具表现力的系统CL4。使CL4富有表现力的是在其语言中存在两种原子：基本原子，代表基本计算问题（即谓词，即零交互度的问题），和一般原子，代表任意计算问题。CL4保守地扩展了CL3，后者只是前者的一般无原子片段。从CL4语言中删除盲（经典）量词组，产生一个可判定的逻辑，尽管后者仍然是一阶的。有关可计算性逻辑的全面在线资源可以在http://www.cis.upenn.edu/~giorgi/cl.html上找到
2005-07-20 cs.AI cs.LO math.LO
Sequential operators in computability logic
Villanova University（维拉诺瓦大学）
可计算性逻辑（Computability Logic，CL）（见http：//www.cis.upenn.edu/cnigiorgi/cl.html）是一个语义学平台和研究程序，用于将逻辑重新发展为可计算性的形式理论，而不是传统上的真值的形式理论。CL中的公式代表（交互式）计算问题，被理解为机器与其环境之间的游戏;逻辑运算符表示对这些实体的操作;“真”被理解为有效解的存在，即，算法获胜策略的一部分CL的形式主义是开放式的，并可能会经历一系列的扩展，作为该主题的研究进展。到目前为止，CL一直关注的主要运营商群体是并行，选择，分支和盲运营商。本文介绍了一组新的重要算子，称为序列算子。后者的形式是连续的合取和析取、连续的量词和连续的递归。顾名思义，与这一组相关联的算法直觉是顺序计算的直觉，而不是与并行运算组相关联的并行计算的直觉：玩游戏的顺序组合意味着以顺序的方式一个接一个地玩它的组件。本文件的主要技术成果是一个健全的和完整的公理化的命题片段的可计算性逻辑的词汇，连同否定，包括所有三个-平行，选择和顺序-排序的合取和析取。这一结果的扩展到一阶水平也概述。
2008-10-15 cs.AI cs.LO math.LO
From formulas to cirquents in computability logic
Shandong University（山东大学）；Villanova University（维拉诺瓦大学）
可计算性逻辑（Computability Logic，CoL）（参见http：//www.cis.upenn.edu/cnigiorgi/cl.html）是一个最近引入的语义平台和雄心勃勃的计划，用于将逻辑重新发展为可计算性的形式理论，而不是逻辑传统上的形式真值理论。它的表达式代表了交互式计算任务，被视为机器与环境的游戏，而“真理”被理解为算法获胜策略的存在。CoL的形式主义是开放式的，并且已经经历了一系列的扩展，其中逻辑运算符代表了对游戏的操作。本文以一种全新的方式扩展了CoL的表达能力，将公式（CoL的早期语言仅限于此）推广到称为cirquents的电路式结构。与公式不同，后者能够解释整个游戏/任务的不同部分之间的子游戏/子任务共享。这种能力所提供的许多优点之一是，它允许我们捕获、提炼和概括众所周知的独立友好逻辑，在目前的飞跃之后，它自然成为CoL的保守片段，就像经典逻辑被认为是CoL的基于公式的版本的保守片段一样。并且可以在不熟悉CoL的情况下阅读。
2011-04-27 cs.AI cs.CC cs.LO
A logical basis for constructive systems
这项工作致力于可计算性逻辑（CoL）-哲学/数学平台和长期项目，用于在其底层语义中用可计算性取代真理之后重新开发经典逻辑（见http：//www.cis.upenn.edu/paggiorgi/cl.html）。本文阐述了CoL框架的一些基本复杂性理论。然后证明了演绎系统CL 12关于CoL语义的可靠性和完备性，包括后者基于多项式时间可计算性而不是原则上可计算性的版本。CL 12是一个微积分系统，其中一个变量的含义直观上可以被描述为“后继变量可以在算法上还原为先行变量”，并且其中公式是由谓词字母、函数字母、变量、常数、恒等式、否定式、平行和选择连接词以及盲量词和选择量词构建的。一个案例是CL 12是一个足够的逻辑基础建设性的应用理论，包括复杂性导向的。
2011-03-14 cs.CC cs.LO math.LO
From truth to computability I
可计算性逻辑是最近提出的一种交互计算的形式化理论。有关该主题的全面在线资源，请访问http://www.cis.upenn.edu/~giorgi/cl.html。本文包含了一个合理性和完整性证明的演绎系统CL3公理化的最基本的一阶片段的可计算性逻辑称为有限深度，元素基片段。这一结果的潜在应用领域包括交互计算理论、建设性应用理论、知识库系统、资源约束规划和行动系统。本文件是自成一体的，因为它重新介绍了所有相关定义以及主要动机。
2005-07-20 cs.AI cs.GT cs.LO
The logic of interactive Turing reduction
本文从可计算性逻辑的语义出发，将直觉蕴涵理解为交互式算法约简，给出了直觉演算的蕴涵片段的可靠性和完备性证明。这个概念--更准确地说，是归约的相关概念--是图灵归约从传统的输入/输出问题到任意交互程度的计算任务的概括。请访问http://www.cis.upenn.edu/~giorgi/cl.html以获得关于可计算性逻辑的全面在线资源。
2006-02-11 cs.AI cs.LO math.LO
Foundations of real analysis and computability theory in non-Aristotelian finitary logic
本文概述了最近提出的非阿斯特丽德有限逻辑（NAFL）的实分析和可计算性理论的新范式。NAFL（NRA）中的构造性实分析是通过将欧几里德几何中的图解概念翻译成NAFL版本的皮亚诺算术（NPA）的扩展（NPAR）来完成的。这样的翻译是可能的，因为NPA证明了存在每一个可以用NPA语言定义的自然数的无限真类。NPAR中不允许无限集合，并且禁止对适当类进行量化;因此康托的对角线方法在NRA中不能合法地公式化，并且对于任何实数的集合（“超类”）都没有“基数”。经典实分析的许多有用的方面，如牛顿和莱布尼茨的微积分，在NRA中是合理的。但悖论，如芝诺的运动悖论和巴拿赫-塔斯基悖论，解决，因为NRA只承认封闭的实数超类，特别是，开放/半开区间的实数是不允许的。NAFL版本的可计算性理论（NCT）拒绝了图灵关于停机问题的不可判定性的论证，并允许超计算。NCT的重要潜在应用是在量子和自主计算领域。
2005-09-29 cs.LO math.GM math.LO
In the beginning was game semantics
本文概述了可计算性逻辑--交互式计算任务和资源的游戏语义构造逻辑。只有一个非概述，在它的技术部分，致力于证明健全的仿射逻辑方面的语义可计算性逻辑。有关该主题的全面在线资源可以在http://www.cis.upenn.edu/~giorgi/cl.html上找到
2008-10-24 cs.AI cs.LO math.LO
Introduction to Cirquent Calculus and Abstract Resource Semantics
本文介绍了一种改进的微积分的方法，称为cirquent演算。而在Gentzen风格的证明树兄弟姐妹（或堂兄弟姐妹等）序列是不相交的公式序列，在圆微积分中，它们可以共享元素。明确地允许或禁止共享资源，从而将子结构逻辑的资源感知直觉带到一个更微妙的层次，cirquent演算提供了比cirquent演算更大的灵活性和功能。随着可计算性逻辑的诞生，对新的演绎工具的需求也随之而来（见http：//www.cis.upenn.edu/linggiorgi/cl.html）--这是一种语义构建的计算资源形式理论，它顽固地抵制了传统句法方法框架内的任何公理化尝试。循环微积分打破了僵局。从其规则的全部集合中去除收缩，产生了可计算性逻辑的基本片段CL 5的健全和完整的系统。另一方面，在微积分中做同样的事情，会把婴儿和洗澡水一起扔掉，导致严格较弱的仿射逻辑。可计算性逻辑的一个隐含的主张是，它是CL 5，而不是仿射逻辑，充分体现了传统上与后者相关的资源哲学。为了加强这一主张，本文进一步引入了一个抽象的资源语义，并显示了CL 5的可靠性和完整性。
2005-12-23 cs.LO math.LO
Algebra of Self-Replication
本文提出使用可通过项重写判定的极小等式逻辑来检验可计算性理论，并对两个可判定片段中的 quine 程序进行分类，解释了其本质相似性。
2023-11-19 cs.LO math.LO
Many concepts and two logics of algorithmic reduction
在为可计算性逻辑的各个部分寻找公理化的程序中，早先证明了交互式图灵归约逻辑正是海廷直觉主义演算的蕴涵片段。这种简化允许对前件所表示的计算资源进行无限的重用。然而，一种至少同样基本和自然的算法简化是不允许这种重用的。本文表明，把第一类归约的逻辑转变为第二类归约的逻辑，只需要从它的根岑式公理化中删除收缩规则。第一种（图灵）交互式约简也有三种自然版本。虽然这三个版本彼此非常不同，但它们的逻辑行为（孤立地）是无法区分的，而这种共同行为被隐含的直觉主义逻辑精确地捕获。在本文的其他贡献是一个非正式的介绍了一系列新的-有限和有界-版本的递归操作和相关的减少操作。有关可计算性逻辑的在线资源可在http://www.cis.upenn.edu/~giorgi/cl.html上找到
2008-10-12 cs.LO math.LO
Introduction to clarithmetic I
“Clarithmetic”是一个与皮亚诺算术类似的形式数论的通用名称，但基于可计算性逻辑（参见http：//www.cis.upenn.edu/classgi/cl.html），而不是更传统的经典或直觉逻辑。claithmetical理论的公式代表交互式计算问题，它们的“真理”被理解为算法解的存在。对这些解决方案施加各种复杂性约束会产生各种版本的clarithmetic。本文介绍了一个多项式时间可计算性的算法体系，该体系是完善的。在这个意义上，系统的每个定理T都代表一个具有多项式时间解的交互数论计算问题，而且，这样的解可以有效地从T的证明中提取出来。完备性的意义在于，每一个具有多项式时间解的交互数论问题都由系统的某个定理T表示。这篇论文是写在semitutorial风格和目标读者事先不熟悉可计算性逻辑。
2011-08-23 cs.CC cs.LO math.LO
Modified realizability subtoposes and total Weihrauch reducibility
Graduate School of Informatics and Graduate School of Mathematics, Nagoya University（名古屋大学情报大学院和数学研究生院）
该研究在全可计算框架下提出归约概念，利用层子拓扑分离了弱排中律、小有限全知原则与马尔可夫原则等逻辑原则的层级。
2026-08-04 cs.LO math.LO
