This paper presents several extensions of order-sorted logic based on the notion of property classification in formal ontology. The refined order-sorted language contains types (as rigid sorts), anti-rigid sorts, and unary predicates in order to distinctly express the following properties: substantial sorts, non-substantial sorts, and non-sortal properties. For many separated knowledge bases constructed using the logic, we propose an enriched reasoning mechanism such that each independent knowledge base can extract rigid property information from other knowledge bases (called rigid property derivation). Additionally, we classify (i) anti-rigid properties on the basis of their dependences on time, situation, and belief and (ii) non-sortal properties on the basis of the countability of the elements of the properties.