solidot新版网站常见问题,请点击这里查看。
消息
本文已被查看7012次
Axiomatizing Category Theory in Free Logic. (arXiv:1609.01493v5 [cs.LO] UPDATED)
来源于:arXiv
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. 查看全文>>