Syntactic forcing models for coherent logic

DOI10.1016/J.INDAG.2018.06.004MaRDI QIDQ1788327zbMATH OpenOpenAlexFDO

Authors Marc Bezem, Ulrik Buchholtz, Thierry Coquand

Publication date 8 October 2018

Published in Indagationes Mathematicae. New Series (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1712.07743

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Categorical logic, topoi (03G30) Topoi (18B25)

Abstract: We present three syntactic forcing models for coherent logic. These are based on sites whose underlying category only depends on the signature of the coherent theory, and they do not presuppose that the logic has equality. As an application we give a coherent theory T and a sentence {psi} which is T-redundant (for any geometric implication {phi}, possibly with equality, if T + {psi} proves {phi}, then T proves {phi}), yet false in the generic model of T. This answers in the negative a question by Wraith.

Recommendations

• scientific article; zbMATH DE number 3880663
• scientific article; zbMATH DE number 1163388
• Compositional model-theoretic semantics for logic programs
• scientific article; zbMATH DE number 1251242
• Semantic models for concurrent logic languages
• Syntactical models and fixed points for the basic logic of proofs
• Expressive Logics for Coinductive Predicates
• Expressive logics for coinductive predicates
• Basic principles of the synthesis of logical-linguistic models

Cites work

• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 3668606 (Why is no real title available?)
• scientific article; zbMATH DE number 1840601 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Constructive Sheaf Semantics
• Cut Elimination in the Presence of Axioms
• Exact completions and small sheaves
• On the rules of proof in the pure functional calculus of the first order
• Open maps of toposes
• Proof analysis beyond geometric theories: from rule systems to systems of rules

Cited in

(2)

• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
• Polysemy and Coercion – A Frame-Based Approach Using LTAG and Hybrid Logic

This page was built for publication: Syntactic forcing models for coherent logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1788327)