2016/09/06 by Christoph Benzmüller, Benzmüller, Christoph, Dana Scott +1
Computer Science · #03B15 #03B35 #03B80 #68T15 #Artificial Intelligence (cs.AI) #Category Theory (math.CT) #F.4 #FOS: Computer and information sciences #FOS: Mathematics #I.2.3 #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.1609.01493
openalex publication_date 2016/09/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Starting from a generalization of the standard axioms for a monoid we present a stepwise development of various, mutually equivalent foundational axiom systems for category theory. Our axiom sets have been formalized in the Isabelle/HOL interactive proof assistant, and this formalization utilizes a semantically correct embedding of free logic in classical higher-order logic. The modeling and formal analysis of our axiom sets has been significantly supported by series of experiments with automated reasoning tools integrated with Isabelle/HOL. We also address the relation of our axiom systems to alternative proposals from the literature, including an axiom set proposed by Freyd and Scedrov for which we reveal a technical issue (when encoded in free logic where free variables range over defined and undefined objects): either all operations, e.g. morphism composition, are total or their axiom system is inconsistent. The repair for this problem is quite straightforward, however.