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".
Motivation
Point-free geometry was first formulated in Whitehead (1919, 1920), 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. [See Kneebone (1963), chpt. 13.5, for a gentle introduction to Whitehead's theory. Also see Lucas (2000), chpt. 10.]
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 our understanding of Whitehead's theories. The domain 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. Both sets of axioms have four existential quantifiers.
Inclusion-based point-free geometry
The axioms "G1-G7" are, but for numbering, those of Def. 2.1 in Gerla and Miranda (2008). The identifiers of the form WPn, included in the verbal description of each axiom, refer to the corresponding axiom in Simons (1987: 83).
"Inclusion", denoted by infix "≤", is the fundamental primitive binary relation. (This is the "Parthood" relation that is a standard feature of all mereological theories.) The intuitive meaning of "x"≤"y" is "x" is part of "y"." Assuming that identity, denoted by infix "=", is part of the background logic, the binary relation "Proper Part", denoted by infix "<", is defined as: