An equational metalogic for monadic equational systems

MaRDI QIDQ2855643zbMATH OpenFDO

Authors Marcelo P. Fiore

Publication date 25 October 2013

Published in Theory and Applications of Categories (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1309.4821, http://www.emis.de/journals/TAC/volumes/27/18/27-18abs.html

IPFS File on IPFS (Hint: this is only the Hash - if you get a timeout, this file is not available on our server.)

zbMATH Keywords

soundnessstrong completenessfree algebraequational logicequational presentationstrong monadmonoidal actiondouble dualizationenriched monadenriched universal algebramonadic equational system

Mathematics Subject Classification ID

Equational logic, Mal'tsev conditions (08B05) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Semantics in the theory of computing (68Q55) Enriched categories (over closed or monoidal categories) (18D20)

Abstract: The paper presents algebraic and logical developments. From the algebraic viewpoint, we introduce Monadic Equational Systems as an abstract enriched notion of equational presentation. From the logical viewpoint, we provide Equational Metalogic as a general formal deductive system for the derivability of equational consequences. Relating the two, a canonical model theory for Monadic Equational Systems is given and for it the soundness of Equational Metalogic is established. This development involves a study of clone and double-dualization structures. We also show that in the presence of free algebras the model theory of Monadic Equational Systems satisfies an internal strong-completeness property.

Recommendations

• On equation systems in monotonic models of typed \(\lambda\)-calculus
• Unions of Equational Monadic Theories
• Towards a practical library for monadic equational reasoning in Coq
• Symbolic protocol analysis for monoidal equational theories
• scientific article; zbMATH DE number 522862
• Logical equations in monadic logic
• Monadic EQ-algebras
• Equational theories as congruences of enriched monoids
• A simple abstract semantics for equational theories

Cited in

(9)

• List Objects with Algebraic Structure
• Just do it
• Quotients, inductive types, and quotient inductive types
• Diagrammatic presentations of enriched monads and varieties for a subcategory of arities
• Term equational systems and logics (extended abstract)
• Eilenberg-Moore monoids and backtracking monad transformers
• scientific article; zbMATH DE number 5944670 (Why is no real title available?)
• Equational axiomatization of algebras with structure
• On the mathematical synthesis of equational logics

This page was built for publication: An equational metalogic for monadic equational systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2855643)