This paper develops a general methodology to connect propositional and first-order interpolation. In fact, the existence of suitable skolemizations and of Herbrand expansions together with a propositional interpolant suffice to construct a first-order interpolant. This methodology is realized for lattice-based finitely-valued logics, the top element representing true. It is shown that interpolation is decidable for these logics.
We introduce and investigate the notion of uniform Lyndon interpolation property (ULIP) which is a strengthening of both uniform interpolation property and Lyndon interpolation property. We prove several propositional modal logics including ${\bf K}$, ${\bf KB}$, ${\bf GL}$ and ${\bf Grz}$ enjoy ULIP. Our proofs are modifications of Visser's proofs of uniform interpolation property using layered bisimulations. Also we give a new upper bound on the complexity of uniform interpolants for ${\bf GL}$ and ${\bf Grz}$.
In this paper, we study several propositional team logics that are closed under unions, including propositional inclusion logic. We prove that all these logics are expressively complete, and we introduce sound and complete systems of natural deduction for these logics. We also discuss the locality property and its connection with interpolation in these logics.
Analogues of Scott's isomorphism theorem, Karp's theorem as well as results on lack of compactness and strong completeness are established for infinitary propositional relevant logics. An "interpolation theorem" (of a particular sort introduced by Barwise and van Benthem) for the infinitary quantificational boolean logic $L_{\infty ω}$ holds. This yields a preservation result characterizing the expressive power of infinitary relevant languages with absurdity using the model-theoretic relation of relevant directed bisimulation as well as a Beth definability property.
We develop a Gentzen-style proof theory for super-Belnap logics (extensions of the four-valued Dunn-Belnap logic), expanding on an approach initiated by Pynko. We show that just like substructural logics may be understood proof-theoretically as logics which relax the structural rules of classical logic but keep its logical rules as well as the rules of Identity and Cut, super-Belnap logics may be seen as logics which relax Identity and Cut but keep the logical rules as well as the structural rules of classical logic. A generalization of the cut elimination theorem for classical propositional l…
We consider the propositional logic equipped with Chellas stit operators for a finite set of individual agents plus the historical necessity modality. We settle the question of whether such a logic enjoys restricted interpolation property, which requires the existence of an interpolant only in cases where the consequence contains no Chellas stit operators occurring in the premise. We show that if action operators count as logical symbols, then such a logic has restricted interpolation property iff the number of agents does not exceed three. On the other hand, if action operators are considered…
We prove that the sequent calculus $\mathsf{L_{RBL}}$ for residuated basic logic $\mathsf{RBL}$ has strong finite model property, and that intuitionistic logic can be embedded into basic propositional logic $\mathsf{BPL}$. Thus $\mathsf{RBL}$ is decidable. Moreover, it follows that the class of residuated basic algebras has the finite embeddability property, and that $\mathsf{BPL}$ is PSPACE-complete, and that intuitionistic logic can be embedded into the modal logic $\mathsf{K4}$.
In this paper we show that the intuitionistic monotone modal logic $\mathsf{iM}$ has the uniform Lyndon interpolation property (ULIP). The logic $\mathsf{iM}$ is a non-normal modal logic on an intuitionistic basis, and the property ULIP is a strengthening of interpolation in which the interpolant depends only on the premise or the conclusion of an implication, respecting the polarities of the propositional variables. Our method to prove ULIP yields explicit uniform interpolants and makes use of a terminating sequent calculus for $\mathsf{iM}$ that we have developed for this purpose. As far as …
In the present paper we consider modal propositional logic and look for the constraints that are imposed to the propositions of the special type $\Box a$ by the structure of the relevant finite Kripke frame. We translate the usual language of modal propositional logic in terms of notions of commutative algebra, namely polynomial rings, ideals, and bases of ideals. We use extensively the perspective obtained in previous works in Algebraic Statistics. We prove that the constraints on $\Box a$ can be derived through a binomial ideal containing a toric ideal and we give sufficient conditions under…
In this paper the 3-valued paraconsistent first-order logic QCiore is studied from the point of view of Model Theory. The semantics for QCiore is given by partial structures, which are first-order structures in which each n-ary predicate R is interpreted as a triple of paiwise disjoint sets of n-uples representing, respectively, the set of tuples which actually belong to R, the set of tuples which actually do not belong to R, and the set of tuples whose status is dubious or contradictory. Partial structures were proposed in 1986 by I. Mikenberg, N. da Costa and R. Chuaqui for the theory of qua…
