We introduce the general notions of an index and a core of a relation. We postulate a limited form of the axiom of choice -- specifically that all partial equivalence relations have an index -- and explore the consequences of adding the axiom to standard axiom systems for point-free reasoning. Examples of the theorems we prove are that a core/index of a difunction is a bijection, and that the so-called ``all or nothing'' axiom used to facilitate pointwise reasoning is derivable from our axiom of choice.
翻译:本文引入了关系索引与核心的一般概念。我们假设选择公理的一种受限形式——具体而言,即所有部分等价关系都存在索引——并探讨将该公理加入标准无点推理公理系统后产生的推论。我们证明的定理示例包括:双函数的核/索引是双射,以及用于促进逐点推理的所谓"全有或全无"公理可从我们的选择公理推导得出。