Subatomic Natural Deduction for a Naturalistic First-Order Language with Non-Primitive Identity

A first-order language with a defined identity predicate is proposed whose apparatus for atomic predication is sensitive to grammatical categories of natural language (e.g., common nouns, verbs, adjectives, adverbs, modifiers). Subatomic natural deduction systems are defined for this naturalistic first-order language. These systems contain subatomic systems which govern the inferential relations which obtain between naturalistic atomic sentences and between their possibly composite components. As a main result it is shown that normal derivations in the defined systems enjoy the subexpression property which subsumes the subformula property with respect to atomic and identity formulae as a special case. The systems admit a proof-theoretic semantics which does not only apply to logically compound but also to atomic and identity formulae—as well as to their components. The potential of the defined systems for a meticulous first-order analysis of natural inferences whose validity crucially depends on expressions of some of the aforementioned categories is demonstrated.