| Résume | The starting point of this talk is a theorem of A. Pitts on encoding propositional quantifiers inside intuitionistic logic. I will explain Pitts' result, and a proof of it via an open mapping theorem between certain topological spaces [1]. I will further discuss how to compute propositional quantifiers in practice [2], and how all this relates to model completions [3].
References:
[1] S. v. Gool and L. Reggio, An open mapping theorem for finitely copresented Esakia spaces, Topology and its Applications 240, 69-77 (2018)
[2] H. Férée and S. v. Gool, Formalizing and Computing Propositional Quantifiers, Conference on Programs and Proofs (2023)
[3] S. v. Gool, G. Metcalfe, and C. Tsinakis, Uniform interpolation and compact congruences, Annals of Pure and Applied Logic 168, 1927-1948 (2017) |
