Robert Goldblatt, Ian Hodkinson
We prove strong completeness results for some modal logics with the universal modality, with respect to their topological semantics over 0-dimensional dense-in-themselves metric spaces. We also use failure of compactness to show that, for some languages and spaces, no standard modal deductive system is strongly complete.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
This thesis aims to provide a suite of techniques to generate completeness results for coalgebraic logics with axioms of arbitrary rank. We have chosen to investigate the possibility to generalize what is arguably one of the most successful methods to prove completeness results in `classical' modal logic, namely completeness-via-canonicity. This technique is particularly well-suited to a coalgebraic generalization because of its clean and abstract algebraic formalism.
We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the completeness of variants of classical and intuitionistic natural deduction and sequent calculi with respect to model-theoretic, algebraic, and game-theoretic semantics. As completeness with respect to the standard model-theoretic semantics à la Tarski and Kripke is not readily constructive, we analyse connections of completeness theorems to Markov's Principle and Weak König's Lemma and discuss non-standard semantics a…
There has been a significant interest in extending various modal logics with intersection, the most prominent examples being epistemic and doxastic logics with distributed knowledge. Completeness proofs for such logics tend to be complicated, in particular on model classes such as S5 like in standard epistemic logic, mainly due to the undefinability of intersection of modalities in standard modal logics. A standard proof method for the S5 case was outlined in [8] and later explicated in more detail in [13], using an "unraveling-folding method" case to achieve a treelike model to deal with the …
Bi-Intuitionistic Stable Tense Logics (BIST Logics) are tense logics with a Kripke semantics where worlds in a frame are equipped with a pre-order as well as with an accessibility relation which is 'stable' with respect to this pre-order. BIST logics are extensions of a logic, BiSKt, which arose in the semantic context of hypergraphs, since a special case of the pre-order can represent the incidence structure of a hypergraph. In this paper we provide, for the first time, a Hilbert-style axiomatisation of BISKt and prove the strong completeness of BiSKt. We go on to prove strong completeness of…
Importing soundness and completeness in modal logics
提出从表达能力更强的模态语言向较弱语言传递可靠性与完全性的通用策略，统一了多种算子可定义性概念，并通过语义不敏感性和保真翻译实现。
Game logic was introduced by Rohit Parikh in the 1980s as a generalisation of propositional dynamic logic (PDL) for reasoning about outcomes that players can force in determined 2-player games. Semantically, the generalisation from programs to games is mirrored by moving from Kripke models to monotone neighbourhood models. Parikh proposed a natural PDL-style Hilbert system which was easily proved to be sound, but its completeness has thus far remained an open problem. In this paper, we introduce a cut-free sequent calculus for game logic, and two cut-free sequent calculi that manipulate annota…
Completeness of Tableau Calculi for Two-Dimensional Hybrid Logics
本文提出二元混合逻辑的完备表记演算，同时构建了依赖维度的混合依赖积逻辑演算，并证明其完备性，但所有系统均不具终止性。
An algebraic proof is presented for the finite strong standard completeness of involutive uninorm logic with fixed point. The result may provide a first step towards settling the open standard completeness problem for involutive uninorm logic posed in [G. Metcalfe, F. Montagna: Substructural fuzzy logics, J. Symb. Logic, 72, 834-864 (2007)].
We investigate a recent proposal for modal hypersequent calculi. The interpretation of relational hypersequents incorporates an accessibility relation along the hypersequent. These systems give the same interpretation of hypersequents as Lellman's linear nested sequents, but were developed independently by Restall for S5 and extended to other normal modal logics by Parisi. The resulting systems obey Dosen's principle: the modal rules are the same across different modal logics. Different modal systems only differ in the presence or absence of external structural rules. With the exception of S5,…
Proof-Theoretic Functional Completeness for the Connexive Logic C
本文通过纯证明论方法，在双边主义框架下结合相干推理理解，证明了逻辑C联结词的功能完备性。
We present a simpler way than usual to deduce the completeness theorem for the second-oder classical logic from the first-order one. We also extend our method to the case of second-order intuitionistic logic.
In the present paper, we continue the research in \cite{Zh21c} to develop the Sahlqvist-type completeness theory for hybrid logic with satisfaction operators and downarrow binders $\mathcal{L}(@, \downarrow)$. We define the class of skeletal Sahlqvist formulas for $\mathcal{L}(@, \downarrow)$ following the ideas in \cite{ConRob}, but we follow a different proof strategy which is purely proof-theoretic, namely showing that for every skeletal Sahlqvist formula $ϕ$ and its hybrid pure correspondence $π$, $\mathbf{K}_{\mathcal{H}(@, \downarrow)}+ϕ$ proves $π$, therefore $\mathbf{K}_{\mathcal{H}(@,…
It is known that the satisfiability problems of the product logics K4xS5 and S4xS5 and of the logic SSL of subset spaces are in N2EXPTIME. We improve this upper bound for the complexity of these problems by presenting ESPACE-algorithms for these problems. In another paper we show that these problems are EXPSPACE-hard. This shows that all three problems are EXPSPACE-complete.
In 1933, Gödel considered two modal approaches to describing provability. One captured formal provability and resulted in the logic GL and Solovay's Completeness Theorem. The other was based on the modal logic S4 and led to Artemov's Logic of Proofs LP. In this paper, we study introduced by the author logic GLA, which is a fusion of GL and LP in the union of their languages. GLA is supplied with a Kripke-style semantics and the corresponding completeness theorem. Soundness and completeness of GLA with respect to the arithmetical provability semantics is established.
We present a completeness result for the implicit fragment of justification stit logic. Although this fragment allows for no strongly complete axiomatization, we show that a restricted form of strong completeness (subsuming weak completeness) is available, as well as deduce a version of restricted compactness property.
Subreflexive Logic: Completeness without Identity
研究次自反逻辑，通过多种方式构建语义，包括引入海廷和布尔半代数、定义半伴随和单位等，证明其具有可靠且完备语义，能将蕴含解释为稳健后承，还允许句法消去切割，在经典情形下特定指称集语义也完备。
We consider dynamic versions of epistemic logic as formulated in Baltag and Moss "Logics for epistemic programs" (2004). That paper proposed a logical language (actually families of languages parameterized by action signatures) for dynamic epistemic logic. It had been shown that validity in the language is Pi-1-1-complete, so there are no recursively axiomatized complete logical systems for it. In contrast, this paper proves a weak completeness result for the fragment without action iteration, and a strong completeness result for the fragment without action iteration and common knowledge. Our …
We begin the study of categorical logic for continuous model theory. In particular, we 1. introduce the notions of metric logical categories and functors as categorical equivalents of a metric theory and interpretations, 2. prove a continuous version of conceptual completeness showing that $T^\eq$ is the maximal conservative expansion of $T$, and 3. define the concept of a metric pre-topos.
We provide a sound and complete proof system for an extension of Kleene's ternary logic to predicates. The concept of theory is extended with, for each function symbol, a formula that specifies when the function is defined. The notion of "is defined" is extended to terms and formulas via a straightforward recursive algorithm. The "is defined" formulas are constructed so that they themselves are always defined. The completeness proof relies on the Henkin construction. For each formula, precisely one of the formula, its negation, and the negation of its "is defined" formula is true on the constr…
It is known that the satisfiability problems of the product logics K4xS5 and S4xS5 are NEXPTIME-hard and that the satisfiability problem of the logic SSL of subset spaces is PSPACE-hard. We improve these lower bounds for the complexity of these problems by showing that all three problems are EXPSPACE-hard under logspace reduction. In another paper we show that these problems are in ESPACE. This shows that all three problems are EXPSPACE-complete.
A logic is said to admit an equational completeness theorem when it can be interpreted into the equational consequence relative to some class of algebras. We characterize logics admitting an equational completeness theorem that are either locally tabular or have some tautology. In particular, it is shown that a protoalgebraic logic admits an equational completeness theorem precisely when its has two distinct logically equivalent formulas. While the problem of determining whether a logic admits an equational completeness theorem is shown to be decidable both for logics presented by a finite set…
Completeness in local positive logic
本文提出融合正逻辑与局部逻辑的局部正逻辑，并系统研究其紧致性、正封闭性与完备性等基础模型论性质。
We present a completeness result for a logical system which combines stit logic and justification logic in order to represent proving activity of the agents. This logic is interpreted over the semantics introduced in earlier publications. We define a Hilbert-style axiomatic system for this logic and show that this system is strongly complete relative to the intended semantics.
Conceptual completeness for subgeometric logics
研究几何逻辑片段的“概念完备性”，通过理论与拓扑斯之间的对偶刻画，证明相干逻辑等片段在完整几何逻辑中保守嵌入，并等价于基于集合模型的传统重构定理。
In this paper, we present a generalized effective completeness theorem for continuous logic. The primary result is that any continuous theory is satisfied in a structure which admits a presentation of the same Turing degree. It then follows that any decidable theory is satisfied by a computably presentable structure. This modifies and extends previous partial effective completeness theorems for continuous logic given by Calvert and Didehvar, Ghasemloo, and Pourmahdian.
In the present article, we extend the fragment of inductive formulas for the hybrid language L(@) in [8] including a McKinsey-like formula, and show that every formula in the extended class has a first-order correspondent, by modifying the algorithm hybrid-ALBA in [8]. We also identify a subclass of this extended inductive fragment, namely the extended skeletal formulas, which extend the class of skeletal formulas in [8], each formula in which axiomatize a complete hybrid logic. Our proof method here is proof-theoretic, following [10, 19] and [3, Chapter 14], in contrast to the algebraic proof…
A formal proof of modal completeness for provability logic
本研究在HOL Light定理证明器中实现哥德尔-勒布可证性逻辑（GL）模态完备性的形式化证明，介绍实现细节与非标准证明结构选择，并分析该形式化系统推理的优缺点。
We give a sufficient condition for Kripke completeness of modal logics enriched with the transitive closure modality. More precisely, we show that if a logic admits what we call definable filtration (ADF), then such an expansion of the logic is complete; in addition, has the finite model property, and again ADF. This argument can be iterated, and as an application we obtain the finite model property for PDL-like expansions of logics that ADF.
On the Completeness of Interpolation Algorithms
该研究聚焦插值算法可得到的插值元范围问题，定义了插值算法的完备性概念，并针对多类逻辑的标准消解与相继式演算算法，得出了不完备性及不同类型的完备性结果。
We consider quantified pretransitive Horn modal logic. It is known that such logics are complete with respect to predicate Kripke frames with expanding domains. In this paper we prove that they are also complete with respect to neighbourhood frames with constant domains.
Completeness theorems for modal logic in second-order arithmetic
本文在二阶算术框架下研究模态命题逻辑完备性定理的逻辑强度，证明弱完备性定理在 $\mathrm{RCA}_0$ 中可证，且强完备性定理分别等价于 $\mathrm{ACA}_0$ 和 $\mathrm{WKL}_0$。
Many-valued coalgebraic dynamic logics: Safety and strong completeness via reducibility
本文提出多值余格动态逻辑框架，通过可约性证明安全性与强完备性，应用于PDL和游戏逻辑的扩展。
In this paper, we study the provability logic of intuitionistic theories of arithmetic that prove their own completeness. We prove a completeness theorem for theories equipped with two provability predicates $\Box$ and $\triangle$ that prove the schemes $A\to\triangle A$ and $\Box\triangle S\to\Box S$ for $S\inΣ_1$. Using this theorem, we determine the logic of fast provability for a number of intuitionistic theories. Furthermore, we reprove a theorem previously obtained by M. Ardeshir and S. Mojtaba Mojtahedi determining the $Σ_1$-provability logic of Heyting Arithmetic.
The paper is dedicated to the problem of adding a modality to the \Lukasiewicz many-valued logics in the purpose of obtaining completeness results for Kripke semantics. We define a class of modal many-valued logics and their corresponding Kripke models and modal many-valued algebras. Completeness results are considered through the construction of a canonical model. Completeness is obtained for modal finitely-valued logics but also for a modal many-valued system with an infinitary deduction rule. We introduce two classes of frames for the finitely-valued logics and show that they define two dis…
We consider the explicit fragment of the basic justification stit logic introduced in earlier publications. We define a Hilbert-style axiomatic system for this logic and show that this system is strongly complete relative to the intended semantics.
Proof-theoretic Semantics for First-order Logic
本文为一阶经典逻辑的证明论语义提供了一种初等、构造性且原生的完备性证明，并同时给出一阶直觉主义逻辑的可靠性与完备性证明。
The logics RL, RP, and RG have been obtained by expanding Lukasiewicz logic L, product logic P, and Gödel--Dummett logic G with rational constants. We study the lattices of extensions and structural completeness of these three expansions, obtaining results that stand in contrast to the known situation in L, P, and G. Namely, RL is hereditarily structurally complete. RP is algebraized by the variety of rational product algebras that we show to be Q-universal. We provide a base of admissible rules in RP, show their decidability, and characterize passive structural completeness for extensions of …
In [Mon11] are studied, for the axiomatic extensions of the monoidal t-norm based logic ([EG01]), the properties of single chain completeness. On the other side, in [GJKO07, Chapter 5] are studied many logical and algebraic properties (like Halldén completeness, variable separation properties, amalgamation property etc.), in the context of substructural logics. The aim of this paper is twofold: first of all we will specialize the properties studied in [GJKO07, Chapter 5] from the case of substructural logics to the one of extensions of MTL, by obtaining some general characterization. Moreover …
We study modal completeness and incompleteness of several sublogics of the interpretability logic $\mathbf{IL}$. We introduce the sublogic $\mathbf{IL}^-$, and prove that $\mathbf{IL}^-$ is sound and complete with respect to Veltman prestructures which are introduced by Visser. Moreover, we prove the modal completeness of twelve logics between $\mathbf{IL}^-$ and $\mathbf{IL}$ with respect to Veltman prestructures. On the other hand, we prove that eight natural sublogics of $\mathbf{IL}$ are modally incomplete. Finally, we prove that these incomplete logics are complete with respect to general…
The primary purpose of this article is to show that a certain natural set of axioms yields a completeness result for continuous first-order logic. In particular, we show that in continuous first-order logic a set of formulae is (completely) satisfiable if (and only if) it is consistent. From this result it follows that continuous first-order logic also satisfies an \emph{approximated} form of strong completeness, whereby $Σ\vDashφ$ (if and) only if $Σ\vdashφ\dotminus 2^{-n}$ for all $n<ω$. This approximated form of strong completeness asserts that if $Σ\vDashφ$, then proofs from $Σ$, being fin…
An algebraic setting for the validity of Pavelka style completeness for some natural expansions of Łukasiewicz logic by new connectives and rational constants is given. This algebraic approach is based on the fact that the standard MV-algebra on the real segment $[0, 1]$ is an injective MV-algebra. In particular the logics associated with MV-algebras with product and with divisible MV-algebras are considered.
Approximate Completeness of Hypersequent Calculus for First-Order Łukasiewicz Logic
针对 Baaz 和 Metcalfe 的 GŁ∀ 近似完备性仅适用于前束公式的局限，本文将原证明推广至超矢列，证明其对任意一阶 Łukasiewicz 公式均近似完备。
A proof for completeness of Łukasiewicz logic
本研究提出一种基于极大一致扩张的Hilbert式证明新方法，给出了1930年Łukasiewicz与Tarski提出的无穷值命题Łukasiewicz逻辑的完备性证明，并举例说明其极大扩张的特性。
The paper studies the containment companion of a logic $\vdash$. This consists of the consequence relation $\vdash^{r}$ which satisfies all the inferences of $\vdash$, where the variables of the conclusion are \emph{contained} into those of the (set of) premises. In accordance with our previous work on logics of left variable inclusion, we show that a different generalization of the Płonka sum construction, adapted from algebras to logical matrices, allows us to provide a matrix-based semantics for containment logics. In particular, we provide an appropriate completeness theorem for a wide fam…
This paper exhibits a general and uniform method to prove completeness for certain modal fixpoint logics. Given a set Γof modal formulas of the form γ(x, p1, . . ., pn), where x occurs only positively in γ, the language L\sharp (Γ) is obtained by adding to the language of polymodal logic a connective \sharp\_γfor each γε. The term \sharp\_γ(\varphi1, . . ., \varphin) is meant to be interpreted as the least fixed point of the functional interpretation of the term γ(x, φ1, . . ., φn). We consider the following problem: given Γ, construct an axiom system which is sound and complete with respect t…
In this paper we prove that three of the main propositional logics of dependence (including propositional dependence logic and inquisitive logic), none of which is structural, are structurally complete with respect to a class of substitutions under which the logics are closed. We obtain an analogues result with respect to stable substitutions, for the negative variants of some well-known intermediate logics, which are intermediate theories that are closely related to inquisitive logic.
Assuming the existence of suitable large cardinals, we show it is consistent that the Provability logic $\mathbf{GL}$ is complete with respect to the filter sequence of normal measures. This result answers a question of Andreas Blass from 1990 and a related question of Beklemishev and Joosten.
Some General Completeness Results for Propositionally Quantified Modal Logics
本文研究命题量化模态逻辑的完全性问题，证明含Barcan模式的正规逻辑在可量化一般框架下强完全，给出公式真值在框架过渡中保持的充分条件，并基于有限多样性得到一类Kripke完全的逻辑及欧几里得框架逻辑的有限公理化。
By operations on models we show how to relate completeness with respect to permissive-nominal models to completeness with respect to nominal models with finite support. Models with finite support are a special case of permissive-nominal models, so the construction hinges on generating from an instance of the latter, some instance of the former in which sufficiently many inequalities are preserved between elements. We do this using an infinite generalisation of nominal atoms-abstraction. The results are of interest in their own right, but also, we factor the mathematics so as to maximise the ch…
We prove a topological completeness theorem for the modal logic GLP containing operators $\langleλ\rangle$ for $λ\in$ Ord intended to capture progressively stronger notions of consistency in mathematical theories. We show that, given a scattered space $X$ of large-enough rank, any sentence $ϕ$ consistent with GLP can be satisfied in a polytopological space based on the finitely many Icard topologies over $X$ that correspond to the finitely many modalities appearing in $ϕ$.
Strong standard completeness theorems for S5-modal Lukasiewicz logics
本文研究基于Łukasiewicz t-范数的逻辑的S5模态扩张，通过构造有穷命题演算并引入无穷规则，借助monadic MV-代数的函数表示与有限嵌入性质，证明了有限强完备性与强完备性定理，并推广到有界论域模型。
A Henkin-style proof of completeness of first-order classical logic is given with respect to a very small set (notably missing cut rule) of Genzten deduction rules for intuitionistic sequents. Insisting on sparing on derivation rules, satisfiability theorem is seen to need weaker assumptions than completeness theorem, the missing request being exactly the rule ~ p --> p, which gives a hint of intuitionism's motivations from a classical point of view. A bare treatment of standard, basic first-order syntax somehow more algebraic-flavoured than usual is also given.
Closure Semantics for Weak Modal Logics: Completeness and Representations
本文为弱模态逻辑引入闭包语义，证明其可靠性与强完备性，并给出与邻域、FMT及克里普克语义间的保真翻译。
A recent strand of research in structural proof theory aims at exploring the notion of analytic calculi (i.e. those calculi that support general and modular proof-strategies for cut elimination), and at identifying classes of logics that can be captured in terms of these calculi. In this context, Wansing introduced the notion of proper display calculi as one possible design framework for proof calculi in which the analiticity desiderata are realized in a particularly transparent way. Recently, the theory of properly displayable logics (i.e. those logics that can be equivalently presented with …
Modal definability in Euclidean modal logics
本文研究欧几里得模态逻辑框架类中模态可定义性问题的可计算性，刻画了哪些欧几里得模态逻辑会导致该问题不可判定。
We know extensions of first order logic by quantifiers of the kind "there are uncountable many ...", "most ..." with new axioms and appropriate semantics. Related are operations such as "set of x, such that ...", Hilbert's $ε$-operator, Churche's $λ$-notation, minimization and similar ones, which also bind a variable within some expression, the meaning of which is however partly defined by a translation into the language of first order logic. In this paper a generalization is presented that comprises arbitrary variable-binding symbols as non-logical operations. The axiomatic extension is deter…
In this work we study the decidability of a class of global modal logics arising from Kripke frames evaluated over certain residuated lattices, known in the literature as modal many-valued logics. We exhibit a large family of these modal logics which are undecidable, in contrast with classical modal logic and propositional logics defined over the same classes of algebras. This family includes the global modal logics arising from Kripke frames evaluated over the standard Lukasiewicz and Product algebras. We later refine the previous result, and prove that global modal Lukasiewicz and Product lo…
Intuitionistic modal logics: a minimal setting
本文提出一种严格包含于IK的直觉主义模态逻辑，作为最小正规直觉主义模态逻辑的候选，并探讨其设定。
Positive modal algebras are the positive-subreducts of modal algebras. We prove that the variety of positive S4-algebras is not locally finite. On the other hand, the free one-generated positive S4-algebra is shown to be finite. Moreover, we describe the bottom part of the lattice of varieties of positive S4-algebras. Building on this, we characterize (passively, hereditarily) structurally complete varieties of positive K4-algebras.
Problems in two axiomatizations of Jaśkowski's discussive (or discursive) logic D2 are considered. A recent axiomatization of D2 and completeness proof relative to D2's intended semantics seems to be mistaken because some formulas valid according to the intended semantics turn out to be unprovable. Although no new axiomatization is offered, nor a repaired completeness proof given, the shortcomings identified here may be a step toward an improved axiomatization.
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。