 It is convenient at this point to introduce some degree of formalization. This avoids ambiguities stemming from ordinary language and facilitates comparisons and developments. For definiteness, we assume here a standard first-order language with identity, supplied with a distinguished binary predicate constant, ‘P’, to be interpreted as the parthood  relation.[6]  Taking the underlying logic to be the classical predicate calculus with  identity,[7]  the requisites on parthood discussed in Section 2.1 may then be regarded as forming a first-order theory characterized by the following proper axioms for ‘P’: