Felipe S. Albarelli, Rodolfo Ertola-Biraben
In 1932, Gödel proved that there is no finite semantics for intuitionistic logic. We consider all fragments of intuitionistic logic and check in each case whether a finite semantics exists. We may fulfill a didactic goal, as little logic and algebra are presupposed.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
On algorithmic expressivity of finite-variable fragments of intuitionistic modal logics
本文证明了直觉主义模态逻辑FS和MIPC可多项式时间嵌入其正单变量片段，揭示了其算法表达力。
Intuitionistic logic, dual intuitionistic logic, and modality
本文通过余海廷代数与拓扑空间的关系研究对偶直觉主义逻辑的语义，并证明其与直觉主义逻辑通过Kripke语义共同关联于模态逻辑S4。
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.
Classical logic (the logic of non-constructive mathematics) is stronger than intuitionistic logic (the logic of constructive mathematics). Despite this, there are copies of classical logic in intuitionistic logic. All copies usually found in the literature are the same. This raises the question: is the copy unique? We answer negatively by presenting three different copies.
Following G. Mints(Kluwer 2000 and draft 2013), we present terminating and bicomplete proof searches in multi-succedent sequent calculi for intuitionistic propositional logic, fragments of intuitionistic predicate logic and full intuitionistic predicate logic in the spirit of Schuette's schema.
Sub-sub-intuitionistic logic
本文通过弱化蕴涵和移除分配律提出次次直觉主义逻辑，利用带选择函数的半格给出其语义，证明范畴对偶性并推导完备性，同时探讨了多种公理扩展。
We prove that the first-order logic of CZF is intuitionistic first-order logic. To do so, we introduce a new model of transfinite computation (Set Register Machines) and combine the resulting notion of realisability with Beth semantics. On the way, we also show that the propositional admissible rules of CZF are exactly those of intuitionistic propositional logic.
An intuitionistically complete system of basic intuitionistic conditional logic
本文提出基本直觉主义条件逻辑IntCK，证明其相对克里普克模型和一阶直觉主义逻辑翻译的完备性，并分析其与CK、IK及Weiss的ICK的关系，讨论候选系统的优劣。
In the style of Lindström's theorem for classical first-order logic, this article characterizes propositional bi-intuitionistic logic as the maximal (with respect to expressive power) abstract logic satisfying a certain form of compactness, the Tarski union property and preservation under bi-asimulations. Since bi-intuitionistic logic introduces new complexities in the intuitionistic setting by adding the analogue of a backwards looking modality, the present paper constitutes a non-trivial modification of previous work done by the authors for intuitionistic logic in: G. Badia and G. Olkhovikov…
We find a translation with particularly nice properties from intuitionistic propositional logic in countably many variables to intuitionistic propositional logic in two variables. In addition, the existence of a possibly-not-as-nice translation from any countable logic into intuitionistic propositional logic in two variables is shown. The nonexistence of a translation from classical logic into intuitionistic propositional logic which preserves ``and'' and ``or'' but not necessarily ``true'' is proven. These results about translations follow from additional results about embeddings into free He…
We prove that there is a factor of the Muchnik lattice that captures intuitionistic propositional logic. This complements a now classic result of Skvortsova for the Medvedev lattice.
It is known that intuitionistic Kripke semantics can be generalized so that it can treat arbitrary propositional connectives characterized by truth functions. We extend this generalized Kripke semantics to first-order logic, and study how the choice of connectives changes the relation between intuitionistic predicate logic and the logic of constant domains in terms of validity of sequents. Our main result gives a simple necessary and sufficient condition for the set of valid sequents in intuitionistic predicate logic to coincide with the set of valid sequents in the logic of constant domains.
We extend the main result of (G. Badia and G. Olkhovikov. A Lindström theorem for intuitionistic propositional logic. Notre Dame Journal of Formal Logic, 61 (1): 11--30 (2020)) to the first-order intuitionistic logic (with and without equality), showing that it is the maximal (with respect to expressive power) abstract logic satisfying a certain form of compactness, the Tarski union property and preservation under asimulations. A similar result is also shown for the intuitionistic logic of constant domains.
The paper treats 4 different fragments of first-order logic induced by their respective versions of Kripke style semantics for modal intuitionistic logic. In order to capture these fragments, the notion of asimulation is modified and extended to yield Van Benthem type of semantic characterization of their respective expressive powers. It is shown, further, that this characterization can be easily carried over to arbitrary first-order definable subclasses of classical first-order models.
It is shown that propositional intuitionistic logic is the maximal (with respect to expressive power) abstract logic satisfying a certain topological property reminiscent of compactness, the Tarski union property and preservation under asimulations.
Drawing on the previous work on interpolation failure, we show that Beth's definability theorem does not hold for intuitionistic predicate logic of constant domains without identity.
We show that the intuitionistic propositional logic with a Galois connection (IntGC), introduced by the authors, has the finite model property.
We offer the proofs that complete our article introducing the propositional calculus called semi-intuitionistic logic with strong negation.
On the Various Translations between Classical, Intuitionistic and Linear Logic
本文以直觉主义线性逻辑的扩张为共同基础，提出统一方法设计和简化经典、直觉主义与线性逻辑之间的证明翻译，并由此重新得到文献中多数著名翻译。
It is known that the set of tautologies of second order intuitionistic propositional logic, $\mathrm{IPC} 2$, is undecidable. Here, we prove that the sets of formulas of $\mathrm{IPC} 2$ which are true in the algebra of open subsets of reals or rationals are decidable.
Quantified propositional intuitionistic logic is obtained from propositional intuitionistic logic by adding quantifiers \forall p, \exists p over propositions. In the context of Kripke semantics, a proposition is a subset of the worlds in a model structure which is upward closed. Kremer (1997) has shown that the quantified propositional intuitionistic logic Hπ+ based on the class of all partial orders is recursively isomorphic to full second-order logic. He raised the question of whether the logic resulting from restriction to trees is axiomatizable. It is shown that it is, in fact, decidable.…
We show that intuitionistic logic is deductively equivalent to Connexive Heyting Logic (CHL), hereby introduced as an example of a strong connexive logic with intuitive semantics. We use the reverse algebraisation paradigm: CHL is presented as the assertional logic of a point regular variety (whose structure theory is examined in detail) that turns out to be term equivalent to the variety of Heyting algebras. We provide Hilbert-style and Gentzen-style proof systems for CHL; moreover, we suggest a possible computational interpretation of its connexive conditional, and we revisit Kapsner's idea …
In their seminal paper Artemov and Protopopescu provide Hilbert formal systems, Brower-Heyting-Kolmogorov and Kripke semantics for the logics of intuitionistic belief and knowledge. Subsequently Krupski has proved that the logic of intuitionistic knowledge is PSPACE-complete and Su and Sano have provided calculi enjoying the subformula property. This paper continues the investigations around to sequent calculi for Intuitionistic Epistemic Logics by providing sequent calculi that have the subformula property and that are terminating in linear depth. Our calculi allow us to design a procedure th…
We introduce the logic $\sf ITL^e$, an intuitionistic temporal logic based on structures $(W,\preccurlyeq,S)$, where $\preccurlyeq$ is used to interpret intuitionistic implication and $S$ is a $\preccurlyeq$-monotone function used to interpret temporal modalities. Our main result is that the satisfiability and validity problems for $\sf ITL^e$ are decidable. We prove this by showing that the logic enjoys the strong finite model property. In contrast, we also consider a `persistent' version of the logic, $\sf ITL^p$, whose models are similar to Cartesian products. We prove that, unlike $\sf ITL…
Supervaluations, truth, and intuitionistic logic
本文提出了一种基于超估值方法的直觉逻辑固定点真理理论，并展示了其在Kripke结构上的应用及与经典逻辑的对比。
Polytopological Semantics for Intuitionistic Modal Logics
本文提出多拓扑语义用于构造、直觉及Goedel-Dummett的K4和S4变种，通过单一集合上的多种拓扑解释直觉和模态运算符，并证明这些逻辑在相应语义下是正确且强完备的。
Relative Unification in Intuitionistic Logic: Towards provability logic of HA
该研究将直觉主义逻辑的统一性与可容许性结果推广到 NNIL(par) 命题，用以刻画 HA 的可证性逻辑并证明其可判定性。
We show that intuitionistic propositional logic is \emph{Carnap categorical}: the only interpretation of the connectives consistent with the intuitionistic consequence relation is the standard interpretation. This holds relative to the most well-known semantics with respect to which intuitionistic logic is sound and complete; among them Kripke semantics, Beth semantics, Dragalin semantics, and topological semantics. It also holds for algebraic semantics, although categoricity in that case is different in kind from categoricity relative to possible worlds style semantics.
Projectivity meets Uniform Post-Interpolant: Classical and Intuitionistic Logic
本文研究经典与直觉主义命题逻辑中投射性与一致后插值的关系，证明经典逻辑中二者对所有公式等价，并给出直觉主义逻辑的Kripke语义刻画，进而证明某些直觉主义逻辑扩张的统一类型是有穷的。
We prove that the propositional logic of intuitionistic set theory IZF is intuitionistic propositional logic IPC. More generally, we show that IZF has the de Jongh property with respect to every intermediate logic that is complete with respect to a class of finite trees. The same results follow for CZF.
Bi-intuitionistic logics through the abstract algebraic logic lens
针对双直觉主义逻辑缺乏代数处理的问题，研究者用抽象代数逻辑等方法对wBIL和sBIL开展代数分析，相关结果已在Rocq中形式化。
Esakia's theorem for the amended monadic intuitionistic calculus
该研究证明修正的单子直觉逻辑M^+IPC的Esakia定理成立，揭示了其与修正的单子Grzegorczyk逻辑之间的关系。
This report first shows the equivalence bewteen several formulations of classical logic in intuitionistic logic (tertium non datur, reductio ad absurdum, Pierce's law). Then it establishes the correctness of the Gödel-Kolmogorov translation, whose restriction to the propositional case is due to Glivenko. This translation maps a formula $F$ of first order logic to a formula $F^{\lnot\lnot}$ in such a way that $F$ is provable in classical logic if and only if $F^{\lnot\lnot}$ is provable in intuitionistic logic. All formal proofs are presented in natural deduction. These questions are well-known…
This paper shows that the interpolation theorem fails in the intuitionistic logic of constant domains. This result refutes two previously published claims that the interpolation property holds.
Both propositional dependence logic and inquisitive logic are expressively complete. As a consequence, every formula with intuitionistic disjunction or intuitionistic implication can be translated equivalently into a formula in the language of propositional dependence logic without these two connectives. We show that although such a (non-compositional) translation exists, neither intuitionistic disjunction nor intuitionistic implication is uniformly definable in propositional dependence logic.
Definable Classes of Models and Frames in Bi-intuitionistic Logic
研究双直觉逻辑语言对框架和模型的表达能力，通过提供类似戈德布拉特 - 托马森定理的结果，结合先前成果，完整刻画了命题双直觉逻辑的表达能力。
Intuitionistic Sahlqvist theory for deductive systems
本文将 Sahlqvist 理论扩展至包含合取连接词的直觉主义命题演算片段，引入了适用于任意原代数演绎系统的直觉主义 Sahlqvist 理论，并据此为包含蕴涵连接词的演算片段及直觉主义线性逻辑扩展导出了 Sahlqvist 定理。
In this paper we construct a Beth model for intuitionistic functionals of high types and use it to create a relatively strong theory SLP containg intuitionistic principles for functionals, in particular, the theory of the "creating subject", axioms for lawless functionals and some versions of choice axioms. We prove that the intuitionistic theory SLP is equiconsistent with a classical typed set theory TI, where the comprehension axiom for sets of type n is restricted to formulas with no parameters of types > n. We show that each fragment of SLP with types <= s is equiconsistent with the corres…
We investigate properties of monadic purely negational fragment of Intuitionistic Control Logic (ICL). This logic arises from Intuitionistic Propositional Logic (IPL) by extending language of IPL by additional new constant for falsum. Having two different falsum constants enables to define two forms of negation. We analyse implicational relations between negational monadic formulae and present a poset of non equivalent formulae of this fragment of ICL.
Intuitionistic epistemic logic introduces an epistemic operator, which reflects the intended BHK semantics of intuitionism, to intuitionistic logic. The fundamental assumption concerning intuitionistic knowledge and belief is that it is the product of verification. The BHK interpretation of intuitionistic logic has a precise formulation in the Logic of Proofs and its arithmetical semantics. We show here that this interpretation can be extended to the notion of verification upon which intuitionistic knowledge is based, thereby providing the systems of intuitionistic epistemic logic extended by …
Prawitz conjectured that the proof-theoretically valid logic is intuitionistic logic. Recent work on proof-theoretic validity has disproven this. In fact, it has been shown that proof-theoretic validity is not even closed under substitution. In this paper, we make a minor modification to the definition of proof-theoretic validity found in Prawitz (1973) and refined by Schroeder-Heister (2006). We will call the new notion generalised proof-theoretic validity and show that the logic of generalised proof-theoretic validity is intuitionistic logic.
Intuitionistic and Constructive Modal Logics for Classical Modal Logicians
本文面向经典模态逻辑研究者，综述直觉主义框架下的两类命题模态逻辑，研究介于两者间的新逻辑$\textbf{KI}$并证其完备性，还指出$\textbf{CK}$语义缺陷并证明$\textbf{CK}$、$\textbf{WK}$的Lyndon插值定理。
Intuitionistic K is a Bisimulation-Invariant Fragment of Intuitionistic First-Order Logic
定义直觉主义模态逻辑IK的关系语义上的IK-双模拟，证明IK是直觉主义一阶逻辑的IK-双模拟不变片段，并给出内在刻画及Hennessy-Milner型定理，发展直觉主义一阶模型论。
Given a weakly compact cardinal $κ$, we give an axiomatization of intuitionistic first-order logic over $\mathcal{L}_{κ^+, κ}$ and prove it is sound and complete with respect to Kripke models. As a consequence we get the disjunction and existence properties for that logic. This generalizes the work of Nadel for intuitionistic logic over $\mathcal{L}_{ω_1, ω}$. When $κ$ is a regular cardinal such that $κ^{<κ}=κ$, we deduce, by an easy modification of the proof, a complete axiomatization of intuitionistic first-order logic over $\mathcal{L}_{κ^+, κ, κ}$, the language with disjunctions of at most…
Let V be a set of number-theoretical functions. We define a notion of V -realizability for predicate formulas in such a way that the indices of functions in V are used for interpreting the implication and the universal quantifier. In this paper we prove that Intuitionistic Predicate Calculus is sound with respect to the semantics of V -realizability if and only if some natural conditions for V hold.
We present three examples of \textit{multi-topological} semantics for intuitionistic modal logic with one modal operator $\Box$ (which behaves in some sense like necessity). We show that it is possible to treat neighborhood models, introduced earlier, as multi-topological. From the neighborhood point of view, our method is based on differences between properties of minimal and maximal neighborhoods. Also we propose transformation of multi-topological spaces into the neighborhood structures. Although our neighborhoods can be considered as bi-relational models, we believe that reasoning in terms…
In this paper we investigate the fragment of intuitionistic logic which only uses conjunction (meet) and implication, using finite duality for distributive lattices and universal models. We give a description of the finitely generated universal models of this fragment and give a complete characterization of the up-sets of Kripke models of intuitionistic logic which can be defined by meet-implication-formulas. We use these results to derive a new version of subframe formulas for intuitionistic logic and to show that the uniform interpolants of meet-implication-formulas are not necessarily unifo…
Stable Canonical Rules for Intuitionistic Modal Logics
本文研究了直观模态逻辑的稳定公理规则，证明了多结论推论关系可由稳定公理规则 axiomatize，并以此证明了Blok-Esakia定理的替代证明及扩展，同时解决了Dummett-Lemmon猜想。
Intuitionistic modal logics: a minimal setting
本文提出一种严格包含于IK的直觉主义模态逻辑，作为最小正规直觉主义模态逻辑的候选，并探讨其设定。
Boudou and the authors have recently introduced the intuitionistic temporal logic $\sf ITL^e$ and shown it to be decidable. In this article we show that the `henceforth'-free fragment of this logic is complete for the class of non-deterministic quasimodels introduced by Fernández-Duque. From this and results of Boudou, Romero and the authors, we conclude that this fragment is also complete for the standard semantics of $\sf ITL^e$ over the class of expanding posets.
We prove a Goldblatt-Thomason theorem for dialgebraic intuitionistic logics, and instantiate it to Goldblatt-Thomason theorems for a wide variety of modal intuitionistic logics from the literature.
This work is a mathematician's attempt to understand intuitionistic logic. It can be read in two ways: as a research paper interspersed with lengthy digressions into rethinking of standard material; or as an elementary (but highly unconventional) introduction to first-order intuitionistic logic. For the latter purpose, no training in formal logic is required, but a modest literacy in mathematics, such as topological spaces and posets, is assumed. The main theme of this work is the search for a formal semantics adequate to Kolmogorov's informal interpretation of intuitionistic logic (whose simp…
This paper introduces two sequent calculi for intuitionistic strong Löb logic ${\sf iSL}_\Box$: a terminating sequent calculus ${\sf G4iSL}_\Box$ based on the terminating sequent calculus ${\sf G4ip}$ for intuitionistic propositional logic ${\sf IPC}$ and an extension ${\sf G3iSL}_\Box$ of the standard cut-free sequent calculus ${\sf G3ip}$ without structural rules for ${\sf IPC}$. One of the main results is a syntactic proof of the cut-elimination theorem for ${\sf G3iSL}_\Box$. In addition, equivalences between the sequent calculi and Hilbert systems for ${\sf iSL}_\Box$ are established. It …
Takeuti and Titani have introduced and investigated a logic they called intuitionistic fuzzy logic. This logic is characterized as the first-order Goedel logic based on the truth value set [0,1]. The logic is known to be axiomatizable, but no deduction system amenable to proof-theoretic, and hence, computational treatment, has been known. Such a system is presented here, based on previous work on hypersequent calculi for propositional Goedel logics by Avron. It is shown that the system is sound and complete, and allows cut-elimination. A question by Takano regarding the eliminability of the Ta…
Intuitionistic monotone modal logic via translation
本文通过翻译到直觉主义一阶逻辑，提出直觉主义正规模态逻辑IK的单调模态类比，给出公理化与直觉主义邻域模型语义，并比较其他直觉主义单调模态逻辑及嵌入到IK多模态版本的方法。
We outline an intuitionistic view of knowledge which maintains the original Brou\-wer-Heyting-Kolmogorov semantics for intuitionism and is consistent with the well-known approach that intuitionistic knowledge be regarded as the result of verification. We argue that on this view co-reflection $A \rightarrow {\bf{K}} A$ is valid and the factivity of knowledge holds in the form ${\bf{K}} A \rightarrow \neg\neg A$ `known propositions cannot be false'. We show that the traditional form of factivity ${\bf{K}} A \rightarrow A$ is a distinctly classical principle which, like {\it tertium non datur} $A…
We give Hennessy-Milner classes for intuitionistic, dual-intuitionistic and bi-intuitionistic logic interpreted in intuitionistic Kripke models, and generalise these results to modal (dual- and bi-)intuitionistic logics. Our main technical tools are image-compact and pre-image-compact relations that provide a semantical description of modal saturation properties.
We introduce a realisability semantics for infinitary intuitionistic set theory that is based on Ordinal Turing Machines (OTMs). We show that our notion of OTM-realisability is sound with respect to certain systems of infinitary intuitionistic logic, and that all axioms of infinitary Kripke-Platek set theory are realised. Finally, we use a variant of our notion of realisability to show that the propositional admissible rules of (finitary) intuitionistic Kripke-Platek set theory are exactly the admissible rules of intuitionistic propositional logic.
In a 1985 commentary to his collected works, Kolmogorov remarked that his 1932 paper "was written in hope that with time, the logic of solution of problems [i.e., intuitionistic logic] will become a permanent part of a [standard] course of logic. A unified logical apparatus was intended to be created, which would deal with objects of two types - propositions and problems." We construct such a formal system, as well as its predicate version QHC, which is a conservative extension of both the intuitionistic predicate calculus QH and the classical predicate calculus QC. The only new connectives ? …
We present the logic iJT4, which is an explicit version of intuitionistic S4 and establish soundness and completeness with respect to modular models.
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。