Interpolation and Amalgamation for Arrays with MaxDiff

In this paper, the theory of McCarthy’s extensional arrays enriched with a maxdiff operation (this operation returns the biggest index where two given arrays differ) is proposed. It is known from the literature that a diff operation is required for the theory of arrays in order to enjoy the Craig interpolation property at the quantifier-free level. However, the diff operation introduced in the literature is merely instrumental to this purpose and has only a purely formal meaning (it is obtained from the Skolemization of the extensionality axiom). Our maxdiff operation significantly increases the level of expressivity; however, obtaining interpolation results for the resulting theory becomes a surprisingly hard task. We obtain such results via a thorough semantic analysis of the models of the theory and of their amalgamation properties. The results are modular with respect to the index theory and it is shown how to convert them into concrete interpolation algorithms via a hierarchical approach.

Algebraic Characterization of the Local Craig Interpolation Property

The sole purpose of this paper is to give an algebraic characterization, in terms of a superamalgamation property, of a local version of Craig interpolation theorem that has been introduced and studied in earlier papers. We continue ongoing research in abstract algebraic logic and use the framework developed by Andréka– Németi and Sain.

Interpolation in Normal Extensions of the Brouwer Logic

The Craig interpolation property and interpolation property for deducibility are considered for special kind of normal extensions of the Brouwer logic.

ANALYTIC CUT AND INTERPOLATION FOR BI-INTUITIONISTIC LOGIC

We prove that certain natural sequent systems for bi-intuitionistic logic have the analytic cut property. In the process we show that the (global) subformula property implies the (local) analytic cut property, thereby demonstrating their equivalence. Applying a version of Maehara technique modified in several ways, we prove that bi-intuitionistic logic enjoys the classical Craig interpolation property and Maximova variable separation property; its Halldén completeness follows.

Von Wright’s truth-logic and around

In this paper von Wright’s truth-logic T__ is considered. It seems that it is a De Morgan four-valued logic DM4 (or Belnap’s four-valued logic) with endomorphism e2. In connection with this many other issues are discussed: twin truth operators, a truth-logic with endomorphism g (or logic Tr), the lattice of extensions of DM4, modal logic V2, Craig interpolation property, von Wright–Segerberg’s tense logic W, and so on.

Representability and amalgamation for Heyting polyadic algebras

We prove that every (not necessarily locally finite) polyadic Heyting algebra of infinite dimension is representable in some concrete sense. We also show that this class has the super amalgamation property. As a byproduct we infer that a certain infinitary extension of predicate intuitionistic logic, or equivalently, the intuitionistic fragment of Keisler’s infinitary logics, is complete and enjoys the Craig interpolation property.