Tangentially related to this old post: Why dependent type theory?

It is well-known that SN for impredicative System F requires an impredicative metalanguage, but I started to wonder if SN for impredicative System Fω (impredicativity + type-level computation) additionally requires dependent products from the metatheory.

I recently finished a SN proof for System F Omega by simplifying the SN proof for CoC found in Coq in Coq.

In my proof, I used dependent functions to assign meaning to types (details given below) and I couldn’t find an alternative that does not require dependent functions. The need for dependent functions seems to be caused by the combination of impredicativity and type-level computation since I can model a predicative dependently typed language with large elimination or impredicative System F without the use of dependent types (or to be more pedantic, the use of dependent types in Coq for those proofs is limited to `Prop`

, whose definitions are always sealed with a QeD).

I wonder if SN for System F Omega is an instance of problems that aren’t provable in proof assistants such as HOL/Isabelle which lack dependent types. If not, what would be a way to get rid of the use of dependent types?

Here’s a quick explanation of where dependent types are used in my model. More details can be found in the references I linked in my repository.

Kinds (⋆, ⋆ → ⋆, etc.) are interpreted as the following type signatures from Coq:

```
V(⋆) = Term → Prop
V(κ0 → κ1) = V(κ0) → V(κ1)
```

The interpretation of types is then a dependent function that takes a well-formedness proof of a type with kind κ and returns something of type V(⋆).

```
T : ∀ Δ ⊢ τ : k, V(κ)
```

The interpretation of types maps type-level lambdas to Coq functions. For example, the type-level identity `Λ α . α`

gets mapped to the Coq identity function `fun (s : Term -> Prop) => s`

.

In predicative systems, I can get away with this type of embedding of object functions to meta functions by closing my interpretation of types over reduction. `(λ x . x) nat`

has the same meaning as `nat`

because `(λ x . x) nat ⇒ nat`

, and I don’t need to assign meanings directly to the type constructor `(λ x . x)`

. I was unable to adapt this approach to F Omega and I can’t exactly pinpoint why.