The following section is pure speculation on my part, but I feel compelled to share it on the math stackexchange. I used tags on this question to draw in experts, not to imply any knowledge I have in these areas.
In set theory, understanding the definition of transitive closure involves the acceptance of an underlying construction that can involve an infinite number of recursive steps. It is also of interest that finite sets can be defined by
Definition: A set $X$ is said to be finite if there exists a binary relation $\rho$ on $X$ satisfying the following two properties:
$\tag 1 \rho \text{ is a bijective correspondence on }X$ $\tag 2 \text{The transitive closure of } \rho \text{ is equal to } X \times X$
But with a 'stripped down' set theory that a machine can work with, the transitive closure can be 'programmed' as an axiom:
AoTC: Given a binary relation $R$ on a set X there exists a binary relation $\hat R$ satisfying the following two properties,
$\;$ The relation $\hat R$ is transitive and $R \subset \hat R$.
$\;$ If $T$ is a transitive relation and $R \subset T$ then $\hat R \subset T$.
Have axioms every been 'designed' for use by a computing operating system?
I came up with this after thinking about Noah's comment in an attempt to actualize (physicality is the motivation) the specific AoTC axiom I used in my question.
Here I am going to sketch a $\text{2 by 2 TC chip}$ design.
Inputs: $4$ on/off Pins, so $2^4$ signals, one for each vertex in the $\text{2 by 2 TC chip}$.
Black Box: Take the transitive closure of the the vertices that are turned on by the input pins.
Outputs: $2$ on/off Pins:
$\quad$ Pin 1: On if any vertex in on.
$\quad$ Pin 2: On if any vertex on the diagonal is on.
This chip can handle the logical binary operations of conjunction, disjunction, and XOR.
This is a fun imagination puzzle to work on and I don't want to spoil that by putting up all the details.