Syntactic Forcing Models for Coherent Logic

TL;DR

This paper introduces three syntactic forcing models for coherent logic, demonstrating their properties and providing an example of a T-redundant sentence that is false in the generic model, thus addressing a question by Wraith.

Contribution

It develops new syntactic forcing models for coherent logic based on sites and signatures, without requiring equality, and provides a counterexample to a question about T-redundant sentences.

Findings

Three syntactic forcing models for coherent logic are constructed.

A T-redundant sentence can be false in the generic model.

Answers a question by Wraith negatively.

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.