Join-preserving maps on the discrete time scale $\omega^+$, referred to as time warps, have been proposed as graded modalities that can be used to quantify the growth of information in the course of program execution. The set of time warps forms a simple distributive involutive residuated lattice -- called the time warp algebra -- that is equipped with residual operations relevant to potential applications. In this paper, we show that although the time warp algebra generates a variety that lacks the finite model property, it nevertheless has a decidable equational theory. We also describe an implementation of a procedure for deciding equations in this algebra, written in the OCaml programming language, that makes use of the Z3 theorem prover.

Abstract Necessary and sufficient conditions are presented for the (first-order) theory of a universal class of algebraic structures (algebras) to have a model completion, extending a characterization provided by Wheeler. For varieties of algebras that have equationally definable principal congruences and the compact intersection property, these conditions yield a more elegant characterization obtained (in a slightly more restricted setting) by Ghilardi and Zawadowski. Moreover, it is shown that under certain further assumptions on congruence lattices, the existence of a model completion implies that the variety has equationally definable principal congruences. This result is then used to provide necessary and sufficient conditions for the existence of a model completion for theories of Hamiltonian varieties of pointed residuated lattices, a broad family of varieties that includes lattice-ordered abelian groups and MV-algebras. Notably, if the theory of a Hamiltonian variety of pointed residuated lattices has a model completion, it must have equationally definable principal congruences. In particular, the theories of lattice-ordered abelian groups and MV-algebras do not have a model completion, as first proved by Glass and Pierce, and Lacava, respectively. Finally, it is shown that certain varieties of pointed residuated lattices generated by their linearly ordered members, including lattice-ordered abelian groups and MV-algebras, can be extended with a binary operation to obtain theories that do have a model completion.

A correspondence is established between one-variable fragments of (first-order) intermediate logics defined over a fixed countable linear frame and Gödel modal logics defined over many-valued equivalence relations with values in a closed subset of the real unit interval. It is also shown that each of these logics can be interpreted in the one-variable fragment of the corresponding constant domain intermediate logic, which is equivalent to a Gödel modal logic defined over (crisp) equivalence relations. Although the latter modal logics in general lack the finite model property with respect to their frame semantics, an alternative semantics is defined that has this property and used to establish co-NP-completeness results for the one-variable fragments of the corresponding intermediate logics both with and without constant domains.

This article presents a new method for obtaining small algebras to check the admissibility—equivalently, validity in free algebras—of quasi-identities in a finitely generated quasivariety. Unlike a previous algebraic approach of Metcalfe and Röthlisberger, which is feasible only when the relevant free algebra is not too large, this method exploits natural dualities for quasivarieties to work with structures of smaller cardinality and surjective rather than injective morphisms. A number of case studies are described here that could not be be solved using the algebraic approach, including (quasi)varieties of MS-algebras, double Stone algebras, and involutive Stone algebras.

A many-valued modal logic is introduced that combines the usual Kripke frame semantics of the modal logic K with connectives interpreted locally at worlds by lattice and group operations over the real numbers. A labelled tableau system is provided and a coNEXPTIME upper bound obtained for checking validity in the logic. Focussing on the modal-multiplicative fragment, the labelled tableau system is then used to establish completeness for a sequent calculus that admits cut-elimination and an axiom system that extends the multiplicative fragment of Abelian logic.

Axiomatic bases of admissible rules are obtained for fragments of the substructural logic R-mingle.In particular, it is shown that a "modus-ponens-like" rule introduced by Arnon Avron forms a basis for the admissible rules of its implication and implication-fusion fragments, while a basis for the admissible rules of the full multiplicative fragment requires an additional countably infinite set of rules.Indeed, this latter case provides an example of a three-valued logic with a finitely axiomatizable consequence relation that has no finite basis for its admissible rules.

Petr Cintula, George Metcalfe, Carles Noguera; Special Issue on Mathematical Fuzzy Logic, Journal of Logic and Computation, Volume 21, Issue 5, 1 October 2

An approximate Herbrand theorem is established for first-order infinite-valued Łukasiewicz Logic and used to obtain a proof-theoretic proof of Skolemization. These results are then used to define proof systems in the framework of hypersequents. In particular, a calculus lacking cut elimination is defined for the first-order logic characterized by linearly ordered MV-algebras, a cut-free calculus with an infinitary rule for the full first-order Łukasiewicz Logic, and a cut-free calculus with finitary rules for its one-variable fragment.

George Metcalfe, Constantine Tsinakis; Order, Algebra and Logics, Journal of Logic and Computation, Volume 20, Issue 4, 1 August 2010, Pages 759–760, https

Journal Article Fuzzy Logic Corner Get access Matthias Baaz, Matthias Baaz Search for other works by this author on: Oxford Academic Google Scholar George Metcalfe George Metcalfe Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 19, Issue 2, April 2009, Page 343, https://doi.org/10.1093/logcom/exn053 Published: 18 August 2008

Abstract Substructural fuzzy logics are substructural logics that are complete with respect to algebras whose lattice reduct is the real unit interval [0, 1]. In this paper, we introduce Uninorm logicULas Multiplicative additive intuitionistic linear logicMAILLextended with the prelinearity axiom((A → B) ∧ t) V ((B → A)∧ t). Axiomatic extensions ofULinclude known fuzzy logics such as Monoidalt-norm logicMIXand Gödel logicG, and new weakening-free logics. Algebraic semantics for these logics are provided by subvarieties of (representable) pointed bounded commutative residuated lattices. Gentzen systems admitting cut-elimination are given in the framework of hypersequents. Completeness with respect to algebras with lattice reduct [0, 1] is established forULand several extensions using a two-part strategy. First, completeness is proved for the logic extended with Takeuti and Titani's density rule. A syntactic elimination of the rule is then given using a hypersequent calculus. As an algebraic corollary, it follows that certain varieties of residuated lattices are generated by their members with lattice reduct [0, 1].

Abstract. Comparative logics were introduced by Casari in the 1980s to treat aspects of comparative reasoning occurring in natural language. In this paper Gentzen systems are defined for these logics by means of a special mix rule that combines calculi for various substructural logics with a hypersequent calculus for Meyer and Slaney’s Abelian logic. Cut-elimination is established for all these systems, and as a consequence, a positive answer is given to an open problem on the decidability of the basic comparative logic. 1

We present two embeddings of Łukasiewicz logicŁinto Meyer and Slaney's Abelian logicA, the logic of lattice-ordered Abelian groups. We give new analytic proof systems forAand use the embeddings to derive corresponding systems forŁ. These include hypersequent calculi, terminating hypersequent calculi, co-NP labeled sequent calculi, and unlabeled sequent calculi.