  Even if, as in definitional reflection, we are considering definitional rules for atoms, their defining conditions do not normally decompose these atoms. A proof-theoretic approach that takes the internal structure of atomic sentences into account, has been proposed by Wieckowski (2008; 2011; 2016). He uses introduction and elimination rules for atomic sentences, where these atomic sentences are not just reduced to other atomic sentences, but to subatomic expressions representing the meaning of predicates and individual names. This can be seen as a first step towards natural language applications of proof-theoretic semantics. A further step in this direction has been undertaken by Francez, who developed a proof-theoretic semantics for several fragments of English (see Francez, Dyckhoff, and Ben-Avi, 2010; Francez and Dyckhoff, 2010, Francez and Ben-Avi 2015).