Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: "Negative use'' of sheaf models for geometric logic

Yiming Xu (Aug 13 2025 at 06:33):

One useful application of the completeness of constructive logic with sheaf models is that we can prove something is not provable by giving a sheaf model.

To be clear what I am asking about:
Some effort of searching such an example takes me to this https://www.cse.chalmers.se/~coquand/hott.pdf , page 4 gives an example of showing there is no algorithm telling us if $x^2+1$ is irreducible.
(this also appears in the video by Coquand https://www.youtube.com/watch?v=bF8gcIOKcqw&t=3281s Around 7:50)However, the example is in first-order logic, the inequality has to be there and cannot be modified into geometric form (at least I do not know how to), whereas I am searching for examples on (fragments of) geometric logic.

So, is there any interesting-yet-simple example of establishing something is not provable in the proof system of geometric logic by giving a counterexample using a sheaf model?

If the non-provability can be witnessed by a geometric category that is not a topos (i.e. use the completeness of syntactic category + geometric morphism instead of the completeness among Grothendieck topi), it also makes sense.

Morgan Rogers (he/him) (Aug 14 2025 at 16:46):

The claim on slide 4 is not that there is no algorithm showing that $x^2 +1$ is (ir)reducible. Rather, it says that the proposition $\exists x. x^2+1=0$ is neither globally true nor globally false, and even worse the subspace where it is true is not complemented. So this remains an example valid in geometric logic.

Morgan Rogers (he/him) (Aug 14 2025 at 16:46):

(By the first sentence, I mean that the contention is not really about algorithms, although it is about proofs)

Yiming Xu (Aug 15 2025 at 19:47):

Oh indeed! I just regarded $\forall x (x^2+1)\ne 0 \lor \exists x (x^2 + 1 = 0)$ as a whole and thought it is not geometric. My stupidity! This indeed shows $\exists x (x^2 + 1 = 0)$ is not provable.

Yiming Xu (Aug 15 2025 at 19:53):

My understanding of the algorithmic aspect is still vague. Slide 4 corresponds to the video roughly around 7:50, where Coquand assumes $K$ is a field with decidable equality. From nlab it seems to me that $K$ is a sheaf model of a field, so it seems to me that $K$ is a sheaf in $Sh(C,J)$ where $C$ is a Boolean algebra. I do not know how to intuitively connect this to having an algorithm of determining algebraic equations.