Using recent results in topos theory, two systems of higher-order logic are shown to be complete with respect to sheaf models over topological spaces---so-called ``topological semantics''. The first is classical higher-order logic, with relational quantification of finitely high type; the second system is a predicative fragment thereof with quantification over functions between types, but not over arbitrary relations. The second theorem applies to intuitionistic as well as classical logic.
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 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.
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.
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.
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…
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.
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.
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.
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.
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.
Given a regular cardinal $κ$ such that $κ^{<κ}=κ$ (e.g., if the Generalized Continuum Hypothesis holds), we develop a proof system for classical infinitary logic that includes heterogeneous quantification (i.e., infinite alternate sequences of quantifiers) within the language $\mathcal{L}_{κ^+, κ}$, where there are conjunctions and disjunctions of at most $κ$ any formulas and quantification (including the heterogeneous one) is applied to less than $κ$ many variables. This type of quantification is interpreted in $\mathcal{S}et$ using the usual second-order formulation in terms of strategies fo…
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.
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…
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.
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.
We present a unified categorical treatment of completeness theorems for several classical and intuitionistic infinitary logics with a proposed axiomatization. This provides new completeness theorems and subsumes previous ones by Gödel, Kripke, Beth, Karp, Joyal, Makkai and Fourman/Grayson. As an application we prove, using large cardinals assumptions, the disjunction and existence properties for infinitary intuitionistic first-order logics.
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…
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.
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 $ϕ$.
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…
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.
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…
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.
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 …
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.
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…
We present a streamlined and (hopefully) accessible proof of the model-completeness of the weak monadic second order version of a dense linear order with left-endpoint but no right-endpoint in a particular finite signature. We also show how this can be used to establish model-completeness of the lattice of finite unions of closed intervals of a dense linear order, i.e. the lattice of closed definable subsets in a (densely ordered) o-minimal structure, in a particularly simple signature (comprising binary functions for union and intersection together with two constant symbols and four unary fun…
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.
Institute of Computer Science Czech Academy of Sciences（捷克科学院计算机科学研究所）；The Saul Kripke Center and Philosophy Program The Graduate Center, CUNY（纽约市立大学研究生中心苏尔·克里普克中心与哲学项目）
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…
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.
Provability logic GLP is well-known to be incomplete w.r.t. Kripke semantics. A natural topological semantics of GLP interprets modalities as derivative operators of a polytopological space. Such spaces satisfying all the axioms of GLP are called GLP-spaces. We develop some constructions to build nontrivial GLP-spaces and show that GLP is complete w.r.t. the class of all GLP-spaces.
We investigate a recently-devised polyhedral semantics for intermediate logics, in which formulas are interpreted in n-dimensional polyhedra. An intermediate logic is polyhedrally complete if it is complete with respect to some class of polyhedra. The first main result of this paper is a necessary and sufficient condition for the polyhedral-completeness of a logic. This condition, which we call the Nerve Criterion, is expressed in terms of Alexandrov's notion of the nerve of a poset. It affords a purely combinatorial characterisation of polyhedrally-complete logics. Using the Nerve Criterion w…
We study different representation theorems for various reducts of Heyting polyadic algebras. Superamalgamation is proved for several (natural reducts) and our results are compared to the finitizability problem in classical algebraic logic dealing with cylindric and polyadic (Boolean algebras). We also prove several new neat embedding theorems, and obtain that the class of representable algebras based on (a generalized) Kripke semantics coincide with the class of algebras having the neat embedding property, that is those algebras that are subneat reducts of algebras having $ω$ extra dimensions.
