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.