Godel's Completeness Theorem and Deligne's Theorem
Benjamin Frot

TL;DR
This paper explains the proof of Deligne's theorem on coherent topoi having enough points and shows its equivalence to G"odel's completeness theorem for first-order logic, connecting topos theory and logic.
Contribution
It provides a detailed explanation of Deligne's theorem and its equivalence to G"odel's completeness theorem, emphasizing Barr's theorem and topos-theoretic methods.
Findings
Coherent topoi have enough points.
Deligne's theorem is equivalent to G"odel's completeness theorem.
Surjective geometric morphisms from sheaf topoi over spaces prove the theorem.
Abstract
These notes were written for a presentation given at the university Paris VII in January 2012. The goal was to explain a proof of a famous theorem by P. Deligne about coherent topoi (coherent topoi have enough points) and to show how this theorem is equivalent to G\"odel's completeness theorem for first order logic. Because it was not possible to cover everything in only three hours, the focus was on Barr's and Deligne's theorems. This explains why the corresponding sections have been given more attention. Section 1 and the Appendix were added in an attempt to make this document self-contained and understandable by a reader with a good knowledge of topos theory. A coherent topos is a topos which is equivalent to a Grothendieck topos that admits a site such that has finite limits and there exists a base of with finite covering families. In order to prove that any…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · History and Theory of Mathematics · Computability, Logic, AI Algorithms
