Stream: Coq users

Topic: Higher order logic question


view this post on Zulip Cody Roux (May 27 2022 at 22:03):

I had a question for the great people of https://constructive-maths.zulipchat.com, but I think I'll ask here just in case...

I'm struggling with formalizing the normalization for STLC (really system T) in HA2, even on paper! The stumbling block is the definition of the interpretation of types [ ⁣[T] ⁣]SN [\![ T ]\!]\subseteq {\cal SN}.

In Coq I'd do this:

Fixpoint interp (t : type) : term -> Prop :=
    match t with
     | Nat => (* the set of terms that reduce to a numeral *)
     | Arrow t1 t2 => (* the realizability arrow over the interpretation of t1 and t2 *)
    end.

How do I code this with HA2? I'm suspecting "something something Tarski fixed-point theorem", but some clarification would be much appreciated.

Note that my "real" definition is mutually inductive, so any reference that handles that is appreciated (but not required).

view this post on Zulip Pierre-Marie Pédrot (May 27 2022 at 22:10):

AFAIK you can't really define internally a type by large dependent elimination in HA2 (this would require a form of choice) but if you present this intepretation inductively you can define it by the usual impredicative encoding.

view this post on Zulip Pierre-Marie Pédrot (May 27 2022 at 22:12):

That is, you encode instead

Inductive interp : type -> (term -> Prop) -> Prop :=
| nat_interp : interp nat (the set of terms that realize numerals)
| arr_interp : forall σ σi τ τi, interp σ σi -> interp τ τi -> interp (arr σ τ) (Fun σi τi)

view this post on Zulip Pierre-Marie Pédrot (May 27 2022 at 22:13):

Such inductive declarations can be systematically translated into HA2.

view this post on Zulip Cody Roux (May 27 2022 at 22:21):

That mostly makes sense, thanks!

I'm a bit worried about that second argument of interp, though, can you remind me what the encoding is (roughly)?


Last updated: Jan 28 2023 at 07:30 UTC