Intuitionistic Logic III Subschemas and Topologies

on YouTube ↗55m

" summary

Explains how Grothendieck topologies are implemented as closure operations on the subobject classifier Omega and uses small categories/diagrams as concrete schemas so predicates are actual morphisms. Shows closure builds local logics (e.g. caring only about “today”) and that finite temporal categories give 2^n topologies while loops collapse to trivial boolean behavior. Demonstrates the closure on Omega → pullback construction for subobjects, contrasts set-theoretic topologies with the double-negation topology, and points to worked examples on schema diagrams and temporal KL A+ style categories.

AI-written summary · about

" chapters (20)

1. 0:00Introduction
2. 1:07Categories
3. 5:05Database schema
4. 7:25Intuitionistic logic
5. 10:16Subobject classifier
6. 20:51Boolean logic
7. 22:13Simplifying logic
8. 24:31Explanation
9. 25:08Heritage
10. 26:30Closure Operations
11. 29:38Closure of Truth
12. 32:26Local Predicate
13. 33:39Today Tomorrow
14. 34:34Set Objects
15. 38:38Partial Orders
16. 39:48Groundhog Day
17. 42:30Database
18. 43:26Logical Operations
19. 44:35Subobjects
20. 45:10Boolean

" related talks

• 01h 02mAlgebraic Structures in Logic and Query Evaluation 3Dan Suciu · Logic and Algorithms in Database Theory and AI Boot Camp
• 01h 08mAlgebraic Structures in Logic and Query Evaluation 4Dan Suciu · Logic and Algorithms in Database Theory and AI Boot Camp
• 38mConsistency, Acyclicity, and Positive SemiringsPhokion Kolaitis · Logic and Algebra for Query Evaluation 2023
• 01h 05mAlgebraic Structures in Logic and Query Evaluation 2Val Tannen · Logic and Algorithms in Database Theory and AI Boot Camp
• 21mGenerating Collection Transformations from ProofsMichael Benedikt, Pierre Pradic · POPL 2021
• 01h 01mDatalog and Equality SaturationMax Willsey · Logic and Algebra for Query Evaluation 2023
• 36mOptimizing Relational Programs IIRemy Wang · Fine-Grained Complexity, Logic, and Query Evaluation 2023
• 42mCategories for the Working HackerPhilip Wadler · Strange Loop 2018