Presented is a completeness theorem for fuzzy equational logic with truth values in a complete residuated lattice: Given a fuzzy set Σ of identities and an identity p≈q, the degree to which p≈q syntactically follows (is provable) from Σ equals the degree to which p≈q semantically follows from Σ. Pavelka style generalization of well-known Birkhoff's theorem is therefore established.

Hybrid identities are sentences in a special second order language with identity. The model classes of sets of hybrid identities are called hybrid solid varieties. We give a Birkhoff-type-characterization of hybrid solid varieties and develop a hybrid equational logic.

This note presents some new results from [1] about the Suszko operator and truth‐equational logics, following the works of Czelakowski [11] and Raftery [17]. It is proved that the Suszko operator relative to a truth‐equational logic preserves suprema and commutes with endomorphisms. Together with injectivity, proved by Raftery in [17], the Suszko operator relative to a truth‐equational logic is a structural representation, as defined in [15]. Furthermore, if is a quasivariety, then the Suszko operator relative (...) to a truth‐equational logic is continuous. Finally, it is proved that truth is equationally definable in the class if and only if is a ‐algebraic semantics for and the Suszko operator preserves suprema and commutes with substitutions. (shrink)

This paper deals with the algebraization of multi-signature equational logic in the context of the modern theory of categorical abstract algebraic logic. Two are the novelties compared to traditional treatments: First, interpretations between different algebraic types are handled in the object language rather than the metalanguage. Second, rather than constructing the type of the algebraizing class of algebras explicitly in an ad-hoc universal algebraic way, the whole clone is naturally constructed using categorical algebraic techniques.

After an introduction which demonstrates the failure of the equational analogue of Beth?s definability theorem, the first two sections of this paper are devoted to an elementary exposition of a proof that a functional constant is equationally definable in an equational theory iff every model of the set of those consequences of the theory that do not contain the functional constant is uniquely extendible to a model of the theory itself.Sections three, four and five are devoted to applications (...) and extensions of this result.Topics considered here include equational definability in first order logic, an extended notion of definability in equational logic and the synonymy of equational theories.The final two sections briefly review some of the history of equational logic. (shrink)

In this paper we start an investigation of a logic called the logic of algebraic rules. The relation of derivability of this logic is defined on universal closures of special disjunctions of equations extending the relation of derivability of the usual equational logic. The paper contains some simple theorems and examples given in justification for the introduction of our logic. A number of open questions is posed.

We describe which subdirectly irreducible flat algebras arise in the variety generated by an arbitrary class of flat algebras with absorbing bottom element. This is used to give an elementary translation of the universal Horn logic of algebras, and more generally still, partial structures into the equational logic of conventional algebras. A number of examples and corollaries follow. For example, the problem of deciding which finite algebras of some fixed type have a finite basis for their quasi-identities (...) is shown to be equivalent to the finite identity basis problem for the finite members of a finitely based variety with definable principal congruences. (shrink)

We define a new class of Kripke structures for the second-order λ-calculus, and investigate the soundness and completeness of some proof systems for proving inequalities as well as equations. The Kripke structures under consideration are equipped with preorders that correspond to an abstract form of reduction, and they are not necessarily extensional. A novelty of our approach is that we define these structures directly as functors A: → Preor equipped with certain natural transformations corresponding to application and abstraction . We (...) make use of an explicit construction of the exponential of functors in the Cartesian-closed category Preor, and we also define a kind of exponential ΠΦs ε T to take care of type abstraction. However, we strive for simplicity, and we only use very elementary categorical concepts. Consequently, we believe that the models described in this paper are more palatable than abstract categorical models which require much more sophisticated machinery . We obtain soundness and completeness theorems that generalize some results of Mitchell and Moggi to the second-order λ-calculus, and to sets of inequalities. (shrink)

