I have not seen any mention of binary numerals in lambda calculus. Church numerals are unary system. I had asked a question of how to do this in Haskell here: How to implement Binary numbers in Haskell But even after I saw and understood that answer, I could not understand how to do this in pure untyped lambda calculus.
So here is my question: Are binary numerals defined in untyped lambda calculus and have the successor and predecessor functions also been defined for them?
The following paper answers your question. As you can see, there have been investigated several ways to encode binary numerals in lambda calculus.
An Investigation of Compact and Efficient Number Representations in the Pure Lambda Calculus Torben AE. Mogensen http://link.springer.com/content/pdf/10.1007%2F3-540-45575-2_20
Abstract. We argue that a compact right-associated binary number representation gives simpler operators and better efficiency than the left-associated binary number representation proposed by den Hoed and investigated by Goldberg. This representation is then generalised to higher number-bases and it is argued that bases between 3 and 5 can give higher efficiency than binary representation.