2026-08-21T18:02:52Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27425 2026-08-21T14:42:39Z ddc:004 open_access

Functorial Semantics for First-Order Theories Bonchi, Filippo Di Giorgio, Alessandro Di Virgilio, Roberto Sobociński, Paweł First-order logic Model theory Functorial semantics String diagrams Building on the recent axiomatisation of first-order bicategories, we develop a functorial semantics approach to the model theory of first-order logic. First-order theories 𝕋 are captured by free first-order bicategories ℱ_𝕋 and models of𝕋 are structure-preserving functors from ℱ_𝕋 to a first-order bicategory 𝐂. Elementary morphisms of models arise as lax natural transformations between such functors, and the classical Tarski-Vaught test and downward Löwenheim-Skolem theorem admit direct diagrammatic proofs. Our results instantiate classically when 𝐂 = Rel and hold uniformly for models valued in Rel(𝐃) over an arbitrary Boolean geometric category 𝐃 in which regular epis split. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Filippo Bonchi and Alessandro Di Giorgio and Roberto Di Virgilio and Paweł Sobociński 2026 Is Part Of LIPIcs, Volume 386, 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2026.44 urn:nbn:de:0030-drops-274255 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2026.44 eng https://creativecommons.org/licenses/by/4.0/legalcode