Dijkstra and Scholten have proposed a formalization of classical predicate logic on a novel deductive system as an alternative to Hilbert's style of proof and Gentzen's deductive systems. In this context we call it CED (Calculus of Equational Deduction). This deductive method promotes logical equivalence over implication and shows that there are easy ways to prove predicate formulas without the introduction of hypotheses or metamathematical tools such as the deduction theorem. Moreover, syntactic considerations (in Dijkstra's words, "letting the (...) symbols do the work") have led to the "calculational style," an impressive array of techniques for elegant proof constructions. In this paper, we formalize intuitionistic predicate logic according to CED with similar success. In this system (I-CED), we prove Leibniz's principle for intuitionistic logic and also prove that any (intuitionistic) valid formula of predicate logic can be proved in I-CED. (shrink)

ABSTRACT In this paper it is shown that a broad class of propositional logics can be interpreted in an equational logic based on fork algebras. This interpetability enables us to develop a fork-algebraic formalization of these logics and, as a consequence, to simulate non-classical means of reasoning with equational theories algebras.

We study logical systems for reasoning about equations involving recursive definitions. In particular, we are interested in "propositional" fragments of the functional language of recursion FLR [18, 17], i.e., without the value passing or abstraction allowed in FLR. The "pure," propositional fragment FLR$_0$ turns out to coincide with the iteration theories of [1]. Our main focus here concerns the sharp contrast between the simple class of valid identities and the very complex consequence relation over several natural classes of models.

This paper concerns modal logics of provability — Gödel-Löb systemGL and Solovay logicS — the smallest and the greatest representation of arithmetical theories in propositional logic respectively. We prove that the decision problem for admissibility of rules (with or without parameters) inGL andS is decidable. Then we get a positive solution to Friedman''s problem forGL andS. We also show that A. V. Kuznetsov''s problem of the existence of finite basis for admissible rules forGL andS has a negative solution. Afterwards (...) we give an algorithm deciding the solvability of logical equations inGL andS and constructing some solutions. (shrink)

A signed -equation is an expression of the form t t or t t, where t and t are -terms (for some ranked set ). We characterize those classes of -algebras which are models of a set of signed -equations. Further we consider the problem of finding a complete deductive system analogous to equational logic for the logical consequence operation restricted to signed equations.

Finitely algebraizable deductive systems were introduced by Blok and Pigozzi to capture the essential properties of those deductive systems that are very tightly connected to quasivarieties of universal algebras. They include the equivalential logics of Czelakowski. Based on Blok and Pigozzi’s work, Herrmann defined algebraizable deductive systems. These are the equivalential deductive systems that are also truth-equational, in the sense that the truth predicate of the class of their reduced matrix models is explicitly definable by some set of unary (...) equations. Raftery undertook the task of characterizing the property of truth-equationality for arbitrary deductive systems. In this paper, following Raftery, we extend the notion of truth-equationality for logics formalized as $\pi$-institutions and abstract several of the results that hold for deductive systems in this more general categorical context. (shrink)

Dijkstra and Scholten have proposed a formalization of classical predicate logic on a novel deductive system as an alternative to Hilbert's style of proof and Gentzen's deductive systems. In this context we call it CED . This deductive method promotes logical equivalence over implication and shows that there are easy ways to prove predicate formulas without the introduction of hypotheses or metamathematical tools such as the deduction theorem. Moreover, syntactic considerations have led to the "calculational style," an impressive array (...) of techniques for elegant proof constructions. In this paper, we formalize intuitionistic predicate logic according to CED with similar success. In this system , we prove Leibniz's principle for intuitionistic logic and also prove that any valid formula of predicate logic can be proved in I-CED. (shrink)

We study logical systems for reasoning about equations involving recursive definitions. In particular, we are interested in "propositional" fragments of the functional language of recursion FLR [18, 17], i.e., without the value passing or abstraction allowed in FLR. The "pure," propositional fragment FLR 0 turns out to coincide with the iteration theories of [1]. Our main focus here concerns the sharp contrast between the simple class of valid identities and the very complex consequence relation over several natural classes of models.

In this article, I first analyze and assess the epistemological and semantic status of canonical value-range equations in the formal language of Frege’s Grundgesetze der Arithmetik. I subsequently scrutinize the relation between (a) his informal, metalinguistic stipulation in Grundgesetze I, Section 3, and (b) its formal counterpart, which is Basic Law V. One point I argue for is that the stipulation in Section 3 was designed not only to fix the references of value-range names, but that it was probably also (...) intended to play a regulative role with an eye to Basic Law V. I further intend to shed new light on the status of Frege’s identification of the truth-values with their unit classes in Grundgesetze I, Section 10 and determine its place and importance in his overall logicist project. In a subsequent section, I first discuss the hypothetical extendability of the logical system of Grundgesetze. In what follows, I analyze the incompleteness of that system—were it not inconsistent and hence trivially complete—by focusing on the role of the definite description operator and the axiom governing it (= Basic Law VI) as well as on the role of the application operator. The latter is defined by means of the former. I further comment on the redundancy of an axiom that could be designed to supplement Basic Law VI by incorporating the second clause of Frege’s two-part elucidation of the description operator. I argue that although it seems likely that Basic Law VI could have been shown to be dispensable in Grundgesetze, Frege would probably have been reluctant to dispense with it, despite his commitment to axiomatic parsimony. In my view, the reason is that he considers it essential that every primitive function-name of his formal language be governed and grounded by a basic law that is tailored to the nature and the role of the primitive name occurring at a key point in the law. Toward the end of the article, I propose solutions to two problems with Frege’s use of “=” in the concept-script sentences that result from his definitions involving the replacement of the double stroke of definition with the judgment-stroke. I conclude the article with a summary of the main results that I have achieved. (shrink)

Feature logics are the logical basis for so-called unification grammars studied in computational linguistics. We investigate the expressivity of feature terms with negation and the functional uncertainty construct needed for the description of long-distance dependencies and obtain the following results: satisfiability of feature terms is undecidable, sort equations can be internalized, consistency of sort equations is decidable if there is at least one atom, and consistency of sort equations is undecidable if there is no atom.

This paper introduces an axiomatisation for equational hybrid logic based on previous axiomatizations and natural deduction systems for propositional and first-order hybrid logic. Its soundness and completeness is discussed. This work is part of a broader research project on the development a general proof calculus for hybrid logics.

A logic is said to admit an equational completeness theorem when it can be interpreted into the equational consequence relative to some class of algebras. We characterize logics admitting an equational completeness theorem that are either locally tabular or have some tautology. In particular, it is shown that a protoalgebraic logic admits an equational completeness theorem precisely when it has two distinct logically equivalent formulas. While the problem of determining whether a logic admits (...) an equational completeness theorem is shown to be decidable both for logics presented by a finite set of finite matrices and for locally tabular logics presented by a finite Hilbert calculus, it becomes undecidable for arbitrary logics presented by finite Hilbert calculi. (shrink)

The paper presents generalizations of results on so-called Horn logic, well-known in universal algebra, to the setting of fuzzy logic. The theories we consider consist of formulas which are implications between identities (equations) with premises weighted by truth degrees. We adopt Pavelka style: theories are fuzzy sets of formulas and we consider degrees of provability of formulas from theories. Our basic structure of truth degrees is a complete residuated lattice. We derive a Pavelka-style completeness theorem (degree of provability (...) equals degree of truth) from which we get some particular cases by imposing restrictions on the formulas under consideration. As a particular case, we obtain completeness of fuzzy equational logic. (shrink)