Various topological concepts are often involved in the research of mathematical logic, and almost all of these concepts can be regarded as developing from the Stone representation theorem. In the Stone representation theorem, a Boolean algebra is represented as the algebra of the clopen sets of a Stone space. And based on this, a natural connection is established between the structure of Stone space and the semantics of propositional logic. In other words, models of a propositional theory are represented as points in a Stone space. This enables us to use the concepts of topology to describe many facts in logic. In this paper, we do the same thing for the first-order logic. That is, we organize the basic objects of semantics of first-order logic, such as theories, models, elementary embeddings, and so on, into a kind of topological structure defined abstractly. To be precise, this kind of structure is a kind of enriched-topological space which we call cylindric space in this paper. Furthermore, based on this topological representation of semantics of first-order logic, we systematically introduce a method of point-set topology into the research of model theory. We demonstrate the great advantages of this topological method with an example and provide a general discussion of its features, advantages, and connection to the type space.
This article aims to present a neighborhood semantic for a modal logic, namely, propositional logic of the plausible. As a subnormal character modal logic, not admits a Kripke semantics. However, the authors show that this neighborhood semantic, reach a relational semantics for propositional logic of the plausible.
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.
In this paper, we present a propositional logic (called mixed logic) containing disjoint copies of minimal, intuitionistic and classical logics. We prove a completeness theorem for this logic with respect to a Kripke semantics. We establish some relations between mixed logic and minimal, intuitionistic and classical logics. We present at the end a sequent calculus version for this logic.
Several authors have recently defined intuitionistic logic based on team semantics (tIPC). In this paper we provide two alternative approaches to intermediate logics in the team semantics setting. We do this by modifying tIPC with axioms written with two different versions of disjunction in the logic, a local one and global one. We prove a characterization theorem in the first approach and we introduce a generalized team semantics in the second one.
We introduce some new logics of imperfect information by adding atomic formulas corresponding to inclusion and exclusion dependencies to the language of first order logic. The properties of these logics and their relationships with other logics of imperfect information are then studied. Furthermore, a game theoretic semantics for these logics is developed. As a corollary of these results, we characterize the expressive power of independence logic, thus answering an open problem posed in (Grädel and Väänänen, 2010).
We introduce and develop a topological semantics of conservativity logics and interpretability logics. We prove the topological compactness theorem of consistent normal extensions of the conservativity logic $\mathbf{CL}$ by extending Shehtman's ultrabouquet construction method to our framework. As a consequence, we prove that several extensions of $\mathbf{CL}$ such as $\mathbf{IL}$, $\mathbf{ILM}$, $\mathbf{ILP}$ and $\mathbf{ILW}$ are strongly complete with respect to our topological semantics.
We introduce proper display calculi for basic monotonic modal logic,the conditional logic CK and a number of their axiomatic extensions. These calculi are sound, complete, conservative and enjoy cut elimination and subformula property. Our proposal applies the multi-type methodology in the design of display calculi, starting from a semantic analysis based on the translation from monotonic modal logic to normal bi-modal logic.
We discuss an ongoing line of research in the relational (non topological) semantics of non-distributive logics. The developments we consider are technically rooted in dual characterization results and insights from unified correspondence theory. However, they also have broader, conceptual ramifications for the intuitive meaning of non-distributive logics, which we explore.
We introduce a new semantical formalism for logics of imperfect information, based on Game Logic (and, in particular, on van Benthem, Ghosh and Lu's Concurrent Dynamic Game Logic). This new kind of semantics combines aspects from game theoretic semantics and from team semantics, and demonstrates how logics of imperfect information can be seen as languages for reasoning about games. Finally we show that, for a very expressive fragment of our language, a simpler semantics is available.
Dynamic Topological Logic ($\mathcal{DTL}$) is a combination of $\mathcal{S}${\em 4}, under its topological interpretation, and the temporal logic $\mathcal{LTL}$ interpreted over the natural numbers. $\mathcal{DTL}$ is used to reason about properties of dynamical systems based on topological spaces. Semantics are given by dynamic topological models, which are tuples $\left <X,\mathcal{T},f,V\right >$, where $\left <X,\mathcal{T}\right >$ is a topological space, $f$ a function on $X$ and $V$ a truth valuation assigning subsets of $X$ to propositional variables.
I show that the logic $\textsf{TJK}^{d+}$, one of the strongest logics currently known to support the naive theory of truth, is obtained from the Kripke semantics for constant domain intuitionistic logic by (i) dropping the requirement that the accessibility relation is reflexive and (ii) only allowing reflexive worlds to serve as counterexamples to logical consequence. In addition, I provide a simplified natural deduction system for $\textsf{TJK}^{d+}$, in which a restricted form of conditional proof is used to establish conditionals.
We obtain modal completeness of the interpretability logics ILP_0 and ILR w.r.t. generalized Veltman semantics. Our proofs are based on the notion of smart (full) labels. We also give shorter proofs of completeness w.r.t. generalized semantics for many classical interpretability logics. We obtain decidability and finite model property w.r.t. generalized semantics for ILP_0 and ILR. Finally, we develop a construction that might be useful for proofs of completeness of extensions of ILW w.r.t. generalized semantics in the future, and demonstrate its usage with ILW* = ILM_0W.
We prove completeness, interpolation and omitting types for certain predicate topological logics that properly extend the first order case. We aslo count the non isomorphic topological models of a countable theory
This paper introduces the logic $QLET_{F}$, a quantified extension of the logic of evidence and truth $LET_{F}$, together with a corresponding sound and complete first-order non-deterministic valuation semantics. $LET_{F}$ is a paraconsistent and paracomplete sentential logic that extends the logic of first-degree entailment ($FDE$) with a classicality operator ${\circ}$ and a non-classicality operator $\bullet$, dual to each other: while ${\circ} A$ entails that $A$ behaves classically, ${\bullet} A$ follows from $A$'s violating some classically valid inferences. The semantics of $QLET_{F}$ c…
We introduce proper display calculi for basic monotonic modal logic, the conditional logic CK and a number of their axiomatic extensions. These calculi are sound, complete, conservative and enjoy cut elimination and subformula property. Our proposal applies the multi-type methodology in the design of proper display calculi, starting from a semantic analysis which motivates syntactic translations from single-type non-normal modal logics to multi-type normal poly-modal logics.
The aim of the paper is to study the topological modal logic of $T_0$ spaces, with the difference modality (for $T_n$, where $n\geq1 $ the corresponding logics were known). We consider propositional modal logic with two modal operators $\square$ and $[\ne]$. $\square$ is interpreted as an interior operator and $[\ne]$ corresponds to the inequality relation. We introduce the logic $S4DT_0$ and show that $S4DT_0$ is the logic of all $T_0$ spaces and has the finite model property.
Büchi and Owen studied algebraic structures called hoops. Hoops provide a natural algebraic semantics for a class of substructural logics that we think of as intuitionistic analogues of the widely studied Łukasiewicz logics. Ben Yaacov extended Łukasiewicz logic to get what is called continuous logic by adding a halving operator. In this paper, we define the notion of continuous hoop, or coop for short, and show that coops provide a natural algebraic semantics for continuous logic. We characterise the simple and subdirectly irreducible coops and investigate the decision problem for various the…
A structural theorem for Kleene algebras is proved, showing that an element of a Kleene algebra can be looked upon as an ordered pair of sets. Further, we show that negation with the Kleene property (called the `Kleene negation') always arises from the set theoretic complement. The corresponding propositional logic is then studied through a 3-valued and rough set semantics. It is also established that Kleene negation can be considered as a modal operator, and enables giving a perp semantics to the logic. One concludes with the observation that all the semantics for this logic are equivalent.
In this article we introduce the variety of monadic BL-algebras as BL-algebras endowed with two monadic operators $\forall$ and $\exists$. After a study of the basic properties of this variety we show that this class is the equivalent algebraic semantics of the monadic fragment of Hájek's basic predicate logic. In addition, we start a systematic study of the main subvarieties of monadic BL-algebras, some of which constitute the algebraic semantics of well-known monadic logics: monadic Gödel logic and monadic Łukasiewicz logic. In the last section we give a complete characterization of totally …
Motivated by questions like: which spatial structures may be characterized by means of modal logic, what is the logic of space, how to encode in modal logic different geometric relations, topological logic provides a framework for studying the confluence of the topological semantics for $\sf S4$ modalities, based on topological spaces rather than Kripke frames. Following research initiated by Sgro, and further pursued algebraically by Georgescu, we prove an interpolation theorem and an omitting types theorem for various extensions of predicate topological logic and Chang's modal logic. Our pro…
In [Ban97] a connection among rough sets (in particular, pre-rough algebras) and three-valued Łukasiewicz logic Ł3 is pointed out. In this paper we present a temporal like semantics for Nilpotent Minimum logic NM ([Fod95, EG01]), in which the logic of every instant is given by Ł3: a completeness theorem will be shown. This is the prosecution of the work initiated in [AGM08] and [ABM09], in which the authors construct a temporal semantics for the many-valued logics of Gödel ([Göd32], [Dum59]) and Basic Logic ([Háj98]).
We study the expressive power of fragments of inclusion and independence logic defined by restricting the number k of universal quantifiers in formulas. Assuming the so-called strict semantics for these logics, we relate these fragments of inclusion and independence logic to sublogics ESO_f(k\forall) of existential second-order logic, which in turn are known to capture the complexity classes NTIME_{RAM}(n^k).
Kripke frames (and models) provide a suitable semantics for sub-classical logics, for example Intuitionistic Logic (of Brouwer and Heyting) axiomatizes the reflexive and transitive Kripke frames (with persistent satisfaction relations), and the Basic Logic (of Visser) axiomatizes transitive Kripke frames (with persistent satisfaction relations). Here, we investigate whether Kripke frames/models could provide a semantics for fuzzy logics. For each axiom of the Basic Fuzzy Logic, necessary and sufficient conditions are sought for Kripke frames/models which satisfy them. It turns out that the onl…
In the first part of this paper we analyzed finite non-deterministic matrix semantics for propositional non-normal modal logics as an alternative to the standard Kripke's possible world semantics. This kind of modal systems characterized by finite non-deterministic matrices was originally proposed by Ju. Ivlev in the 70's. The aim of this second paper is to introduce a formal non-deterministic semantical framework for the quantified versions of some Ivlev-like non-normal modal logics. It will be shown that several well-known controversial issues of quantified modal logics, relative to the iden…
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.
We develop a bottom-up approach to truth-value semantics for classical logic of partial terms based on equality and apply it to prove the conservativity of the addition of partial description and partial selection functions, independently of any strictness assumption.
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…
The present paper provides an analysis of the existing proof systems for dynamic epistemic logic from the viewpoint of proof-theoretic semantics. Dynamic epistemic logic is one of the best known members of a family of logical systems which have been successfully applied to diverse scientific disciplines, but the proof theoretic treatment of which presents many difficulties. After an illustration of the proof-theoretic semantic principles most relevant to the treatment of logical connectives, we turn to illustrating the main features of display calculi, a proof-theoretic paradigm which has been…
We introduce hybrid algebras as algebraic semantics for hybrid languages with nominals and, possibly, the satisfaction operator. We establish a duality between hybrid algebras and the descriptive two-sorted general frames of Ten Cate. We show that all axiomatic extensions of the basic hybrid logics, with or without the satisfaction operator, are complete with respect to their classes of hybrid algebras. Moreover, we show that by adding the usual non-orthodox rules to these logics, they become complete with respect to their classes of permeated hybrid algebras, corresponding to strongly descrip…
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.
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…
We develop a classical propositional logic for reasoning about combinatory logic. We define its syntax, axiomatic system and semantics. The syntax and axiomatic system are presented based on classical propositional logic, with typed combinatory terms as basic propositions, along with the semantics based on applicative structures extended with special elements corresponding to primitive combinators. Both the equational theory of untyped combinatory logic and the proposed axiomatic system are proved to be sound and complete w.r.t. the given semantics. In addition, we prove that combinatory logic…
We examine the relationship between Dependence Logic and game logics. A variant of Dynamic Game Logic, called Transition Logic, is developed, and we show that its relationship with Dependence Logic is comparable to the one between First-Order Logic and Dynamic Game Logic discussed by van Benthem. This suggests a new perspective on the interpretation of Dependence Logic formulas, in terms of assertions about reachability in games of im- perfect information against Nature. We then capitalize on this intuition by developing expressively equivalent variants of Dependence Logic in which this interp…
Dynamic topological logic ($\mathbf{DTL}$) is a trimodal logic designed for reasoning about dynamic topological systems. It was shown by Fernández-Duque that the natural set of axioms for $\mathbf{DTL}$ is incomplete, but he provided a complete axiomatisation in an extended language. In this paper, we consider dynamic topological logic over scattered spaces, which are topological spaces where every nonempty subspace has an isolated point. Scattered spaces appear in the context of computational logic as they provide semantics for provability and enjoy definable fixed points. We exhibit the firs…
This paper introduces a notion of generalised geometric logic. Connections of generalised geometric logic with L-topological system and L-topological space are established.
We study the expressive power of fragments of inclusion logic under the so-called lax team semantics. The fragments are defined either by restricting the number of universal quantifiers or the arity of inclusion atoms in formulae. In case of universal quantifiers, the corresponding hierarchy collapses at the first level. Arity hierarchy is shown to be strict by relating the question to the study of arity hierarchies in fixed point logics.
We study the complexity of predicate logics based on team semantics. We show that the satisfiability problems of two-variable independence logic and inclusion logic are both NEXPTIME-complete. Furthermore, we show that the validity problem of two-variable dependence logic is undecidable, thereby solving an open problem from the team semantics literature. We also briefly analyse the complexity of the Bernays-Schönfinkel-Ramsey prefix classes of dependence logic.
We consider propositional modal logic with two modal operators $\Box$ and $\D$. In topological semantics $\Box$ is interpreted as an interior operator and $\D$ as difference. We show that some important topological properties are expressible in this language. In addition, we present a few logics and proofs of f.m.p. and of completeness theorems.
The logics of formal inconsistency (LFIs, for short) are paraconsistent logics (that is, logics containing contradictory but non-trivial theories) having a consistency connective which allows to recover the ex falso quodlibet principle in a controlled way. The aim of this paper is considering a novel semantical approach to first-order LFIs based on Tarskian structures defined over swap structures, a special class of multialgebras. The proposed semantical framework generalizes previous aproaches to quantified LFIs presented in the literature. The case of QmbC, the simpler quantified LFI expandi…
We introduce a variant of Dependence Logic in which truth is defined not in terms of existence of winning strategies for the Proponent (Eloise) in a semantic game, but in terms of lack of winning strategies for the Opponent (Abelard). We show that this language is a conservative but paraconsistent extension of First Order Logic, that its validity problem can be reduced to that of First Order Logic, that it capable of expressing its own truth and validity predicates, and that it is expressively equivalent to Universal Second Order Logic. Furthermore, we prove that a Paraconsistent Non-dependenc…
University of Luxembourg（卢森堡大学）；Freie Universität Berlin（柏林自由大学）
A shallow semantical embedding of a dyadic deontic logic by Carmo and Jones in classical higher-order logic is presented. This embedding is proven sound and complete, that is, faithful. The work presented here provides the theoretical foundation for the implementation and automation of dyadic deontic logic within off-the-shelf higher-order theorem provers and proof assistants.
We continue work of our earlier paper (Lewitzka and Brunner: Minimally generated abstract logics, Logica Universalis 3(2), 2009), where abstract logics and particularly intuitionistic abstract logics are studied. Abstract logics can be topologized in a direct and natural way. This facilitates a topological study of classes of concrete logics whenever they are given in abstract form. Moreover, such a direct topological approach avoids the often complex algebraic and lattice-theoretic machinery usually applied to represent logics. Motivated by that point of view, we define in this paper the cate…
This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first-order intuitionistic logic with constant domains. It is shown that Fitting's nested calculi naturally arise from their corresponding labelled calculi--for each of the aforementioned logics--via the elimination of structural rules in labelled derivations. The translational correspondence between the two types of systems is leveraged to show that the nested calculi inherit proof-theoretic properties from their associa…
