Skolem’s Theorem in Coherent Logic

Issue title: Types, terms and reductions: A special issue dedicated to Paweł Urzyczyn for his 65th birthday

Guest editors: Thorsten Altenkirch and Aleksy Schubert

Article type: Research Article

Authors: Bezem, Marc^{a; *} | Coquand, Thierry^b

Affiliations: [a] Department of Informatics, University of Bergen, Norway. [email protected] | [b] Department of Computer Science and Engineering, Chalmers/University of Gothenburg, Sweden. [email protected]

Correspondence: [*] Address for correspondence: Department of Informatics, University of Bergen, Postboks 7800 N-5020 Bergen, Norway

Abstract: We give a constructive proof of Skolem’s Theorem for coherent logic and discuss several applications, including a negative answer to a question by Wraith.

Keywords: Skolem’s theorem, coherent logic, proof theory

DOI: 10.3233/FI-2019-1853

Journal: Fundamenta Informaticae, vol. 170, no. 1-3, pp. 1-14, 2019