Can you avoid positivity issues with indexing?

Miscellaneous
1

Hi

I was curious if you could do some HOAS nonsense like

Unset Positivity Checking.

Inductive term: nat :=
| lift {n}: term (S n) -> term n

| tt {n}: term n
| fanout {n} (_ _: term n): term n
| fst {n}: term n -> term n
| snd {n}: term n -> term n

| lam {n} (term n -> term n): term (S n)
| app {n} (_ _: term n): term n.

Set Positivity Checking.

I don’t really get Curry’s paradox though.

2

I m not sure Curry’s paradox would help here, but Russell’s paradox certainly applies. By composing, lift and lam, you get an injective function from term n -> term n to term n. And since term n contains at least two elements (e.g., tt and fst tt), you have an inconsistency on the cardinal.

3 Likes