church numeral and successor/predecessor functions
That's dope. I figured out (on paper) several extensions to PA to increasingly construct the rationals, and then the algebraic and complex numbers. It started with dropping the least-element axiom and adding a predecessor function to build the negative numbers. If this is translated to church numerals, we can have the whole of arithmetic built up from pure λ-terms.
The system developed into a rotation group where the "imaginary" unit together with multiplication were the fundamental entities. It can be extended with addition to represent an arbitrary complex number. The system can be generalized to a sort of Clifford algebra.
I wonder if such an algebra can be implemented with pure λ-terms, in such a way that multiplication is encoded by λ-application. So if ι and κ are both objects of the system, another element of the system can be yielded by the expression (ι κ). Furthermore,if the group is cyclic, could there be a term Κ such that ιΚ = ι? For example, could there be a λ-term that applied to itself 3 times yields itself? This in analogy to how powers of the "imaginary" unit i yield: i, -1, -i, 1, i ...
Can this be extended to clifford (aka geometric) algebras? Where we have(say) a set of primitives e1, e2, e3, where you can construct a 'blade' e1*e2, e1*e2*e3, but certain combinations such as e1*e1=0 and e1*e2*e3*e1=0 and so on.
I got stuck with this question, maybe you have an idea as to how this could be done?