Disjunctions with stopping condition
我们介绍了一个工具,分析模型的$\textnormal{CT}^-$,组成的真理理论在皮亚诺算术。本文给出了Lachlan定理的一个新的证明,证明了$\textnormal{PA}$模型的算术部分是递归饱和的.我们使用这个工具来提供一个新的证明,所有模型的$\textnormal{CT}^-$进行部分归纳真谓词。最后,我们构造了一个部分真值谓词定义的公式从一个非标准的切割,不能扩展到一个完整的真值谓词满足$\textnormal{CT}^-$。
2020-10-15 math.LO
A self-contained theory of truth
塔斯基的不可定义性定理指出,基于传统谓词逻辑(PL)的形式系统不能谈论自己的真值谓词。然而,PL并不是唯一可以想象的形式语言。在本文中,它将被证明,它是可能的,以构建一个正式的系统,而不是PL的基础上,而是一个更严格的形式语言,这是自包含的意义上说,在这个系统中,我们可以谈论,甚至定义系统自己的真谓词。这暗示了理解罗素、哥德尔和塔斯基的发现的新方法,以及解决引起这些问题的恶性循环的新方法。这个新系统提出了一个有趣的替代基础数学框架。
2022-12-22 math.LO
Theories of truth for countable languages which conform to classical logic
每一个符合经典逻辑的可数语言都有一个符合经典逻辑的扩张,并有一个定义的真理论。如果客体语言的每一个句子都被它的意义评价为真或假,那么这种延伸就有一种语义学的真理论。这些理论包含真值谓词和非真值谓词。当客体语言的句子被它们的意义所评价时,理论是等价的。
2020-02-03 math.LO
Compositional truth with propositional tautologies and quantifier-free correctness
切维利斯基问是否组成的真理理论与额外的公理,所有命题重言式是真的是保守的皮亚诺算术。我们提供了一个部分的答案,这个问题,表明,如果我们另外假设,真理谓词同意算术真理的量词自由的句子,由此产生的理论是一样强大的$Δ_0$ -归纳的成分真理谓词,因此非保守。另一方面,可以用一个常规的论证来证明无量词正确性原则本身是保守的。
2020-11-13 math.LO
Universal properties of truth
本文研究了在子语言中可定义真理或满足谓词的模型的抽象模型论性质,分析了确保真理谓词可定义性的条件,并探讨了相关公理化理论及其相互可定义性关系。
2023-04-01 math.LO
On Classical Determinate Truth
本文提出了一种经典、无类型真理和确定性理论,结合了经典性和完全组合性,并展示了其与 Fujimoto 和 Halbach 理论的等价性及一些负面结果。
2025-07-24 math.LO
Effect of the Choice of Connectives on the Relation between the Logic of Constant Domains and Classical Predicate Logic
不仅经典语义学可以推广,直觉Kripke语义学也可以推广,从而可以处理任意由真假值表或真假值函数表征的命题连接词。在我们以前的工作中,已经证明了Kripke有效命题序列集和经典有效命题序列集重合当且仅当所有可用的命题连接词都是单调的。本文将这一结果推广到一阶逻辑,证明了在谓词逻辑中,所有可用的命题连接词都是单调的条件是在所有常数域Kripke模型中有效的序列集,而不是Kripke有效序列集和经典有效序列集重合的充要条件.
2021-07-08 math.LO
Predicate Exchangeability and Language Invariance in Pure Inductive Logic
在纯归纳逻辑中,谓词可交换性的理性原则指出,在给定语言L中置换谓词,并根据这个置换替换L-句子$ϕ$中谓词的每个出现,不应该改变我们对$ϕ$真理性的信念。本文研究了纯一元语言L上满足谓词可交换性的概率函数w何时也满足一元语言不变性原理。
2013-05-04 math.LO
The Concept of Truth
在对语言功能进行初步思考的基础上,给出了真值悖论的解决方案,并建立了相应的真值谓词语义。证明了它正是强Kleene三值语义的极大内在不动点的二值描述。
2021-05-28 math.LO
Generalizations of Mezhirov's game semantics to predicate superintuitionistic logics and the Casari formula
本文将Mezhirov提出的命题直觉主义逻辑博弈语义推广至谓词直觉主义逻辑及其扩展,并建立博弈与无限公式集推导之间的联系。
2023-10-24 math.LO
Predicate and Set Bundles in Multi-valued Logic
本文提出基于谓词丛的多值逻辑新模型,定义相关真值度与运算,研究集合丛并解决模态逻辑的必然性/可能性问题及连锁悖论。
2026-08-13 math.LO
What Kinds of Connectives Cause the Difference between Intuitionistic Predicate Logic and the Logic of Constant Domains?
直觉Kripke语义可以推广到任意命题连接词的真假值函数。我们将这种广义Kripke语义推广到一阶逻辑,并研究了连接词的选择如何改变直觉谓词逻辑和常域逻辑之间在序列有效性方面的关系。我们的主要结果给出了直觉谓词逻辑中的有效序列集与常域逻辑中的有效序列集重合的一个简单的充要条件。
2022-05-12 math.LO
A Completeness Proof for A Regular Predicate Logic with Undefined Truth Value
我们提供了一个健全的和完整的证明系统Kleene的三元逻辑谓词的扩展。理论的概念是扩展的,对于每个函数符号,一个公式,指定何时定义的功能。“被定义”的概念通过一个简单的递归算法扩展到术语和公式。“已定义”公式的构造使得它们本身总是已定义的。完整性证明依赖于Henkin构造。对于每一个公式,公式、它的否定和它的“被定义”公式的否定之一在构造的模型上是真的。许多其他三进制逻辑在文献中可以减少到我们的。部分函数在计算机科学中无处不在,甚至在学校的方程求解中也是如此。我们的工作的动机是试图解释,正是在逻辑方面,典型的非正式方法的推理,在这样的应用。
2023-03-26 cs.LO math.LO
The two halves of disjunctive correctness
Ali Enayat曾问过,组合真值谓词的选言正确性(DC)的两个半部分是否比皮亚诺算术保守。在本文中,我们证明了“每个真析取有一个真析取”原则等价于合成真谓词的有界归纳,因此它不是保守的。另一方面,逆蕴涵“任何具有真析取的析取都是真的”可以保守地添加到PA。这里介绍的方法使我们能够直接证明DC的非保守性。
2021-08-31 math.LO
Arboles de Forzamiento Semántico para la Logica de Predicados
本文提出语义强制树作为一阶谓词逻辑的视觉推理工具,其有效性与赋值语义一致,无效公式可由叶标记构造反驳模型。
2024-08-21 math.LO
Positive, Negative, and Reliable Information in a First-Order Logic of Evidence and Truth
University of Campinas (UNICAMP)(坎皮纳斯大学);Federal University of Minas Gerais (UFMG)(米纳斯吉拉斯联邦大学)
本文提出第一阶逻辑QLETF+,展示其满足替换性质并支持连结、否定和预置范式,通过o扩展定义谓词满足条件,证明其在六值一阶语义下的完备性。
2026-04-20 math.LO
Modal logics of conjunctively closed provability predicates
Graduate School of System Informatics, Kobe University(神户大学系统信息研究生院)
研究与满足特定可推导性条件的可证性谓词对应的非正规模态逻辑,引入基于闭包算子的新语义,证明了多个非正规模态逻辑的模态完全性及一些逻辑的算术完全性定理。
2026-07-10 math.LO
The algebraic semantics for the one-variable monadic fragment of the predicate logic $\mathcal{G}\forall_{\sim}$
本文研究一阶逻辑 $\mathcal{G}\forall_{\sim}$ 单变量一元片段的等价代数语义,通过引入并分析配备一元算子和 De Morgan 否定的 Gödel 代数簇,证明其特殊子簇即为所需的等价代数语义。
2024-11-17 math.LO
Decidability of predicate logics with team semantics
我们研究了基于团队语义的谓词逻辑的复杂性。证明了二元独立逻辑和二元包含逻辑的可满足性问题都是NEXPTIME-完全的。此外,我们表明,两个变量的依赖逻辑的有效性问题是不可判定的,从而解决了一个开放的问题,从团队语义文献。我们还简要地分析了依赖逻辑的Bernays-Schönfinkel-Ramsey前缀类的复杂性。
2016-06-18 cs.CC cs.LO math.LO
The provability logic of all provability predicates
本文证明所有可证性谓词的可证性逻辑恰为纯必然化逻辑N,并引入其三个扩展N4、NR和NR4,分别刻画满足特定条件的各类可证性谓词,研究其算术语义。
2023-09-01 math.LO
The Modal Logics of Kripke-Feferman Truth
我们通过Solovay式完备性结果确定了Solomon Feferman的不动点真值模型的模态逻辑及其公理化。给定一个不动点模型$\mathcal{M}$或其公理化$S$,我们找到一个模态逻辑$M$,使得模态语句$φ$是$M$的一个定理当且仅当通过用真值谓词翻译模态算子得到的语句$φ^*$在$\mathcal{M}$中为真,或在所有这样的翻译下都是$S$的一个定理。为此,我们引入了一个新版本的可能世界的语义,具有经典和非经典的世界,并建立了一个家庭的非全等模态逻辑,其内部逻辑是亚经典的这种语义的完整性。
2020-05-06 math.LO
Unlocking of predicate: application to non-anticipating selections
Krasovskii Institute of Mathematics and Mechanics, UB RAS(克拉索夫斯基数学力学研究所,俄罗斯科学院乌拉尔分院);Ural Federal University named after B.N. Yeltsin(以B.N.叶利钦命名的乌拉尔联邦大学)
本文提出谓词解锁方法,用于构建多值映射的非前瞻性选择,通过固定点搜索解决谓词真值集问题,展示了两种解锁映射的构造及最大非前瞻性选择的表达。
2017-03-29 cs.SY eess.SY math.LO
Internal Reasoning and Consistency in Reflective Grounded Arithmetic
EPFL(洛桑联邦理工学院)
本文在Isabelle/HOL中开发了经机器验证的RGA系统,定义了其内在真谓词,完成相关元定理闭合,证明RGA是支持非平凡数学推理的可行形式系统。
2026-10-27 cs.LO cs.PL math.LO
Asymptotic truth-value laws in many-valued logics
University of Queensland(昆士兰大学);Universidad de los Andes(安第斯大学);University of Siena(锡耶纳大学)
本文研究多值逻辑中句子在有限模型中渐近真值的分布规律,推广了Fagin定律,并探讨了PSPACE完全性及真值集合的描述问题。
2023-09-19 math.LO
Truth-value semantics and functional extensions for classical logic of partial terms based on equality
我们开发了一个自下而上的方法,真假值语义的经典逻辑的部分条款的基础上平等和应用它来证明的保守性,除了部分描述和部分选择功能,独立于任何严格的假设。
2012-12-01 math.LO
An interpolant in predicate Gödel logic
一个逻辑满足插值性质,只要一个公式Δ是另一个公式Γ的推论,那么这由一个公式Θ证明,该公式θ只涉及Γ和Δ共有的语言。也就是说,出现在Θ中的关系(和函数)符号出现在Γ和Δ中,Γ具有Θ作为结果,并且Θ具有Δ作为结果。经典谓词逻辑和直觉谓词逻辑都具有插值性质,但中间谓词逻辑如何具有插值性质是一个长期悬而未决的问题,2013年Mints,Olkhovikov和Urquhart证明了常数域直觉主义逻辑不具有插值性质,而谓词哥德尔逻辑是否具有插值性质则是一个悬而未决的问题。在这篇短文中,我们证明了他们关于常域直觉主义逻辑的反例在谓词哥德尔逻辑中确实允许内插。虽然这对解决谓词哥德尔逻辑的问题没有影响,但它使人们相信它确实满足插值。此外,我们的方法是基于Olkhovikov的语义工具的分析,我们希望这可能最终有助于解决这个问题。
2019-02-12 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
Binary Kripke Semantics for a Strong Logic for Naive Truth
我表明,逻辑$\textsf{TJK}^{d+}$,目前已知的最强的逻辑之一,以支持天真的真理理论,是从克里普克语义常数域直觉主义逻辑(一)下降的要求,可访问性关系是自反的和(二)只允许自反世界作为反例逻辑后果。此外,我还为$\textsf{TJK}^{d+}$提供了一个简化的自然演绎系统,其中使用条件证明的限制形式来建立条件。
2020-12-01 math.LO
Categorical semantics of metric spaces and continuous logic
使用范畴的度量空间作为模板,我们开发了一个度量模拟的范畴语义的经典/直觉主义逻辑,并表明,自然概念的谓词在这个“连续语义”是等价的一个先验的单独概念的谓词在连续逻辑,这是独立的模型理论家研究,并发现各种应用。我们通过把度量空间范畴中的实区间[0,1]表示为一个“连续子对象分类器”来证明这一等价性,它不仅给出了两个谓词概念之间的对应关系,而且给出了连续语义中的自然量化概念与连续逻辑中已有的量化概念之间的对应关系。一路上,我们制定了它的意思是一个给定的范畴表现得像度量空间的范畴,然后表明,任何这样的类别支持上述连续语义。作为一个应用,我们表明,范畴的预层的度量空间的例子,事实上,甚至拥有连续的子对象分类。
2019-01-25 math.CT math.LO
Valuation semantics for first-order logics of evidence and truth (and some related logics)
本文介绍了逻辑$QLET_{F}$,证据和真理逻辑$LET_{F}$的量化扩展,以及相应的声音和完整的一阶非确定性赋值语义。$LET_{F}$是一个次协调和次完全的逻辑,它用一个经典算子${\circ}$和一个非经典算子$\bullet$扩展了一级蕴涵逻辑($FDE$),它们彼此对偶:当${\circ} A$要求$A$行为经典时,${\bullet} A$从$A$违反一些经典有效的推论中得出。$QLET_{F}$的语义结合了解释否定谓词的反扩展与一阶非确定性赋值的结构,并通过Henkin方法的推广获得完整性。通过为$FDE$,$K3$和$LP$的一阶扩展提供健全和完整的语义,我们展示了这些工具,我们在这里称之为“反扩展+赋值”的方法,可以自然地应用于一些非经典逻辑。
2021-06-18 math.LO
Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter
本文证明了一阶直觉逻辑的正片段在具有两个变量和一个一元谓词字母的语言中是不可判定的,没有常数和等式。无论我们考虑的是扩展域还是常量域的语义,这都是正确的。然后,我们将这一结果推广到区间[QBL,QKC]和[QBL,QFL],其中QKC是弱排中律的逻辑和QBL和QFL是一阶对应的维塞尔的基本和形式逻辑,分别。我们还表明,对于大多数“自然”的一阶模态逻辑,两个变量片段与一个单一的一元谓词字母,没有常数和平等,是不可判定的,无论我们是否考虑语义与扩展或常数域。这些包括QKTB、QGL和QGrz的所有子逻辑,其中包括QK、QT、QKB、QD、QK4和QS4。
2022-06-12 cs.LO math.LO
Model Theory of Monadic Predicate Logic with the Infinity Quantifier
本文建立了模型理论性质的$\mathrm{FOE}^{\infty}$,一元一阶逻辑的变化,具有广义量词$\exists^\infty$(“有无限多”)。我们提供了语法定义的片段$\mathrm{FOE}^{\infty}$表征四个不同的语义属性的$\mathrm{FOE}^{\infty}$ -句子:(1)是单调的和(2)(斯科特)连续在一个给定的一元谓词集;(3)有真理下保持采取子模型或(4)不变量下采取继承。在每一种情况下,我们产生一个有效定义的映射,将任意句子$φ$翻译成属于相应句法片段的句子$φ^{p}$,其属性是$φ$等同于$φ^{p}$,当它具有相关的语义属性时。我们的方法是首先提供这些结果在更简单的设置一元一阶逻辑($\mathrm{FOE}$)和($\mathrm{FO}$)的平等,然后移动到$\mathrm{FOE}^{\infty}$包括广义量词$\exists^\infty$到图片。作为我们的推论,我们得到了上述四个语义性质对于$\mathrm{FOE}^{\infty}$ -语句是可判定的。此外,我们的结果是直接相关的自动机和表达模bisimilirity的一元二阶逻辑的变种的特征。该应用程序是在一个配套文件中开发的。
2018-09-10 cs.LO math.LO
Simulations and Bisimulations For Coalgebraic Modal Logics
我们定义了一个概念的Lambda模拟的共代数模态逻辑,参数的选择Lambda的谓词提升函子T。我们证明了这个概念在几个方面是足够的:i)它保留了正公式的真值,ii)对于Lambda,单调谓词提升的分离集,Lambda-互模拟的相关概念对应于T-行为等价(此外Lambda-n-互模拟对应于T-n-行为等价),以及iii)事实上,对于Lambda-分离和T保持弱回调,双功能Lambda-互模拟是T-互模拟。从本质上讲,我们得到了一个模块化的等价概念,当与一组单独的单调谓词提升一起使用时,与T-行为等价一致,而不管T是否保留弱回调(与T-双相似性的概念不同)。
2013-04-11 cs.LO math.LO
Recursive enumerability and elementary frame definability in predicate modal logic
研究了一阶谓词模态逻辑中递归可枚举性与基本框架可定义性之间的关系。一方面,众所周知,每个一阶谓词模态逻辑关于Kripke框架的基本类完备,即,一类可由经典一阶公式定义的框架是递归可递归的。另一方面,基于本质上具有二阶Kripke语义的“自然”命题模态逻辑的谓词模态逻辑的许多例子是已知的,它们要么不是递归可排数的,要么是Kripke不完全的。这就提出了一个问题,即是否每一个Kripke完备的、递归可判定的谓词模态逻辑都可以用一个Kripke框架的基本类来刻画。我们回答这个问题的否定,通过构建一个正常的谓词模态逻辑,这是Kripke完全的,递归可重复的,但不完全的一个基本类的框架。我们还提出了一个正常的谓词模态逻辑的例子,是递归可重复的,Kripke完全的,不完全的一个基本类的根框架,但相对于一个基本类的框架,没有根是完整的。
2019-12-20 cs.LO math.LO
Intuitionistic Existential Instantiation and Epsilon Symbol
本文给出了一个具有存在\实例化规则的直觉谓词逻辑的自然演绎系统,它使用了Hilbert的$\e$ -符号.它相对于直觉谓词逻辑是保守的。我们提供了一个合适的Kripke语义的完整性证明,勾勒出一个正规化证明的方法,调查相关的工作和状态一些开放的问题。我们的系统扩展了直觉系统,由于A. Dragalin和Sh.前原
2012-08-03 cs.LO math.LO
Categorical and Algebraic Aspects of the Intuitionistic Modal Logic $\operatorname{IEL}^{-}$ and its predicate extensions
直觉模态逻辑系统${\bf IEL}^{-}$是S. Artemov和T. Protopescu作为信念逻辑\cite{Artemov}的直觉主义版本。我们构造的模态lambda演算是Curry-Howard同构的${\bf IEL}^{-}$作为应用计算的类型理论表示广泛的功能性编程。我们还提供了一个范畴的解释,这模态lambda演算考虑coalgebras与一个monoidal函子上的一个carbohydrate闭范畴。最后,我们研究了Heyting代数和具有相应算子的locale。这种运算符也用于无点拓扑中。我们使用Goldblatt \cite{goldblatt2011cover}引入的Dedekind-MacNeille完备化和模态覆盖系统研究${\bf IEL}^{-}$及其相关逻辑的谓词扩展的完全Kripke-Joyal风格语义。本文扩展了发表在LFCS'20卷\cite{rogozin2020modal}的会议论文。
2020-12-07 math.CT math.LO
Towards a Formal Distributional Semantics: Simulating Logical Calculi with Tensors
University of Oxford(牛津大学)
语义的组合分布模型的发展调和了分布语义的经验方面与形式语义的组合方面,是当代文献中的一个热门话题。本文旨在通过展示如何使用组合分布模型中常用的数学结构(如张量和矩阵)来模拟谓词逻辑的不同方面,进一步实现这种和解。本文讨论了如何利用张量和多线性映射之间的规范同构来模拟一个成熟的无量词谓词演算使用张量。它提供了一组逻辑连接词的张量解释,这些逻辑连接词是建模命题演算所必需的。它提出了这些张量演算的一个变体,能够使用很少的非线性运算来模拟量词。最后讨论了这些变体之间的关系,以及这种关系如何构成未来工作的主题。
2013-04-28 cs.CL cs.LO math.LO
Notes on neighborhood semantics for logics of unknown truths and false beliefs
School of Humanities, University of Chinese Academy of Sciences(中国科学院大学人文学院)
在这篇文章中,我们研究了在邻域语义下的未知真和假信念逻辑。我们比较了这两种逻辑的相对表现力。事实证明,它们在不同类别的邻域模型上是不可比较的,并且这两种逻辑的组合在任何类别的邻域模型上都具有标准模态逻辑的表达能力。我们为每一个逻辑提出了态射,它可以帮助我们探索框架可定义性问题,给出一个一般的可靠性和完备性结果,并推广了文献中的一些结果。我们公理化的两个逻辑在不同类别的邻域框架。最后,我们将结果推广到公告的情形,这对Moore判决和其他一些判决有很好的应用。
2020-02-22 cs.AI math.LO
Truth and Preferences -- A Game Approach for Qualitative Choice Logic
TU Wien(维也纳工业大学);Institute of Logic and Computation(逻辑与计算研究所)
在本文中,我们介绍了博弈论语义(GTS)的定性选择逻辑(QCL),为了表达偏好,扩展了经典的命题逻辑与一个额外的连接称为有序析取。首先,我们证明了游戏语义可以捕获现有的程度为基础的语义QCL在一个自然的方式。其次,我们表明,游戏语义可以利用QCL的语言派生新的语义。特别是,我们提出了一个新的语义,利用GTS否定,并通过这样做,避免在现有的QCL语义否定的问题。
2022-09-27 cs.AI cs.LO math.LO