Sheaves, games, and model completions. A categorical approach to nonclassical propositional logics

zbMath1036.03001MaRDI QIDQ1405891

Silvio Ghilardi, Marek W. Zawadowski

Publication date: 8 September 2003

Published in: Trends in Logic -- Studia Logica Library (Search for Journal in Brave)

zbMATH Keywords

toposEhrenfeucht-Fraïssé gamesmodel completionHeyting categoryfinitely-presented Heyting algebras

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Categorical logic, topoi (03G30) Heyting algebras (lattice-theoretic aspects) (06D20) Topoi (18B25) Metamathematics of constructive systems (03F50) Categories of algebras (08C05) Nonclassical models (Boolean-valued, sheaf, etc.) (03C90) Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects) (18F20) Quantifier elimination, model completeness, and related topics (03C10)

Related Items

Uniform interpolation and compact congruences ⋮ Free Heyting Algebras: Revisited ⋮ Uniform Lyndon interpolation for basic non-normal modal logics ⋮ On propositional definability ⋮ Characterization of residuated lattices via multipliers ⋮ Unification, finite duality and projectivity in varieties of Heyting algebras ⋮ THE AUTOMORPHISM GROUP OF THE FRAÏSSÉ LIMIT OF FINITE HEYTING ALGEBRAS ⋮ Weak Fraisse categories ⋮ Deciding the existence of uniform interpolants over transitive models ⋮ A new combination procedure for the word problem that generalizes fusion decidability results in modal logics ⋮ Tarski's theorem on intuitionistic logic, for polyhedra ⋮ Uniform interpolation and sequent calculi in modal logic ⋮ Free Heyting algebra endomorphisms: Ruitenburg’s Theorem and beyond ⋮ Uniform interpolation and coherence ⋮ An open mapping theorem for finitely copresented Esakia spaces ⋮ Gödel algebras free over finite distributive lattices ⋮ Projective algebras and primitive subquasivarieties in varieties with factor congruences ⋮ Quantifier Elimination and Provers Integration ⋮ Model-theoretic methods in combined constraint satisfiability ⋮ Computing coproducts of finitely presented Gödel algebras ⋮ Unnamed Item ⋮ EXISTENTIALLY CLOSED BROUWERIAN SEMILATTICES ⋮ Fixed-Point Elimination in the Intuitionistic Propositional Calculus ⋮ Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) ⋮ Model completeness, covers and superposition ⋮ Interpolation in non-classical logics ⋮ Uniform interpolation and the existence of sequent calculi ⋮ Admissibility of \(\Pi_2\)-inference rules: interpolation, model completion, and contact algebras ⋮ Combination of uniform interpolants via Beth definability ⋮ Combined covers and Beth definability ⋮ MODEL COMPLETIONS FOR UNIVERSAL CLASSES OF ALGEBRAS: NECESSARY AND SUFFICIENT CONDITIONS