Explore the vast range of titles available.

A definition and some inaccurate cross-references in the paper A Survey of Abstract Algebraic Logic, which might confuse some readers, are clarified and corrected; a short discussion of the main one is included. We also update a dozen of bibliographic references.

A deductive system S (in the sense of Tarski) is Fregean if the relation of interderivability, relative to any given theory T, i.e., the binary relation between formulas$\\{\\langle \\alpha,\\beta \\rangle \\colon T,\\alpha \\vdash s\\beta \\ \\text{and}\\ T,\\beta \\vdash s\\alpha \\}$, is a congruence relation on the formula algebra. The multiterm deduction-detachment theorem is a natural generalization of the deduction theorem of the classical and intuitionistic propositional calculi (IPC) in which a finite system of possibly compound formulas collectively plays the role of the implication connective of IPC. We investigate the deductive structure of Fregean deductive systems with the multiterm deduction-detachment theorem within the framework of abstract algebraic logic. It is shown that each deductive system of this kind has a deductive structure very close to that of the implicational fragment of IPC. Moreover, it is algebraizable and the algebraic structure of its equivalent quasivariety is very close to that of the variety of Hilbert algebras. The equivalent quasivariety is however not in general a variety. This gives an example of a relatively point-regular, congruence-orderable, and congruence-distributive quasivariety that fails to be a variety, and provides what apparently is the first evidence of a significant difference between the multiterm deduction-detachment theorem and the more familiar form of the theorem where there is a single implication connective.

Object-oriented (OO) programming techniques can be applied to equational specification logics by distinguishing visible data from hidden data (that is, by distinguishing the output of methods from the objects to which the methods apply), and then focusing on the behavioural equivalence of hidden data in the sense introduced by H. Reichel in 1984. Equational specification logics structured in this way are called hidden equational logics, HELs. The central problem is how to extend the specification of a given HEL to a specification of behavioural equivalence in a computationally effective way. S. Buss and G. Roşu showed in 2000 that this is not possible in general, but much work has been done on the partial specification of behavioural equivalence for a wide class of HELs. The OO connection suggests the use of coalgebraic methods, and J. Goguen and his collaborators have developed coinductive processes that depend on an appropriate choice of a cobasis, which is a special set of contexts that generates a subset of the behavioural equivalence relation. In this paper the theoretical aspects of coinduction are investigated, specifically its role as a supplement to standard equational logic for determining behavioural equivalence. Various forms of coinduction are explored. A simple characterisation is given of those HELs that are behaviourally specifiable. Those sets of conditional equations that constitute a complete, finite cobasis for a HEL are characterised in terms of the HEL's specification. Behavioural equivalence, in the form of logical equivalence, is also an important concept for single-sorted logics, for example, sentential logics such as the classical propositional logic. The paper is an application of the methods developed through the extensive work that has been done in this area on HELs, and to a broader class of logics that encompasses both sentential logics and HELs.

In this paper we consider the structure of the class FGModS of full generalized models of a deductive system S from a universal-algebraic point of view, and the structure of the set of all the full generalized models of S on a fixed algebra A from the lattice-theoretical point of view; this set is represented by the lattice${\\bf FACS}_{s}A$of all algebraic closed-set systems$\\scr{C}$on A such that$\\langle A,\\scr{C}\\rangle \\in {\\bf FGMod}S$. We relate some properties of these structures with tipically logical properties of the sentential logic S. The main algebraic properties we consider are the closure of FGModS under substructures and under reduced products, and the property that for any A the lattice${\\bf FACS}_{s}A$is a complete sublattice of the lattice of all algebraic closed-set systems over A. The logical properties are the existence of a fully adequate Gentzen system for S, the Local Deduction Theorem and the Deduction Theorem for S. Some of the results are established for arbitrary deductive systems, while some are found to hold only for deductive systems in more restricted classes like the protoalgebraic or the weakly algebraizable ones. The paper ends with a section on examples and counterexamples.

An equality-test algebra has a two-element Boolean sort and an equality-test operation $eq_s $ for each non-Boolean sort $s$, where $eq_s (x,y)$ equals TRUE if $x = y$ and FALSE otherwise. An if-then-else algebra is an equality-test algebra with the if-then-else operations $[\\_,\\_,\\_]_s $ adjoined: $[b,x,y]_s $ equals $x$ if $b = \\text{TRUE}$ and $y$ if $b = \\text{FALSE}$. A finite set of axioms for the conditional-equational (i.e., quasi-equational) theory of equality-test algebras is given. A finite axiomatization of the equational theory of if-then-else algebras is also given, and it is shown that this also serves as a basis for the conditional-equational theory of if-then-else algebras. Finite bases for the equational theories of several classes of algebras closely related to if-then-else algebras were previously known. The power of conditional and equational specifications of equality-test and if-then-else data types are investigated, and the following results, among others, are obtained. (i) Every equality-test data type that can be specified in either the initial or final algebra sense by a finite set of universal first-order sentences can be completely specified (i.e., in both the initial and final algebra senses simultaneously) by a finite set of conditional equations. (ii) The same as (i) but with \"equality-test\" and \"conditional equations\" replaced, respectively, by \"if-then-else\" and \"equations.\" (iii) An arbitrary data type that can be specified in the initial algebra sense by a finite set of universal sentences can be specified in the same sense by a finite set of conditional equations with the equality-test operations as hidden operations. (iv) The same as (iii) but with \"conditional equations\" replaced by \"equations,\" and the if-then-else operations adjoined as additional hidden operations; this holds however only under the additional hypothesis that the original specification is complete.