Whitehead's point-free geometry

[2] Whitehead did not set out his theories in a manner that would satisfy present-day canons of formality.

No axiom requires more than three quantified variables; hence a translation of first-order theories into relation algebra is possible.

Assuming that equality, denoted by the infix operator "=", is part of the background logic, the binary relation Proper Part, denoted by the infix operator "<", is defined as: The axioms are:[3] A model of G1–G7 is an inclusion space.

For example, if the inclusion space is the Euclidean plane, then the corresponding abstractive classes are points and lines.

[8] Hence inclusion-based point-free geometry would be a proper extension of D (namely D ∪ {G4, G6, G7}), were it not that the D relation "≤" is a total order.

[10] C is a proper fragment of the theories proposed by Clarke,[11] who noted their mereological character.

C has one primitive relation, binary "connection," denoted by the prefixed predicate letter C. That x is included in y can now be defined as x ≤ y ↔ ∀z[Czx→Czy].

Hence C extends the atomless variant of SMT by means of the axioms C5 and C6, suggested by chapter 2 of part 4 of Process and Reality.