# Coq defining a hierarchy of collections of integers with infinitely many "levels"

I'm trying to formalize a small part of higher-order arithmetic in Coq as an exercise (Wikipedia article for second-order arithmetic).

It's straightforward to formalize something resembling second-order arithmetic or something resembling higher-order arithmetic in Coq if there are a fixed number of possible levels.

I'm curious if there's a way to define such a notion, though, for an infinite number of levels.

Require Import BinNums.

Definition col (X : Type) : Type := X -> bool.

(* This is bad because it only goes up to 2 levels *)
| catom : N -> col_hierarchy_bad_1
| ccol1 : (col N) -> col_hierarchy_bad_1
| ccol2 : (col (col N)) -> col_hierarchy_bad_1.

(* This attempt doesn't even compile. I'm trying to decorate "col_hierarchy"
with the kind of thing it contains and then later figure out how to stitch
the different col_hierarchies together into a single type. *)
(*
Inductive col_hierarchy_bad_2 (contents : Type) : Type :=
| catom : N -> col_hierarchy_bad_2 N
| ccol : forall T : Type, (col_hierarchy_bad_2 T -> col_hierarchy_bad_2 (col T)).
*)

• Slightly off-topic, but except if you are adding a strong variant of the excluded middle axiom, representing predicates on X as functions X -> bool is never going to work. You should use X -> Prop instead. Mar 7, 2022 at 7:07
• The coq-definition tag makes very little sense to me. Mar 8, 2022 at 17:27
• Gregory, could you please react to Bubbler's answer. Is that what you're looking for? If not, please clarify. Mar 8, 2022 at 17:28
• I accepted the answer now (and also upvoted it before). It was exactly what I was looking for. Sorry, I thought that did not require an explicit message. I originally used the tag definition because the question is about how to define a concept expressed informally, rather than how to prove something. I can remove the tag if it doesn't make sense. Mar 8, 2022 at 18:25

A simple way is to define the type in terms of the Peano natural numbers nat.

Require Import BinNums Arith.

Definition col (X : Type) : Type := X -> bool.

Fixpoint col_repeat (n : nat) (X : Type) : Type :=
match n with
| O => X
| S n => col (col_repeat n X)
end.

Inductive col_hierarchy : Type :=
| ccoln (n : nat) : col_repeat n N -> col_hierarchy.


This way, ccoln 0 corresponds to your catom, ccoln 1 to ccol1, and so on, and ccoln n is defined for every natural number n.

Your definition is awkward because of strict positivity requirements in inductive datatypes.

Your definition of col is really a decidable subset and there exists an alternative strictly positive encoding of subsets in terms of the image of a function.

Inductive hierarchy: nat -> Type :=
| catom: N -> hierarchy 0
| cimage {n} (X: Set): (X -> hierarchy n) -> hierarchy (S n).


The decidable hierarchy consists of

Fixpoint decidable {n} (h: hierarchy) : Type :=
match h with
| catom _ => unit
| cimage X P => (forall y. {exists x. P x = y} + {~exists x. P x = y}) * forall x. decidable (P x)
end.


A little mucky but I thought it was worth mentioning. The image strictly positive encoding trick is often useful for some constructions.