The usual definition of numbers in lambda calculus is closer to what you want; numbers are iterators, which given a zero z and a function f, iterate f some number of times. I played around with defining numbers in lambda calculus plus an iota operator. (iota [p]) returns a term t such that (p t) = true, if such a term exists. (“true” is just λxy.x) This allows us to define negative numbers as the things that inverse-iterate, define imaginary numbers, etc, all in one simple formalism.
iota plus lambda allows for higher-order logic already (∃x.p(x) is just p(ιp); ∃p.px is just [λp(px)](ιλp(px))) so there are definitely questions of consistency. However, it feels like some suitable version of this could be a really pleasing foundation close to what you had in mind.
The usual definition of numbers in lambda calculus is closer to what you want; numbers are iterators, which given a zero z and a function f, iterate f some number of times. I played around with defining numbers in lambda calculus plus an iota operator. (iota [p]) returns a term t such that (p t) = true, if such a term exists. (“true” is just λxy.x) This allows us to define negative numbers as the things that inverse-iterate, define imaginary numbers, etc, all in one simple formalism.
iota plus lambda allows for higher-order logic already (∃x.p(x) is just p(ιp); ∃p.px is just [λp(px)](ιλp(px))) so there are definitely questions of consistency. However, it feels like some suitable version of this could be a really pleasing foundation close to what you had in mind.