On the Multicategorical Meta-Theorem and the Completeness of Restricted Algebraic Deduction Systems

TL;DR

This paper establishes categorical soundness and completeness theorems for algebraic theories, demonstrating how properties of models transfer from sets to multicategories, and introduces a semantic framework for equational deduction systems.

Contribution

It introduces a multicategorical meta-theorem that transfers model properties from sets to multicategories and constructs a semantic framework for context-structured deduction systems.

Findings

Six of eight deduction systems are complete within the category of sets.

A bijective correspondence between context structures and structure categories is established.

Each modelable context structure has a corresponding soundness and completeness theorem.

Abstract

Eight categorical soundness and completeness theorems are established within the framework of algebraic theories. Exactly six of the eight deduction systems exhibit complete semantics within the cartesian monoidal category of sets. The multicategorical meta-theorem via soundness and completeness enables the transference of properties of families of models from the cartesian monoidal category of sets to $\Delta$-multicategories $C$. A bijective correspondence $R \mapsto \Delta_R$ is made between context structures $R$ and structure categories $\Delta$, which are wide subcategories of $\textbf{FinOrd}$ consisting of finite ordinals and functions. Given a multisorted signature $\sigma$ with a context structure $R$, an equational deduction system $\vdash_R$ is constructed for $R$-theories. The models within $\Delta_R$-multicategories provide a natural semantic framework for the deduction system $\vdash_R$ for modelable context structures $R$. Each of the eight modelable context structures $R$ is linked with a soundness and completeness theorem for the deduction system $\vdash_R$.