Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userNeighbourhood semantics for graded modal logic
125
0
0.0
(
0
)
Ask ChatGPT about the research
No Arabic abstract
We introduce a class of neighbourhood frames for graded modal logic embedding Kripke frames into neighbourhood frames. This class of neighbourhood frames is shown to be first-order definable but not modally definable. We also obtain a new definition of graded bisimulation with respect to Kripke frames by modifying the definition of monotonic bisimulation.
rate research
Read More
Let $alphageq 2$ be any ordinal. We consider the class $mathsf{Drs}_{alpha}$ of relativized diagonal free set algebras of dimension $alpha$. With same technique, we prove several important results concerning this class. Among these results, we prove that almost all free algebras of $mathsf{Drs}_{alpha}$ are atomless, and none of these free algebras contains zero-dimensional elements other than zero and top element. The class $mathsf{Drs}_{alpha}$ corresponds to first order logic, without equality symbol, with $alpha$-many variables and on relativized semantics. Hence, in this variation of first order logic, there is no finitely axiomatizable, complete and consistent theory.
In this paper we provide two new semantics for proofs in the constructive modal logics CK and CD. The first semantics is given by extending the syntax of combinatorial proofs for propositional intuitionistic logic, in which proofs are factorised in a linear fragment (arena net) and a parallel weakening-contraction fragment (skew fibration). In particular we provide an encoding of modal formulas by means of directed graphs (modal arenas), and an encoding of linear proofs as modal arenas equipped with vertex partitions satisfying topological criteria. The second semantics is given by means of winning innocent strategies of a two-player game over modal arenas. This is given by extending the Heijltjes-Hughes-Stra{ss}burger correspondence between intuitionistic combinatorial proofs and winning innocent strategies in a Hyland-Ong arena. Using our first result, we provide a characterisation of winning strategies for games on a modal arena corresponding to proofs with modalities.
Let 2<nleq l<m< omega. Let L_n denote first order logic restricted to the first n variables. We show that the omitting types theorem fails dramatically for the n--variable fragments of first order logic with respect to clique guarded semantics, and for its packed n--variable fragments. Both are modal fragments of L_n. As a sample, we show that if there exists a finite relation algebra with a so--called strong l--blur, and no m--dimensional relational basis, then there exists a countable, atomic and complete L_n theory T and type Gamma, such that Gamma is realizable in every so--called m--square model of T, but any witness isolating Gamma cannot use less than $l$ variables. An $m$--square model M of T gives a form of clique guarded semantics, where the parameter m, measures how locally well behaved M is. Every ordinary model is k--square for any n<k<omega, but the converse is not true. Any model M is omega--square, and the two notions are equivalent if M is countable. Such relation algebras are shown to exist for certain values of l and m like for nleq l<omega and m=omega, and for l=n and mgeq n+3. The case l=n and m=omega gives that the omitting types theorem fails for L_n with respect to (usual) Tarskian semantics: There is an atomic countable L_n theory T for which the single non--principal type consisting of co--atoms cannot be omitted in any model M of T. For n<omega, positive results on omitting types are obained for L_n by imposing extra conditions on the theories and/or the types omitted. Positive and negative results on omitting types are obtained for infinitary variants and extensions of L_{omega, omega}.
Fix 2<n<omega. Let L_n denote first order logic restricted to the first n variables. CA_n denotes the class of cylindric algebras of dimension n and for m>n, Nr_nCA_m(subseteq CA_n) denotes the class of n-neat reducts of CA_ms. The existence of certain finite relation algebras and finite CA_ns lacking relativized complete representations is shown to imply that the omitting types theorem (OTT) fails for L_n with respect to clique guarded semantics (which is an equivalent formalism of its packed fragments), and for the multi-dimensional modal logic S5^n. Several such relation and cylindric algebras are explicitly exhibited using rainbow constructions and Monk-like algebras. Certain CA_n constructed to show non-atom canonicity of the variety SNr_nCA_{n+3} are used to show that Vaughts theorem (VT) for L_{omega, omega}, looked upon as a special case of OTT for L_{omega, omega}, fails almost everywhere (a notion to be defined below) when restricted to L_n. That VT fails everywhere for L_n, which is stronger than failing almost everywhere as the name suggests, is reduced to the existence, for each n<m<omega, of a finite relation algebra R_m having a so-called m-1 strong blur, but R_m has no m-dimensional relational basis. VT for other modal fragments and expansions of L_n, like its guarded fragments, n-products of uni-modal logics like K^n, and first order definable expansions, is approached. It is shown that any multi-modal canonical logic L, such that $K^nsubseteq Lsubseteq S5^n$, L cannot be axiomatized by canonical equations. In particular, L is not Sahlqvist. Elementary generation and di-completeness for L_n and its clique guarded fragments are proved. Positive omitting types theorems are proved for L_n with respect to standard semantics.
We show that numerous distinctive concepts of constructive mathematics arise automatically from an antithesis translation of affine logic into intuitionistic logic via a Chu/Dialectica construction. This includes apartness relations, complemented subsets, anti-subgroups and anti-ideals, strict and non-strict order pairs, cut-valued metrics, and apartness spaces. We also explain the constructive bifurcation of some classical concepts using the choice between multiplicative and additive affine connectives. Affine logic and the antithesis construction thus systematically constructivize classical definitions, handling the resulting bookkeeping automatically.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
