 From Frege’s Theorem, one can derive arithmetic. It is an immediate consequence Theorem 5 and the fact that Predecessor is a functional relation that every number has a unique successor. That means we can define the successor function by adding definite descriptions of the form ‘the \(x\) such that \(\phi\)’ to our language: