Skolem’s Theorem in Coherent Logic

• Autorzy: Bezem Marc , Coquand Thierry

Identyfikatory

DOI

10.3233/FI-2019-1853

• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

Skolem’s theorem; coherent logic; proof theory

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 170, nr 1-3
• Strony: 1--14
• Opis fizyczny: Bibliogr. 13 poz.

Twórcy

autor

Bezem Marc

• Department of Informatics, University of Bergen, Norway

autor

Coquand Thierry

• Department of Computer Science and Engineering, Chalmers/University of Gothenburg, Sweden

Bibliografia

• [1] M. Baaz and A. Leitsch. On Skolemization and Proof Complexity. Fundamenta Informaticae 1994. 20(4):353-379. https://doi.org/10.3233/FI-1994-2044.
• [2] Barr M. Toposes without points. Journal of Pure and Applied Algebra 1974. 5(3):265-280.
• [3] Bezem MA, Buchholtz U, and Coquand T. Syntactic Forcing Models for Coherent Logic. Indagationes Mathematicae, https://doi.org/10.1016/j.indag.2018.06.004.
• [4] Coste M, Lombardi H, and Roy MF. Dynamical methods in algebra: effective Nullstellensätze. Annals of Pure and Applied Logic 2001. 111(3):203-256.
• [5] Coquand Th, and Mannaa B. A Sheaf Model of the Algebraic Closure. Proceedings of EPTCS, 2014. https://doi.org/10.4204/EPTCS.164.2.
• [6] Dowek G, and Werner B. A constructive proof of Skolem theorem for constructive logic. Manuscript, 2004. http://www.lsv.fr/~dowek/Publi/skolem.pdf.
• [7] Kock A. Universal projective geometry via topos theory. J. Pure Appl. Algebra 1976/77. 9(1):1-24. URL https://doi.org/10.1016/0022-4049(76)90002-5.
• [8] Mac Lane S, and Moerdijk I. Sheaves in geometry and logic. Springer-Verlag, New York 1994. ISBN-100387977104, 13:978-0387977102.
• [9] Maehara S. The predicate calculus with є-symbol. Journal of the Mathematical Society of Japan 1955. 7(4):323-344. doi:10.2969/jmsj/00740323.
• [10] Mints G. Axiomatisation of a Skolem function in intuitionistic logic. In: In M. Faller, S. Kaufmann and M. Pauly, editors, Formalizing the dynamics of information, volume 92 of CSLI Lecture Notes 2000 pp. 105-114.
• [11] Negri S. Contraction-free sequent calculi for geometric theories with an application to Barrs theorem. Arch. Math. Logic 2003. 42(4):389-401. doi:10.1007/s001530100124.
• [12] Skolem Th. Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit und Beweisbarkeit mathematischen Sätze nebst einem Theoreme über dichte Mengen, Skrifter I 4:1-36, Det Norske Videnskaps-Akademi, 1920. Also in: Jens Erik Fenstad, editor, Selected Works in Logic by Th. Skolem, Universitetsforlaget, Oslo 1970 pp. 103-136.
• [13] Wraith GC. Intuitionistic algebra: some recent developments in topos theory. Proceedings of the International Congress of Mathematicians (Helsinki) 1978 pp. 331-337.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).