On the Sets Inhabited by Numbers 1
Andrzej Trybulec · 2003
Summary. The information that all members of a set enjoy a property expressed by an adjective can be processed in a systematic way. The purpose of the work is to find out how to do that. If it works, ‘membered ’ will become a reserved word and the work with it will be automated. I have chosen membered rather than inhabited because of the compatibility with the Automath terminology. The phrase τ inhabits θ could be translated to τ is θ in Mizar.