The Index and Core of a Relation. With Applications to the Axiomatics of Relation Algebra

TL;DR

This paper introduces the concepts of index and core of a relation, explores their properties under a limited axiom of choice, and demonstrates their implications in relation algebra and point-free reasoning.

Contribution

It defines the notions of index and core for relations, and shows how a limited axiom of choice influences relation algebra theorems.

Findings

A core/index of a difunction is a bijection.

The 'all or nothing' axiom is derivable from the axiom of choice.

Adding the axiom affects standard point-free reasoning systems.

Abstract

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.