For a long while the pioneers of contemporary symbolic logic concentrated their research on formal reasonings whose only logical constants were the traditional connectives "if… then", "and", "not", "or" and the quantifiers. These are, furthermore, the only notions which are required to analyse a mathematical proof, with the proviso that the "∈" of set theory is added to the list of constants.