Experts often disagree about the organization of biological taxa. The shifting definitions of taxonomic names complicate otherwise simple queries concerning these taxa. For example, a query such as “how many occurrences of specimens in genus G are recorded in database D” will return different answers depending on whose definition of genus G is used. In our proposed framework, taxonomic classifications of multiple experts are captured using first-order logic (FOL). Specifically, taxonomies, and relationships between them, are viewed as sets of first-order formulas, constraining the possible interpretations of names and concepts in the taxonomies. The formalization of taxonomies and the relationships between them via our FOL language Ltax allows us to clarify (a) what it means for a taxonomy to be consistent, (b) to be inconsistent, (c) whether a new relationship between two taxa (e.g., a congruence A ≡ B) is implied, thus “filling logic gaps”, and (d) whether two taxo...