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 *) Inductive col_hierarchy_bad_1 : Type := | 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)). *)
X -> boolis never going to work. You should use
X -> Propinstead. $\endgroup$
coq-definitiontag makes very little sense to me. $\endgroup$
definitionbecause 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. $\endgroup$