In mathematics, point-free geometry is a geometry whose primitive ontological notion is region rather than point. Two axiomatic systems are set out below, one grounded in mereology, the other in mereotopology and known as connection theory.
Point-free geometry was first formulated by Alfred North Whitehead,[1] not as a theory of geometry or of spacetime, but of "events" and of an "extension relation" between events. Whitehead's purposes were as much philosophical as scientific and mathematical.[2]
Whitehead did not set out his theories in a manner that would satisfy present-day canons of formality. The two formal first-order theories described in this entry were devised by others in order to clarify and refine Whitehead's theories. The domain of discourse for both theories consists of "regions." All unquantified variables in this entry should be taken as tacitly universally quantified; hence all axioms should be taken as universal closures. No axiom requires more than three quantified variables; hence a translation of first-order theories into relation algebra is possible. Each set of axioms has but four existential quantifiers.
The fundamental primitive binary relation is inclusion, denoted by the infix operator "≤", which corresponds to the binary Parthood relation that is a standard feature in mereological theories. The intuitive meaning of x ≤ y is "x is part of y." 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:
x<y\leftrightarrow(x\ley\landx\not=y).
The axioms are:[3]
G1.
x\lex.
G2.
(x\lez\landz\ley) → x\ley.
G3.
(x\ley\landy\lex) → x=y.
G4.
\existsz[x\lez\landy\lez].
G5.
x<y → \existsz[x<z<y].
G6.
\existsy\existsz[y<x\landx<z].
G7.
\forallz[z<x → z<y] → x\ley.
A model of G1–G7 is an inclusion space.
Definition.[4] Given some inclusion space S, an abstractive class is a class G of regions such that S\G is totally ordered by inclusion. Moreover, there does not exist a region included in all of the regions included in G.
Intuitively, an abstractive class defines a geometrical entity whose dimensionality is less than that of the inclusion space. For example, if the inclusion space is the Euclidean plane, then the corresponding abstractive classes are points and lines.
Inclusion-based point-free geometry (henceforth "point-free geometry") is essentially an axiomatization of Simons's system W.[5] In turn, W formalizes a theory of Whitehead[6] whose axioms are not made explicit. Point-free geometry is W with this defect repaired. Simons did not repair this defect, instead proposing in a footnote that the reader do so as an exercise. The primitive relation of W is Proper Part, a strict partial order. The theory[7] of Whitehead (1919) has a single primitive binary relation K defined as xKy ↔ y < x. Hence K is the converse of Proper Part. Simons's WP1 asserts that Proper Part is irreflexive and so corresponds to G1. G3 establishes that inclusion, unlike Proper Part, is antisymmetric.
Point-free geometry is closely related to a dense linear order D, whose axioms are G1-3, G5, and the totality axiom
x\ley\lory\lex.
A different approach was proposed in Whitehead (1929), one inspired by De Laguna (1922). Whitehead took as primitive the topological notion of "contact" between two regions, resulting in a primitive "connection relation" between events. Connection theory C is a first-order theory that distills the first 12 of Whitehead's 31 assumptions[9] into 6 axioms, C1-C6.[10] C is a proper fragment of the theories proposed by Clarke,[11] who noted their mereological character. Theories that, like C, feature both inclusion and topological primitives, are called mereotopologies.
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'']. Unlike the case with inclusion spaces, connection theory enables defining "non-tangential" inclusion,[12] a total order that enables the construction of abstractive classes. Gerla and Miranda (2008) argue that only thus can mereotopology unambiguously define a point.
C1.
Cxx.
C2.
Cxy → Cyx.
C3.
\forallz[Czx\leftrightarrowCzy] → x=y.
C4.
\existsy[y<x].
C5.
\existsz[Czx\landCzy].
C6.
\existsy\existsz[(y\lex)\land(z\lex)\land\negCyz].
A model of C is a connection space.
Following the verbal description of each axiom is the identifier of the corresponding axiom in Casati and Varzi (1999). Their system SMT (strong mereotopology) consists of C1-C3, and is essentially due to Clarke (1981).[13] Any mereotopology can be made atomless by invoking C4, without risking paradox or triviality. 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.[14]
Biacino and Gerla (1991) showed that every model of Clarke's theory is a Boolean algebra, and models of such algebras cannot distinguish connection from overlap. It is doubtful whether either fact is faithful to Whitehead's intent.