What untyped term inhabits induction on natural numbers in CoC?

cs.stackexchange https://cs.stackexchange.com/questions/111631

Question

Induction on Church-encoded natural numbers (which I will call indNat) can not be defined within the Calculus of Constructions.

If we assumed indNat as an axiom, is there an untyped term that would have the semantics of the induction function? What if we had Scott-encoded natural numbers and fix?

Can induction be inhabited in CoC + fix (such that the function would have the proper semantics, not an infinite loop)?

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top