Document

# A Reflection Principle for Potential Infinite Models of Type Theory

## File

LIPIcs.TYPES.2023.6.pdf
• Filesize: 0.77 MB
• 20 pages

## Cite As

Matthias Eberl. A Reflection Principle for Potential Infinite Models of Type Theory. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.TYPES.2023.6

## Abstract

Denotational models of type theory, such as set-theoretic, domain-theoretic, or category-theoretic models use (actual) infinite sets of objects in one way or another. The potential infinite, seen as an extensible finite, requires a dynamic understanding of the infinite sets of objects. It follows that the type nat cannot be interpreted as a set of all natural numbers, [[nat]] = ℕ, but as an increasing family of finite sets ℕ_i = {0, … , i-1}. Any reference to [[nat]], either by the formal syntax or by meta-level concepts, must be a reference to a (sufficiently large) set ℕ_i. We present the basic concepts for interpreting a fragment of the simply typed λ-calculus within such a dynamic model. A type ϱ is thereby interpreted as a process, which is formally a factor system together with a limit of it. A factor system is very similar to a direct or an inverse system, and its limit is also defined by a universal property. It is crucial to recognize that a limit is not necessarily an unreachable end beyond the process. Rather, it can be regarded as an intermediate state within the factor system, which can still be extended. The logical type bool plays an important role, which we interpret classically as the set {true, false}. We provide an interpretation of simply typed λ-terms in these factor systems and limits. The main result is a reflection principle, which states that an element in the limit has a "full representative" at a sufficiently large stage within the factor system. For propositions, that is, terms of type bool, this implies that statements about the limit are true if and only if they are true at that sufficiently large stage.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Lambda calculus
• Theory of computation → Higher order logic
• Theory of computation → Type theory
• Theory of computation → Denotational semantics
##### Keywords
• Indefinite extensibility
• Potential infinite
• Reflection principle

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. Samson Abramsky and Achim Jung. Domain theory. In Handbook of logic in computer science. Oxford University Press, 1994.
2. Hendrik Pieter Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, Amsterdam, 1985.
3. Alonzo Church. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5(2):56-68, 1940. URL: https://doi.org/10.2307/2266170.
4. Matthias Eberl. A model theory for the potential infinite. Reports on Mathematical Logic, 57:3-30, 2022. URL: https://doi.org/10.4467/20842589rm.22.001.16658.
5. Matthias Eberl. Higher-order concepts for the potential infinite. Theoretical Computer Science, 945:113667, 2023. URL: https://doi.org/10.1016/j.tcs.2022.12.017.
6. Marcelo P. Fiore, Gordon D. Plotkin, and Daniele Turi. Abstract syntax and variable binding. In Proc. 14^th LICS Conf., pages 193-202. IEEE, Computer Society Press, 1999. URL: https://doi.org/10.1109/LICS.1999.782615.
7. Nicola Gambino and Peter Aczel. The generalised type-theoretic interpretation of constructive set theory. The Journal of Symbolic Logic, 71(1):67-103, 2006. URL: https://doi.org/10.2178/jsl/1140641163.
8. John Longley and Dag Normann. Higher-order computability, volume 100. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47992-6.
9. Saunders MacLane and Ieke Moerdijk. Sheaves in geometry and logic: A first introduction to topos theory. Springer Science & Business Media, 2012. URL: https://doi.org/10.1007/978-1-4612-0927-0.
10. John C. Mitchell and Eugenio Moggi. Kripke-style models for typed lambda calculus. Annals of Pure and Applied Logic, 51(1-2):99-124, 1991. URL: https://doi.org/10.1016/0168-0072(91)90067-V.
11. Rob Nederpelt and Herman Geuvers. Type theory and formal proof: an introduction. Cambridge University Press, 2014.
12. Gordon Plotkin. Lambda-definability and logical relations. Edinburgh University, 1973.
13. Anne S. Troelstra. Choice sequences. A chapter of intuitionistic mathematics. Oxford logic guides, volume 44. Clarendon Press, 1979.
14. Anne S. Troelstra and Dirk van Dalen. Constructivism in mathematics. vol. i, volume 121 of. Studies in Logic and the Foundations of Mathematics, 26, 1988.
X

Feedback for Dagstuhl Publishing