Logics of Intuitionistic Kripke-Platek Set Theory
Rosalie Iemhoff, Robert Passmann
研究了直觉Kripke-Platek集合论IKP的逻辑结构，证明了IKP的一阶逻辑是直觉一阶逻辑IQC。
We investigate the logical structure of intuitionistic Kripke-Platek set theory IKP, and show that the first-order logic of IKP is intuitionistic first-order logic IQC.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Kreisel-Lévy-type theorems for Kripke-Platek and other set theories
我们证明了，在Kripke-Platek集合论与无穷（KP），超穷归纳法沿序数$ε_{Ω+1}$是等价的模式断言的可靠性KP，其中$Ω$表示的上确界的所有序数在宇宙中，这是类似的结果，在皮亚诺算术（PA），超穷归纳法沿$ε_0$是等价的模式断言的可靠性PA。在证明中，我们需要在KP中编码无穷证明，这是通过使用部分递归集函数来完成的。这个结果可以推广到KP + $Γ$ -分离+ $Γ$ -收集，其中$Γ$是任何给定的语法复杂度，但不能推广到ZF。
On a slight weakening of Kripke-Platek Set Theory
该研究将克里普克-普拉特集合论（$\textsf{KP}$）弱化得到$\textsf{ReR}$，证明$\textsf{ReR}$可证$\textsf{TCo}$，并构建模型说明$\textsf{TCo}$不成立以论证证明依赖类基础片段的必要性。
Realisability for Infinitary Intuitionistic Set Theory
我们介绍了一个基于有序图灵机（OTM）的无穷直觉集合论的可实现性语义。我们表明，我们的OTM-可实现性的概念是健全的某些系统的无穷直觉主义逻辑，并实现了所有公理的无穷Kripke-Platek集合论。最后，我们使用我们的可实现性概念的一个变体来证明（有限）直觉Kripke-Platek集合论的命题容许规则正是直觉命题逻辑的容许规则。
Power Kripke-Platek set theory and the axiom of choice
虽然幂次Kripke-Platek集合论（KPP）与普通Kripke-Platek集合论（KP）有许多相同的性质，但在几个方面它的行为与KP完全不同。这也许是最引人注目的证明结果，由于马蒂亚斯，大意是增加公理的可构造性KPP产生了一个更强的理论，而在KP的情况下，可构造的层次提供了一个内部模型，使KP和KP+V=L具有相同的强度。本文将讨论KPP和KPP加上选择公理甚至全局选择公理GAC之间的关系。由于L是提供一个模型的标准工具，在这个模型中，这个公理成立，通常的论点，证明增加AC或GAC的KPP不增加证明理论的强度不适用于任何明显的方式。在其他工具中，本文使用了序数分析的技术来表明KPP+GAC与KPP具有相同的强度，从而回答了Mathias的问题。此外，它表明，KPP+GAC是保守的KPP的Pi-1-4的分析报表。理论的序分析方法与幂集是在早期的论文中发展起来的。该技术允许人们从无穷证明中计算见证信息，为理论中可证明的幂集运算的超限迭代提供边界。由于KPP+GAC理论为定义其他理论的模型和可实现性模型提供了非常有用的工具，这些模型在没有统一选择机制的情况下很难构建，因此需要确定其确切的证明理论强度。这方面的知识，例如可以用来确定的力量费弗曼的操作集合论与幂集的运作，以及建设性的泽梅罗-弗兰克尔集合论与选择公理。
Ordinal analysis of intuitionistic power and exponentiation Kripke Platek set theory
直到20世纪70年代，证明理论的研究主要涉及归纳定义，分析子系统和有限型系统的理论。随着Gerhard Jaeger在20世纪70年代末和80年代初的开创性工作，焦点转向了集合论，为普通理论证明论提供了一个统一而优雅的框架。最近的研究表明，这些工具有时甚至可以适用于强公理，如幂集公理，其中一个没有达到完全削减消除，但仍然可以提取见证信息和表征的强度理论的累积层次的可证明的高度。在这里，这种技术被应用到直观的Kripke-Platek集合论IKP（P）和IKP（E），其中幂集和幂运算分别被允许作为分离和集合模式中的原语。特别地，IKP（P）证明了幂集公理，而IKP（E）证明了指数公理。后者表示给定任何集合A和B，从A到B的所有函数的集合也是一个集合。虽然IKP（P）可以用与其经典表亲类似的方法治疗，但IKP（E）的治疗存在相当大的障碍。其中之一是，在无限系统中，术语的层次成为一个移动的目标，因为它们不能被分配一个固定的水平，在正式的累积层次结构的基础上，他们的句法结构。正如在前面的文章中所述，本文的结果是一个重要的工具，表明了几个具有集合公理的直觉集合论具有存在性，即，如果他们证明了存在定理，那么见证者可以在理论中被可证明地描述，一个例子是具有有界分离的直觉主义的Zermelo-Fraenkel集合论。
IKP and Friends
发展了直觉主义Kripke-Platek集合论的基本理论，并利用Kripke模型证明了相关经典等价理论之间的一些独立性结果。
Generalized Kripke's Schema and the Expressive Power of Intuitionistic Real Algebra
本文引入相对化的随机Kripke模式，通过在其中解释二阶Heyting算术，展示了该方法在研究直觉主义实代数表达力中的应用。
Supervaluations, truth, and intuitionistic logic
本文提出了一种基于超估值方法的直觉逻辑固定点真理理论，并展示了其在Kripke结构上的应用及与经典逻辑的对比。
What Kinds of Connectives Cause the Difference between Intuitionistic Predicate Logic and the Logic of Constant Domains?
直觉Kripke语义可以推广到任意命题连接词的真假值函数。我们将这种广义Kripke语义推广到一阶逻辑，并研究了连接词的选择如何改变直觉谓词逻辑和常域逻辑之间在序列有效性方面的关系。我们的主要结果给出了直觉谓词逻辑中的有效序列集与常域逻辑中的有效序列集重合的一个简单的充要条件。
Encoding Sequences in Intuitionistic Real Algebra
本文展示了在直觉实数代数中如何通过随机Kripke方案递归编码序列。
Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic
在他们的开创性论文中，阿特莫夫和Protopescu提供了希尔伯特形式系统，Brower-Heyting-Kolmogorov和Kripke语义的直觉信念和知识的逻辑。随后Krupski证明了直觉知识的逻辑是PSPACE完全的，Su和Sano提供了享有子公式属性的演算。本文通过提供具有子公式性质且终止于线性深度的隐式演算，继续了对直觉主义认知逻辑隐式演算的研究。我们的演算允许我们设计一个过程，对于无效的公式，返回一个最小深度的Kripke模型。最后我们还讨论了反驳的反演算，即证明无效性的反演算。
Cut-elimination for $ω_{1}$
本文利用无穷公理和无穷集公理，在“存在不可数正则序数”的假设下，用序数的存在性来标定Kripke-Platek集合论的可靠性强度.
Decidability of quantified propositional intuitionistic logic and S4 on trees
量化命题直觉主义逻辑是由命题直觉主义逻辑通过在命题上添加量词\forall p，\exists p而得到的.在Kripke语义学的上下文中，一个命题是一个向上封闭的模型结构中世界的子集。Kremer（1997）证明了基于所有偏序类的量化命题直觉主义逻辑Hπ+与完全二阶逻辑递归同构。他提出了一个问题，即从限制到树的逻辑是否是可公理化的。事实证明，它是可判定的。所使用的方法也可以用来建立模态S4的可判定性与类似类型的Kripke结构的命题量化。
Classifying the provably total set functions of KP and KP(P)
本文对Kripke-Platek集合论KP和Power Kripke-Platek集合论KP（P）的可证全集函数进行分类，并证明了几个（部分）保守性结果。本文中使用的主要技术工具是相对化技术，其中相对于任意但固定的集合x进行序数分析。序分析的一个经典结果是皮亚诺算术PA的可证递归函数的特征化，通过快速增长的层次[10]。虽然KP中的自然数是可以公式化的，但该理论主要讨论的是集合。由于这个原因，它是可取的，以获得其可证明的总集函数的特性。我们将证明，KP证明了一个集函数的整体性，正是当它属于一个层次结构的集函数的基础上延伸到任何序数以下的巴赫曼-霍华德序数的长度相对化的可构造层次结构。作为这个结果的结果，我们得到IKP +对所有x，y（x在y中或x不在y中）是保守的KP对所有存在公式，其中IKP代表直觉Kripke-Platek集合论。在类似的脉络中，利用[56]，它表明，KP（P）证明了一个集函数的整体，当它属于一个层次的集函数的基础上相对化冯诺依曼层次的相同长度。应用于KP（P）的相对化技术与全局选择选择公理AC-全局，也得到了[58]中结果的参数化扩展，表明KP（P）+AC-全局在幂集陈述中对Pi_2的KP（P）+ AC和CZF + AC是保守的。这里AC代表普通的选择公理，CZF指的是构造性的策梅洛-弗兰克尔集合论。
Hennessy-Milner Properties via Topological Compactness
本文给出了直觉Kripke模型下的直觉逻辑、对偶直觉逻辑和双直觉逻辑的Hennessy-Milner类，并将这些结果推广到模态（对偶和双）直觉主义逻辑.我们的主要技术工具是图像紧凑和预图像紧凑的关系，提供了一个语义描述的模态饱和度属性。
Localizing Finite-Depth Kripke Models
我们可以将一阶（或命题）直觉Kripke模型看作是经典模型的有序集合。在本文中，我们表明，有限深度的Kripke模型在任意一阶语言或命题语言，本地（经典）真理的公式是等价的非经典真理（真理的Kripke语义）的弗里德曼翻译的公式，即$ α\Vdash A^ρ\Leftrightarrow \mathfrak{M}_α\models A$。我们介绍这个事实的一些应用。推广了[Ardeshir and Hessam 2002]的结果，证明了Heyting算术$ {\sf HA} $的半窄Kripke模型是局部的$ {\sf PA} $ .
Kripke-like models of Set Theory in Modal Residuated Logic
本文借助Ono–Komori剩余Kripke模型推广Fitting的直觉主义集合论语义，构建模态剩余逻辑中的von Neumann层级，建立与Heyting值模型的公式翻译，并提出可构造集全域概念。
Binary Kripke Semantics for a Strong Logic for Naive Truth
我表明，逻辑$\textsf{TJK}^{d+}$，目前已知的最强的逻辑之一，以支持天真的真理理论，是从克里普克语义常数域直觉主义逻辑（一）下降的要求，可访问性关系是自反的和（二）只允许自反世界作为反例逻辑后果。此外，我还为$\textsf{TJK}^{d+}$提供了一个简化的自然演绎系统，其中使用条件证明的限制形式来建立条件。
Intuitionistic logic, dual intuitionistic logic, and modality
本文通过余海廷代数与拓扑空间的关系研究对偶直觉主义逻辑的语义，并证明其与直觉主义逻辑通过Kripke语义共同关联于模态逻辑S4。
Constructing the Constructible Universe Constructively
本文在直觉主义集合论中扩展生成 L 的基本运算，并证明 CZF（即使含幂集公理）也不能证明指数公理在 L 中成立，从而揭示 L 未必是传统内模型。
Carnap's problem for intuitionistic propositional logic
我们表明，直觉命题逻辑是\emph{Carnap categorical}：唯一的解释与直觉后果关系一致的连接词是标准的解释。这相对于最著名的语义学而言是成立的，直觉主义逻辑在这些语义学中是健全的和完备的;其中包括克里普克语义学、贝斯语义学、德拉加林语义学和拓扑语义学。它也适用于代数语义，尽管在这种情况下的范畴性与相对于可能世界样式语义的范畴性在种类上不同。
Kripke Semantics for Fuzzy Logics
克里普克框架（和模型）为次经典逻辑提供了合适的语义，例如直觉主义逻辑（布劳威尔和海廷）将自反和传递克里普克框架（具有持久满意关系）公理化，而基本逻辑（维瑟）将传递克里普克框架（具有持久满意关系）公理化。在这里，我们调查Kripke框架/模型是否可以提供一个语义模糊逻辑。对于基本模糊逻辑的每一个公理，寻找满足它们的Kripke框架/模型的充要条件。事实证明，唯一的模糊逻辑（包含基本模糊逻辑的逻辑），这是健全的和完整的关于一类克里普克框架/模型是哥德尔逻辑（或超直觉主义逻辑的达米特）的扩展，事实上，这种逻辑是健全的和强完整的关于自反，传递和连接（线性）克里普克框架（与持久的满意关系）。这为（命题）模糊逻辑中的哥德尔逻辑提供了一个语义特征。
Expressive power of basic modal intuitionistic logic as a fragment of classical FOL
本文讨论了模态直觉主义逻辑的Kripke式语义的四种不同版本所导出的一阶逻辑片断。为了捕捉这些片段，asimulation的概念进行了修改和扩展，以产生Van Benthem类型的语义表征各自的表达能力。它示出，进一步，这种特征可以很容易地进行到任意一阶可定义的子类的经典一阶模型。
Admissible extensions of subtheories of second order arithmetic
本文研究逆数学中若干理论的可容许扩张，即在满足原理论公理的自然数结构之上，叠加受KP公理支配的超限层次集合论世界。
Generalizations of Mezhirov's game semantics to predicate superintuitionistic logics and the Casari formula
本文将Mezhirov提出的命题直觉主义逻辑博弈语义推广至谓词直觉主义逻辑及其扩展，并建立博弈与无限公式集推导之间的联系。
An intuitionistically complete system of basic intuitionistic conditional logic
本文提出基本直觉主义条件逻辑IntCK，证明其相对克里普克模型和一阶直觉主义逻辑翻译的完备性，并分析其与CK、IK及Weiss的ICK的关系，讨论候选系统的优劣。
From Intuitionism to Many-Valued Logics through Kripke Models
直觉命题逻辑是由Kurt Gödel（1932）证明的无限多值逻辑，它是由Stanismartaw Jaumkowski（1936）证明的可数多值逻辑。在本文中，我们使用Saul Kripke（1959）的模型为这些定理提供了另一种证明。哥德尔的证明产生了一个中间命题逻辑（介于直觉主义和经典之间），现在被称为哥德尔或哥德尔-达米特逻辑，也被模糊逻辑学家研究。我们还提供了一些结果，在此逻辑命题连接词的可定义性。
Intuitionistic Existential Instantiation and Epsilon Symbol
本文给出了一个具有存在\实例化规则的直觉谓词逻辑的自然演绎系统，它使用了Hilbert的$\e$ -符号.它相对于直觉谓词逻辑是保守的。我们提供了一个合适的Kripke语义的完整性证明，勾勒出一个正规化证明的方法，调查相关的工作和状态一些开放的问题。我们的系统扩展了直觉系统，由于A. Dragalin和Sh.前原
Completeness and interpolation for intuitionistic infinitary predicate logic, in connection to finitizing the class of representable Heyting polyadic algebras
研究了Heyting多进代数的各种约简的表示定理。超合并证明了几个（自然约简）和我们的结果进行了比较，在经典代数逻辑处理圆柱和polyadic（布尔代数）的有限性问题。我们还证明了几个新的整齐嵌入定理，并得到了基于（广义）Kripke语义的可表示代数类与具有整齐嵌入性质的代数类，即那些代数是具有$ω$额外维数的代数的次整齐约化.
Propositional Mixed Logic: Its Syntax and Semantics
在本文中，我们提出了一个命题逻辑（称为混合逻辑）包含不相交的副本的最小，直觉和经典逻辑。我们证明了这个逻辑的Kripke语义的完备性定理。建立了混合逻辑与极小逻辑、直觉逻辑和经典逻辑之间的关系。最后，我们提出了这个逻辑的微积分版本。
Projectivity meets Uniform Post-Interpolant: Classical and Intuitionistic Logic
本文研究经典与直觉主义命题逻辑中投射性与一致后插值的关系，证明经典逻辑中二者对所有公式等价，并给出直觉主义逻辑的Kripke语义刻画，进而证明某些直觉主义逻辑扩张的统一类型是有穷的。
A complete axiomatization of infinitary first-order intuitionistic logic over $\mathcal{L}_{κ^+, κ}$
给定一个弱紧基数$κ$，给出了$\mathcal{L}_{κ^+, κ}$上直觉一阶逻辑的公理化，并证明了它对于Kripke模型是可靠的和完备的.因此，我们得到了该逻辑的析取和存在性质。这推广了Nadel关于$\mathcal{L}_{ω_1, ω}$上的直觉主义逻辑的工作。当$κ$是一个正则基数使得$κ^{<κ}=κ$时，我们通过一个简单的证明修改，推导出$\mathcal{L}_{κ^+, κ, κ}$上的直觉一阶逻辑的一个完全公理化，该语言具有至多$κ$公式的析取，小于$κ$公式的合取和小于$κ$许多变量的量化.特别地，这适用于广义连续统假设下的任何正则基数。
First-Order Intuitionistic Logic with Decidable Propositional Atoms
用可判定命题原子扩展的直觉主义逻辑结合了命题部分的经典性质和不含命题符号的可导公式的直觉性质。序贯演算是用来作为一个框架，调查这个扩展。削减的可接受性被保留。引入了约束Kripke结构，用于对具有可判定命题原子的直觉主义逻辑进行建模.研究了分离性和存在性的程度。关于这项研究的最新信息可以在http://sakharov.net/median.html上找到。
Effect of the Choice of Connectives on the Relation between the Logic of Constant Domains and Classical Predicate Logic
不仅经典语义学可以推广，直觉Kripke语义学也可以推广，从而可以处理任意由真假值表或真假值函数表征的命题连接词。在我们以前的工作中，已经证明了Kripke有效命题序列集和经典有效命题序列集重合当且仅当所有可用的命题连接词都是单调的。本文将这一结果推广到一阶逻辑，证明了在谓词逻辑中，所有可用的命题连接词都是单调的条件是在所有常数域Kripke模型中有效的序列集，而不是Kripke有效序列集和经典有效序列集重合的充要条件.
Proof Theory for Intuitionistic Strong Löb Logic
本文介绍了两种直觉强Löb逻辑的终结演算${\sf iSL}_\Box$：一种是基于直觉命题逻辑${\sf IPC}$的终结演算${\sf G4ip}$的终结演算${\sf G4iSL}_\Box$，另一种是标准无割演算${\sf G3ip}$的无结构规则的扩展${\sf G3iSL}_\Box$.主要结果之一是${\sf G3iSL}_\Box$的割消定理的句法证明。此外，还建立了${\sf iSL}_\Box$的微积分与Hilbert系统之间的等价关系.从文献中可知，${\sf iSL}_\Box$对于一类直觉模态Kripke模型是完备的，其中模态关系是传递的，相反是良基的，并且是直觉关系的子集.在这里，这一事实的建设性证明是通过使用一个反模型的基础上的一个变种的${\sf G4iSL}_\Box$建设。因此，该文件包含两个证明削减消除，语义和句法证明。
Duality and universal models for the meet-implication fragment of IPC
本文利用分配格和万有模型的有限对偶性，研究了直觉主义逻辑中只使用合取和蕴涵的片断。我们给出了这一片段的生成的万有模型的描述，并给出了直觉主义逻辑的Kripke模型的翻转集的完整刻画，这些翻转集可由满足蕴涵公式定义.我们利用这些结果导出了直觉主义逻辑的一个新的子框架公式，并证明了满足蕴涵公式的一致插值在完全直觉主义逻辑中不一定是一致插值.
Base-extension Semantics for Intuitionistic Modal Logics
本文为Simpson直觉主义模态逻辑建立基扩展语义，并证明其相对自然演绎系统的可靠性与完备性。
Definable Classes of Models and Frames in Bi-intuitionistic Logic
研究双直觉逻辑语言对框架和模型的表达能力，通过提供类似戈德布拉特 - 托马森定理的结果，结合先前成果，完整刻画了命题双直觉逻辑的表达能力。
Two-dimensional Kripke Semantics II: Stability and Completeness
本文针对直觉主义及模态逻辑的 Kripke 与代数语义不匹配问题，提出以分配格为基础的稳定语义，并构造性证明其完备性等价，进而通过范畴化建立二维稳定语义与 Lawvere 代数理论模型的 2-对偶。
Infinitary provability logic
本文研究Gödel-Löb可证性逻辑的无穷性对应物，提出非良基深层推理系统$\dgla$，证明其相对于良基传递Kripke框架的可靠性与完备性，并借助Kripke-Platek集合论建立无穷可证性解释，表明Hilbert式变体可靠，且在某些条件下无穷可证性逻辑介于两者之间。
Temporal interpretation of intuitionistic quantifiers
我们表明，直觉量词承认以下的时间解释：$\forall x A$是真的，在一个世界$w$当且仅当$A$是真的，在每个对象的域中的每个未来的世界，和$\exists x A$是真的，在$w$当且仅当$A$是真的，在一些对象的域中的一些过去的世界。为此目的，我们工作的谓词版本的著名的时态命题逻辑$\sf S4.t$。谓词逻辑$\sf Q^\circ S4.t$是通过沿着Corsi将$\sf QK$弱化为$\sf Q^\circ K$的路线弱化$\sf S4.t$的标准谓词扩展$\sf QS4.t$的公理来获得的。哥德尔翻译将谓词直觉主义逻辑$\sf IQC$完全忠实地嵌入到$\sf QS4$中。我们提供了一个时间版本的哥德尔翻译，并证明它嵌入$\sf IQC$到$\sf Q^\circ S4.t$充分和忠实的，也就是说，我们表明，一个句子是可证明的$\sf IQC$当且仅当其翻译是可证明的$\sf Q^\circ S4.t$。忠实性证明使用语法的方法，而我们证明丰满利用广义Kripke语义的Corsi。
Gödel-Dummett and $\mathsf{BD_2}$: Linearity and Depth-Two Branching in Kripke Semantics
本文研究了GL和BD₂之间的语义关系，证明二者不可比，并展示了其结合后接近经典逻辑的特性。
Axiomatic systems and topological semantics for intuitionistic temporal logic
我们提出了四个公理系统的直觉线性时态逻辑，并表明，这些系统是健全的一类结构的基础上Kripke框架或动态拓扑系统。我们的拓扑语义的特点是一个新的解释的“从今以后”的模态，是一个自然的直觉的变体的经典。利用可靠性结果，我们证明了由公理系统得到的四种逻辑是不同的。最后，我们表明，当语言被限制到'henceforth'-免费的片段，一组有效的公式的关系和拓扑语义相吻合。
Bi-modal Gödel logic over [0,1]-valued Kripke frames
考虑由模糊Kripke模型确定的Gödel双模态逻辑，其中命题和可达关系都是标准Gödel代数[0，1]上的无穷值，并证明了Fischer Servi直觉模态逻辑IK加上关于此语义的预线性公理的强完备性.我们也公理化的双峰类似物的$T,$ $S4,$和$S5$通过限制到模型的框架满足[0，1]-值版本的结构特性，这些逻辑的特点。作为完备性定理的应用，我们得到了双峰Gödel代数的一个表示定理。
Not all Kripke models of $\sf HA$ are locally $\sf PA$
令${\bf K}$为海廷算法的任意Kripke模型${\sf HA}$。对于${\bf K}$中的每个节点$k$，我们可以将$k$的经典结构${\mathfrak M}_k$看作是某种经典算术理论的模型。让${\sf T}$成为算术语言中的经典理论。我们说${\bf K}$是局部的${\sf T}$，当且仅当对于${\bf K}$中的每个$k$，${\mathfrak M}_k\models{\sf T}$。${\sf HA}$模型论中最重要的问题之一是以下问题：{ \it是${\sf HA}$的每个Kripke模型局部的${\sf PA}$吗？}我们对这个问题的回答是否定的。为此，我们引入两个新的Kripke模型的建设。第一种结构实际上表征了可以作为克里普克模型${\bf K}\Vdash{\sf HA}+{\sf ECT_0}$（${\sf ECT_0}$代表扩展教会论文）的根的算术结构。该特征表示，对于每个算术结构${\mathfrak M}$，存在一个根Kripke模型${\bf K}\Vdash{\sf HA}+{\sf ECT_0}$，其根$r$使得${\mathfrak M}_r={\mathfrak M}$当且仅当${\mathfrak M}\models{\bf Th}_{Π_2}({\sf PA})$。该特征化的结果之一是，存在具有根$r$的根Kripke模型…
Questions and dependency in intuitionistic logic
近年来，疑问句逻辑和依赖逻辑在探究逻辑和依赖逻辑两个密切相关的框架中得到了研究。这些研究假设经典逻辑作为陈述的背景逻辑，并在这个经典核心中加入了表达问题和依赖关系的公式。在本文中，我们通过在直觉主义逻辑的背景下研究问题和依赖关系来拓宽这些研究的范围。我们提出了一个直观的团队语义，团队嵌入在直观的Kripke模型。伴随逻辑是直觉主义逻辑的一个保守的扩展，带有问题和依赖公式。我们建立了一些关于这个逻辑的结果，包括一个范式的结果，一个完整性的结果，并翻译到经典的查询逻辑和模态依赖逻辑。
A $j$-translation with Kripke forcing relation
本文提出一种结合j-翻译与Kripkeforcing的内部逻辑拓扑学翻译，证明其对直觉逻辑和Heyting算术的正确性，并扩展了de Jongh和Goodman的sheaf模型。
Intuitionistic logic with two Galois connections combined with Fischer Servi axioms
早些时候，作者介绍了逻辑IntGC，它是通过两个模仿伽罗瓦连接性能的推理规则对直觉命题逻辑的扩展（Logic J. of the IGPL，18：837-858，2010）。本文研究了IntGC的扩展Int 2GC和Int 2GC +FS。Int 2GC可以看作是两个IntGC逻辑的融合，Int 2GC +FS是通过添加由G. Fischer Servi（Rend. Sem等Mat.宇宙Politecn. Torino，42：179-194，1984），用于互连Int 2GC的两个伽罗瓦连接。给出了Int 2GC和Int 2GC +FS的Kripke风格和代数语义，并证明了其逻辑在这两种语义下都是完备的。我们证明了定义在完备Heyting代数上的粗糙格值模糊集是Int 2GC +FS的适当代数模型。我们还证明了Int 2GC +FS等价于直觉时态逻辑IKt，以及IKt的一个公理化，其公理数目减少到W给出的公理数目的一半。B. Ewald（J. Symb. Log，51：166-179，1986）。
On subreducts of subresiduated lattices and logic
替代剩余格是在1970年由Epstein和Horn引入的，作为Lewy和Hacking以前研究的一些强蕴涵逻辑的代数对应。这些逻辑是次直觉主义逻辑的例子，即，以直觉主义逻辑的语言的逻辑，其通过使用Kripke模型以与定义直觉主义逻辑相同的方式在语义上定义，但是不要求模型具有直觉主义情况下所需的某些属性。此外，在有关研究subintuitionistic逻辑，切兰尼和Jansana得到这些代数的元素的一个子品种的弱海廷代数。在这里，我们研究了子剩余格的蕴涵子约简和蕴涵下确界子约简。此外，我们提出了一个演算，其代数语义是由这些类的代数。本文还研究了这类演算的几种展开式，并得到了它们的一些有趣的性质。
Infinitary first-order categorical logic
我们提出了一个统一的分类处理的几个经典和直觉无穷逻辑的完备性定理的建议公理化。这提供了新的完备性定理，并包含了Gödel，Kripke，Beth，Karp，Joyal，Makkai和Fourman/Grayson以前的定理。作为应用，我们利用大基数假设证明了无穷直觉一阶逻辑的析取性和存在性。
Implication via Spacetime
本文主要研究蕴涵的最一般形式，推广了不同类型的蕴涵，包括Heyting蕴涵、子结构蕴涵和弱严格蕴涵。在对直觉主义逻辑的拓扑解释之后，我们将引入非交换时空，以提供对直觉主义命题的更动态和主观的解释。这些空间和时间的组合是行为良好的含义的自然来源，我们将证明他们的时空含义代表任何其他合理的抽象含义。然后提供一个忠实的行为良好的语法抽象的影响，我们将开发一个逻辑系统的非交换时空，我们将提出拓扑和Kripke语义。这些逻辑通过把亚结构逻辑和亚直觉主义逻辑作为它们的特殊片段而把它们统一起来。
Provability Models
本文提出名为可证性模型的经典模态逻辑新型克里普克式语义，证明了多类模态逻辑、解释性逻辑ILM对该类模型的可靠性与完全性，并将其改进为谓词可判定版本。
Semantical Analysis of Intuitionistic Modal Logics between CK and IK
本文通过扩展 CK 的克里普克语义以涵盖 IK 公理，解决了 CK 与 IK 之间逻辑在无菱形片段上的保守性开放问题，并使用 Coq 进行了形式化验证。
Intuitionistic Common Knowledge
本文研究了直觉逻辑中的共同知识逻辑变种ICK，扩展了直觉命题逻辑IPL，引入多层知识算子和共同知识算子，并通过birelational Kripke模型分析其语义，证明了逻辑的完备性、有限模型性质和可判定性。
An algebraic generalization of Kripke structures
经典命题正规模态逻辑的Kripke语义是通过将Kripke结构嵌入到更大类的点稳定支撑量子中来代数化的。这种代数语义包含了传统的代数语义的基础上格与一元运算符，它提出了自然的解释模态逻辑，可能感兴趣的应用，在结构中出现的几何和分析，如叶状流形和算子代数，通过拓扑群胚和逆半群。我们研究了系统K，T，K4，S4和S5的基于Quantale的语义的完备性，特别是获得了S5的公理化，它不使用否定或模态必要性算子。作为额外的例子，我们描述直觉命题模态逻辑，程序PDL的逻辑，和分歧的时态逻辑CTL。
A Coalgebraic Semantics for Intuitionistic Modal Logic
本文利用 Esakia 空间到 Priestley 空间包含的右伴随，为带 $\Box$ 的直觉主义模态逻辑建立余代数语义，并应用于互模拟、自由模态 Heyting 代数对偶及余代数直觉主义逻辑理论。
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}的会议论文。
Strong Completeness and the Finite Model Property for Bi-Intuitionistic Stable Tense Logics
双直觉稳定时态逻辑（英语：Bi-Intuitionistic Stable Tense Logics）是一种具有克里普克语义的时态逻辑，其中框架中的世界配备有前序以及相对于该前序“稳定”的可达性关系。BIST逻辑是在超图的语义背景下产生的逻辑BiSKt的扩展，因为预序的特殊情况可以表示超图的关联结构。在本文中，我们提供了，第一次，一个希尔伯特式公理化的BISKt和证明强完备性的BiSKt。我们继续证明强完备性的一类BIST逻辑得到的BiSKt由一定形式的公式扩展。此外，我们还证明了一类BIST逻辑的有限模型性质和可判定性。
Proof-Theoretic Soundness and Completeness
我们给出了一个演算推理的一阶片段的经典逻辑，这是足够的直觉Kripke框架的真值条件，并概述了证明理论的合理性和完整性证明，我们相信这是有利于自动化。
Continuation-passing Style Models Complete for Intuitionistic Logic
一类模型，在连续单子的形式多态的一阶个人，这是健全的和完整的最小直觉谓词逻辑。证明的健全性和完整性是建设性的，其组成的计算内容，特别是一个$β$ -规范化的评估程序简单类型的lambda演算和类型。虽然灵感来自Danvy的类型导向部分求值器，但避免了分隔控制运算符（即计算效果）的必要使用。多态性的作用是至关重要的--去掉它可以让我们获得经典谓词逻辑的模型完备的概念。我们的模型和克里普克模型之间的联系是通过加强双重否定转移图式来实现的。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。