Realizability Interpretation of PA by Iterated Limiting PCA
对于任何部分组合代数(简称PCA)A,从N到A的A-可表示部分函数类被N的余有限集滤子所表示,是一个PCA,使得可表示部分函数恰是A-可表示部分函数的极限部分函数(Akama,“Limiting partial combinatory algebras”Theoret. Comput. Sci. Vol.311 2004)。这种构造的n次迭代导致表示任何n次迭代的极限部分递归函数的PCA,并且PCA在所有n上的归纳极限是表示任何算术部分函数的PCA。Kleene对前一种PCA的可实现性解释解释了双否定消去的逻辑原理,对后一种PCA的可实现性解释解释了Peano算术(简称PA)。利用Heyting算术与PA之间的逻辑系统层次,讨论了HA的前束范式定理、相对化的前提独立方案,以及PA是HA的无界扩张. "
2013-07-21 math.LO
Realizability of Univalence: Modest Kan complexes
适度Kan复形是关于Horn包含体$Λ_k[n] \to Δ[n]$具有右提升性质的适度单纯集。本文发展的范畴逻辑,需要表明,有一个适度的Kan复合物之间的单纯组装的单价宇宙。
2016-04-16 math.CT math.LO
Every metric space is separable in function realizability
本文在函数可实现性拓扑中证明所有度量空间可分、可判定相等性对象可数,并推广到合成拓扑,表明直觉主义逻辑无法证明不可分空间或不可数可判定集合的存在。
2019-05-22 cs.LO math.LO
A $j$-translation with Kripke forcing relation
Graduate School of Informatics, Nagoya University(名古屋大学情报学研究科)
本文提出一种结合j-翻译与Kripkeforcing的内部逻辑拓扑学翻译,证明其对直觉逻辑和Heyting算术的正确性,并扩展了de Jongh和Goodman的sheaf模型。
2026-03-20 math.CT math.LO
An intuitionistically complete system of basic intuitionistic conditional logic
本文提出基本直觉主义条件逻辑IntCK,证明其相对克里普克模型和一阶直觉主义逻辑翻译的完备性,并分析其与CK、IK及Weiss的ICK的关系,讨论候选系统的优劣。
2023-06-17 math.LO
A Canonical Model for Constant Domain Basic First-Order Logic
对Visser基本命题逻辑的常域一阶扩展--常域基本一阶逻辑(BQLCD)建立了一个规范模型,并利用该规范模型证明了BQLCD满足析取和存在性质。
2020-05-20 math.LO
A basic system of paraconsistent Nelsonian logic of conditionals
该研究为基于次协调纳尔逊强否定逻辑变体$\u27a2N4$的条件句逻辑定义Kripke语义,公理化极小系统$\u27a2N4CK$,并通过嵌入关系揭示其与已有直觉主义条件句逻辑、$\u27a2N4$基模态逻辑的紧密关联。
2023-11-04 math.LO
Expressive power of basic modal intuitionistic logic as a fragment of classical FOL
本文讨论了模态直觉主义逻辑的Kripke式语义的四种不同版本所导出的一阶逻辑片断。为了捕捉这些片段,asimulation的概念进行了修改和扩展,以产生Van Benthem类型的语义表征各自的表达能力。它示出,进一步,这种特征可以很容易地进行到任意一阶可定义的子类的经典一阶模型。
2015-11-06 math.LO
Completeness in local positive logic
本文提出融合正逻辑与局部逻辑的局部正逻辑,并系统研究其紧致性、正封闭性与完备性等基础模型论性质。
2025-03-14 math.LO
A Deep-Inference Sequent Calculus for Basic Propositional Team Logic (Without Delving Too Deep)
本文为包含分裂析取与探究析取的基础命题团队逻辑引入了一种深度推理矢列演算,证明了其保高度弱化、切消除等性质,并导出了新的Lyndon插值定理。
2025-08-10 math.LO
Topological Semantics and Decidability
众所周知,所有拓扑空间的基本模态逻辑是$S4$。然而,满足各种分离公理的空间类的基本模态和混合逻辑的结构直到现在还不清楚。本文证明了$T_0$、$T_1$和$T_2$拓扑空间的模态逻辑是重合的,并且是S4 $. We also examine basic hybrid logics of these classes and prove their decidability; as part of this, we find out that the hybrid logics of $ T_1 $ and T_2$空间重合的.
2007-06-01 math.LO
Infra-topologies revisited: logic and clarification of basic notions
在本文中,我们坚持定义的infra-拓扑空间,因为它是由铝Odhari介绍。也就是说,我们说的家庭的子集,其中包含空集和整个宇宙X,在同一时间关闭有限的交集(但不一定在任意或甚至有限的工会)。这种轻微的修改允许我们区分新的子集类别(infra-open,ps-infra-open和i-genuine)。类似的概念在闭包语言中讨论。研究了极小亚开集类,以及广义亚空间的概念。最后,我们利用上面介绍的一些概念,用模态逻辑得到了亚空间的特征。
2021-01-06 math.LO
A Basic Łukasiewicz m-valued conditional logic
本文基于 Łukasiewicz m 值命题逻辑构造了条件逻辑系统 ŁCR,通过将条件句和可及关系推广至 m 值建立世界语义,证明了其可靠性、完备性与有限模型性。
2024-07-27 math.LO
Compactness of first-order fuzzy logics
一阶逻辑的一个优良性质是可满足性的紧性。它指出一个可满足的理论是可满足的。然而,多值逻辑的可满足性程度不同,导致了这些逻辑的各种紧性。其中一个问题是$K$ -可满足性的紧性。在这里,在综述了基于连续t-范数(基本逻辑)的多值逻辑中的可满足性的紧性和$K$ -可满足性的紧性的结果之后,我们扩展了围绕这一主题的结果。为此,我们考虑基本逻辑的反向语义意义。然后我们在$[0,1]$和$[0,1]^2$上引入了一个拓扑,使得所有逻辑连接词的解释关于这些拓扑是连续的。最后利用这一事实推广了基本逻辑中可满足性紧性的结果。
2019-05-04 math.LO
Coalgebraic Geometric Logic: Basic Theory
本文利用余代数理论,为命题几何逻辑引入模态词,构建统一框架,研究推导系统、可靠性与完备性,并比较模态等价、行为等价与互模拟,提供终对象。
2022-12-07 math.LO
Separating the basic logics of the basic recurrences
本文表明,即使在最基本的水平上,并行,可数分支和不可数分支递归的可计算性逻辑(见http://www.cis.upenn.edu/caugiorgi/cl.html)验证不同的原则。
2011-11-15 cs.LO math.LO
Residuated Basic Logic II. Interpolation, Decidability and Embedding
证明了剩余基本逻辑$\mathsf{RBL}$的逻辑演算$\mathsf{L_{RBL}}$具有强有限模型性质,并证明了直觉主义逻辑可以嵌入到基本命题逻辑$\mathsf{BPL}$中.因此,$\mathsf{RBL}$是可判定的。证明了剩余基本代数类具有有限可嵌入性,$\mathsf{BPL}$是PSPACE完备的,直觉主义逻辑可以嵌入模态逻辑$\mathsf{K4}$ .
2014-02-24 cs.LO math.LO
Some modal and temporal translations of generalized basic logic
我们介绍了一个家庭的模态扩展的Mukasiewicz逻辑,旨在适应模态翻译的广义基本逻辑(制定与交换,弱化,和假)。我们进一步展示代数语义在这个家庭中的每个逻辑,特别是显示,所有这些都是代数化的意义上的Blok和Pigozzi。利用这个代数化的结果和相关品种的同余分析,我们建立了每一个引进的模态dukasiewicz逻辑有一个局部演绎分离定理。利用Jipsen和Montagna的偏序集积构造方法,我们给出了广义基本逻辑的两种具有交换、弱化和虚假的翻译,其翻译风格类似于著名的Gödel-McKinsey-Tarski翻译。第一个解释广义基本逻辑在模态的Mukasiewicz逻辑在经典的模态逻辑S4的精神,而第二个解释广义基本逻辑在后者的时间变体。
2021-06-10 cs.LO math.LO
Monadic BL-algebras: the equivalent algebraic semantics of Hájek's monadic fuzzy logic
本文引入了一元BL-代数簇作为赋有两个一元算子$\forall$和$\exists$的BL-代数.经过研究的基本性质,这个品种,我们表明,这类是等价的代数语义的一元片段的哈耶克的基本谓词逻辑。此外,我们开始了一元BL-代数的主要子簇的系统研究,其中一些构成了著名的一元逻辑的代数语义:一元哥德尔逻辑和一元Kukasiewicz逻辑。在最后一节中,我们给出了全序一元BL-代数的一个完整刻画。
2016-09-16 math.LO
Residuated Basic Logic I
研究了剩余基本代数的剩余基本逻辑($\mathsf{RBL}$),其中Visser的基本命题逻辑($\mathsf{BPL}$)的基本蕴涵被解释为非结合二元算子$\cdot$(积)的右剩余.本文建立了剩余基本代数的代数系统$\mathsf{S_{RBL}}$,证明了$\mathsf{RBL}$是$\mathsf{BPL}$的保守扩张.给出了分配全非结合Lambek演算($\mathsf{DFNL}$)的推广$\mathsf{S_{RBL}}$的形式化$\mathsf{L_{RBL}}$,并证明了它的割消和子公式性质.
2014-02-24 cs.LO math.LO
A unified relational semantics for BPL, IPL and OL -- axiomatization without disjunction
该研究提出一种统一的命题语言关系语义,整合直觉主义逻辑、BPL与OL的关系语义,在两类无析取语言下完成多框架条件组合的逻辑公理化,并提供到模态逻辑的翻译。
2024-12-12 math.LO
Explicit justification stit logic: a completeness result
我们认为,在早期的出版物中介绍的基本理由STIT逻辑的明确片段。我们定义了一个希尔伯特式的公理系统,这个逻辑,并表明,这个系统是强完整的相对于预期的语义。
2017-09-19 math.LO
The provably total recursive functions and the MRDP theorem in Basic Arithmetic and its extensions
我们学习了W.鲁滕伯格BA是建立在基本逻辑基础上的一种算术理论,它比直觉主义逻辑弱。证明了BA的可证全递归函数类是本原递归函数的真子类。本文研究了BA的三种扩张BA + U、BA_c和EBA与它们的可证全递归函数的关系。证明了BA的这三种扩张的可证全递归函数都是本原递归函数。此外,还证明了著名的MRDP定理在BA,BA + U,BA_c中不成立,而在EBA中成立.
2022-07-05 math.LO
The logic of vague categories
我们介绍了一个完整的多值语义的基本正规格为基础的模态逻辑。这种关系语义是基于形式概念分析的多值形式上下文。我们讨论的解释和可能的应用,这一逻辑框架的分类理论的形式分析多市场竞争。
2019-08-13 math.LO
Non normal logics: semantic analysis and proof theory
本文介绍了基本单调模态逻辑、条件逻辑CK及其公理化扩展的真显示演算。这些结石是健全的,完整的,保守的,并享有削减消除和子公式的财产。我们的建议适用于多类型的方法在显示演算的设计,从语义分析的基础上从单调模态逻辑到正常的双模态逻辑的翻译。
2019-03-12 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
Basic Logic and Quantum Computing: Logical Judgements by an Insider Observer
我们考虑一个假设的观察者在量子计算机内部的逻辑断言,并执行可逆的量子测量,获得一对对称的新公理,仅在量子计算机内部有效。结果是,在这个逻辑框架中,对称性和次协调性成立。
2004-07-07 math-ph math.LO math.MP
Interpolation in Hájek's Basic Logic
本文通过穷尽分类具有合并性质的 BL-代数簇与 basic hoop 簇,解决 Montagna 公开问题,并完整刻画 BL 及其无否定片段中具备演绎插值性质的公理化扩张。
2024-10-29 math.LO math.RA
An approach to basic set theory and logic
本文的目的是概述一套简单的公理基本集合论,从最基本的事实可以得出。整个项目的关键是一个新的集合论公理,我称之为“极值定律”。它允许快速证明基本的集合论恒等式和逻辑重言式,所以它也是一个很好的工具,以帮助一个人的记忆。我并不认为我通过公理接触过欧几里德几何。只需要有变换代数的恒等式的经验。这个想法是让学生从一开始就做证明。特别是,我避免让学生在早期就陷入逻辑的细微差别中,逻辑的基本事实是从集合论推导出来的,而不是相反。
2013-05-14 math.GN math.GT math.LO
Complexity of the interpretability logic IL
我们证明了可解释性逻辑IL的基本系统的判定问题是PSPACE完全的。为此,我们提出了一个算法,它使用多项式空间的复杂性,一个给定的公式。这样的算法的存在,连同先前已知的PSPACE硬度的封闭片段的IL,意味着PSPACE完全。
2018-04-06 math.LO
Deducibility of Identicals, Reflection Principle and Synthetic Connectives
本文证明了同一物可推导性条件与反射原理的等价性,并指出满足反射原理的连词仅是 Girard 的合成连词。
2026-01-28 math.LO
Logic Lectures: Gödel's Basic Logic Course at Notre Dame
一个编辑版本是给文本哥德尔的未发表的手稿的说明当然在基本逻辑,他发表在圣母大学于1939年。哥德尔的笔记处理什么是今天被认为是重要的逻辑问题出类拔萃,完整性,可判定性,独立性的公理,并与自然演绎太,这一切仍然是一个新奇的时候,当然是交付。对初学者充满敬意,笔记并不过分形式化。哥德尔大概只是为他自己打算的,它们充满了缩写。这与其他一些问题(如同一主题的两个版本,以及猜测页面的正确顺序)一起需要额外的努力才能获得可读的编辑版本。由于哥德尔提供的材料的质量,包括重要的哲学观点,这项努力应该是值得的。文本的编辑版本伴随着另一个版本,称为源版本,这是相当接近哥德尔的手稿。这是为了记录编辑过程中的编辑干预(特别是缩写是如何被删除的),并为后来的版本提供理由。
2017-06-16 math.HO math.LO
Basic Logic and Quantum Entanglement
众所周知,量子纠缠是量子计算最重要的特征之一,因为它导致大规模的量子并行性,从而使计算速度呈指数级提高。从某种意义上说,量子纠缠被认为是量子计算本身的一种隐含性质。但是...可否说得清楚一点?换句话说,是否有可能在机器语言的逻辑微积分中找到连接符“纠缠”?还有,有没有可能“教”量子计算机“模仿”EPR“悖论”?答案是肯定的,如果逻辑微积分是最弱的可能逻辑,即基本逻辑。弱逻辑几乎没有结构规则。但在逻辑中,弱结构为连接词留下了更多的空间(例如连接词“纠缠”)。此外,在基本逻辑中,压缩和弱化这两个结构规则的缺失分别对应于量子计算中的不可克隆定理和不可擦除定理的有效性。
2007-02-05 hep-th math.LO quant-ph
A Cut-free Sequent Calculus for Basic Intuitionistic Dynamic Topological Logic
针对$\textsf{iK}_d$和$\textsf{iK}_{d*}$这两个动态拓扑逻辑系统,本文提出无切割的G3风格相继式演算,补充了其证明论分析,并证明了析取性质、Visser规则推广及插值性质等关键结果。
2025-02-13 cs.LO math.LO
Turning the Liar paradox into a metatheorem of Basic logic
我们表明,自指可以形式化的基本逻辑的手段,通过新的连接词@,称为“纠缠”。事实上,连接词@的非恒等性是一个元定理,它说明一个自纠缠的句子失去了它自己的同一性。这就防止了在相应的元语言中出现自我指涉悖论。在这种情况下,我们引入了一个广义的自指定义,这是需要处理的乘法连接子结构逻辑。
2007-03-28 cs.LO math.LO quant-ph
Uniform Lyndon Interpolation for Basic Non-normal Modal and Conditional Logics
本文介绍了一种证明非正规模态逻辑和条件逻辑的一致Lyndon插值的证明理论方法,并证明了除了$\mathsf{CKID}$之外,逻辑$\mathsf{E}$、$\mathsf{M}$、$\mathsf{EN}$、$\mathsf{MN}$、$\mathsf{MC}$、$\mathsf{K}$及其条件形式$\mathsf{CE}$、$\mathsf{CM}$、$\mathsf{CEN}$、$\mathsf{CMN}$、$\mathsf{CMC}$、$\mathsf{CK}$也具有该性质.特别是,它意味着这些逻辑具有一致插值。虽然对他们中的一些人后者是已知的,事实上,他们有统一的林登插值是新的。此外,这些事实的证明理论证明是新的,以及明确计算它们提供的插值的建设性方法。在否定的一面,它表明,逻辑$\mathsf{CKCEM}$和$\mathsf{CKCEMID}$享有一致的插值,但不是均匀的林登插值。证明了非正规模态逻辑$\mathsf{EC}$和$\mathsf{ECN}$及其条件形式$\mathsf{CEC}$和$\mathsf{CECN}$不具有Craig插值,因而也不具有一致(Lyndon)插值.
2022-08-10 cs.LO math.LO
Weakly Aggregative Modal Logic: Characterization and Interpolation (new version)
Peking University(北京大学);UC Berkeley(加州大学伯克利分校)
弱聚合模态逻辑(WAML)是一组伪装的多元模态逻辑,它们的参数都是相同的。WAML在认知逻辑和博弈逻辑中有着有趣的应用,因此本文研究了WAML的一些基本模型理论问题。具体地说,我们基于互模拟的直观概念给出了WAML的vanBenthem-Rosen特征定理,并证明了每个基本WAML系统K_n都缺少Craig插值。
2019-05-30 cs.AI cs.LO math.LO
Refutation calculi for lattice-based logics: from display to tableaux
Vrije Universiteit Amsterdam(阿姆斯特丹自由大学);University of Johannesburg(约翰内斯堡大学);Scuola Normale Superiore di Pisa(比萨高等师范学院)
本文引入基本LE-逻辑的反驳显示演算,通过可推导矢列的分析证明其可靠性和完全性,并从中得到终止的表格演算。
2026-05-23 cs.LO math.LO
The Logic of Approximate Dependence
我们扩展处理的函数相关,依赖逻辑的基本概念,包括依赖的可能性与有限数量的例外。我们称之为近似依赖。本文的主要结果是近似依赖原子的完备性定理。我们指出了一些有问题的特点,这表明我们应该考虑多个团队,而不仅仅是团队。
2014-08-19 cs.LO math.LO