2025/05/16 by Martı́n Hötzel Escardó, Bruno Da Rocha Paiva, Escardo, Martin H. +5
Computer Science · #03B38 #03B40 #03F50 #F.3.1 #F.3.2 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2505.11055
openalex publication_date 2025/05/16 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The effectful forcing technique allows one to show that the denotation of a closed System T term of type (ι→ ι) → ι in the set-theoretical model is a continuous function (ℕ → ℕ) → ℕ. For this purpose, an alternative dialogue-tree semantics is defined and related to the set-theoretical semantics by a logical relation. In this paper, we apply effectful forcing to show that the dialogue tree of a System T term is itself System T-definable, using the Church encoding of trees.