Axiomatizing Category Theory in Free Logic
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Generalized Categorization Axioms
Categorization axioms have been proposed to axiomatizing clustering results, which offers a hint of bridging the difference between human recognition system and machine learning through an intuitive observation: an objec…
BIG-bench Machine LearningClusteringDensity EstimationDimensionality ReductionKnowing Whether
Knowing whether a proposition is true means knowing that it is true or knowing that it is false. In this paper, we study logics with a modal operator Kw for knowing whether but without a modal operator K for knowing that…
Axiomatizing consciousness, with applications
Consciousness will be introduced axiomatically, inspired by Buddhist insight meditation and psychology, logic in computer science, and cognitive neuroscience, as consisting of a stream of $configurations$ that is $compou…
The Institutional Approach
This chapter discusses the institutional approach for organizing and maintaining ontologies. The theory of institutions was named and initially developed by Joseph Goguen and Rod Burstall. This theory, a metatheory based…
Mathematical Morphology via Category Theory
Mathematical morphology contributes many profitable tools to image processing area. Some of these methods considered to be basic but the most important fundamental of data processing in many various applications. In this…