I am trying to read bits and pieces of Ingo Blechschmidt's notes on using the internal language of toposes in algebraic geometry.

I have not studied the internal language. I only have a bare bones idea of what it is through these and some other notes. I have also never studied logic. My question is about the last two lines of table 1, which presents the Kripke-Joyal semantics of sheaf topos:

$\begin{aligned} U\models \forall \mathcal F.\; \varphi (\mathcal F) & :\iff\text{for all sheaves }\mathcal F \text{ on }V\text{, open }V\subset U:\; V\models \varphi (\mathcal F) \\ U\models \exists \mathcal F.\; \varphi (\mathcal F)& :\iff \text{there exists an open covering }U=\bigcup_iU_i\text{ such that for all }i\text{ there exists a sheaf }\mathcal F_i\text{ on }U_i\text{ such that }U_i\models \varphi (\mathcal F_i)\end{aligned}$

These last two rules, according to remark 2.2, concern "unbounded quantification and are not part of the classical Kripke Joyal semantics. They are part of Mike Shulman's stack semantics, a slight extension. They are needed so that we can formulate universal properties in the internal language".

First, these two lines are identical to the two preceding them except $\mathcal F$ replaces $s$. Since the structure of the statements doesn't change, I'm confused - what is meant by "unbounded quantification"? Why is quantifying sheaves suddenly a different story?

Second, why were these definitions not taken as part of the Kripke-Joyal semantics?

I understand the tempting answer is "go study logic", but I would really appreciate an explanation for the layman.

  • $\begingroup$ Just because the form (syntax) is the same doesn't mean the meaning (semantics) is the same. The difference here is entirely contained in the word "unbounded": ordinary quantification is bounded, in the sense of being restricted to the "elements" of some object; but how could there be an object whose "elements" are all objects? $\endgroup$ – Zhen Lin Nov 25 '15 at 1:34
  • $\begingroup$ @ZhenLin I have no doubt you are right and I don't know how to answer your question. I'm hoping for some answers myself. $\endgroup$ – Arrow Nov 26 '15 at 14:33
  • $\begingroup$ It's a rhetorical question. There is no such object. $\endgroup$ – Zhen Lin Nov 26 '15 at 15:47
  • $\begingroup$ @ZhenLin I thought proper classes circumvented this issue. $\endgroup$ – Arrow Nov 26 '15 at 20:09
  • $\begingroup$ A proper class, being proper, is not an actual object itself. $\endgroup$ – Zhen Lin Nov 26 '15 at 20:32

Bounded quantification is saying "for all elements $x \in X$, it holds that ..." or "there exists an element $x \in X$ such that ...". Unbounded quantification is saying "for all (sets) $X$, it holds that ..." or saying "there exists a set $X$ such that ...".

For some parts of mathematics, bounded quantifications entirely suffice. For instance, when talking about continuous functions and their elementary properties, one only quantifies about sets like $\mathbb{R}$, $\mathbb{R}^{\mathbb{R}}$ (functions $\mathbb{R} \to \mathbb{R}$), and $\mathbb{R}^{\mathbb{N}}$ (sequences of real numbers).

However, in other parts of mathematics, unbounded quantifications are a common occurence. For instance, you need those for formulating universal properties: "For any monoid $M$ ..." is short for "for any set $M$, any map $\circ : M \times M \to M$, and any designated element $e \in M$ such that the monoid axioms hold, ...".

If we want to be able to import "all of constructive mathematics" into the internal setting, it's therefore important to also be able to express unbounded quantification internally.

Why is quantifying sheaves suddenly a different story? It's because inside $\mathrm{Sh}(X)$, there is no "sheaf of all sheaves" with which we could express unbounded quantification as bounded quantification. (This is what Zhen Lin alluded to in the comments.) From a purely practical point of view, there is indeed not so much of a difference.

Second, why were these definitions not taken as part of the Kripke–Joyal semantics? This should be answered by someone more well-versed with the history. You are quite right that these definitions are not intrinsically hard, but saying so with the benefit of hindsight is always easy. I don't know why the early pioneers of internal language didn't think about, didn't write about, or at least didn't give a formal account of expressing unbounded quantification internally. See for instance chapter 3 of the 1987 paper "Polymorphism is Set Theoretic, Constructively" by Andrew Pitts for an indication that some of the relevant ideas were already present.

In any case, thanks for your questions! I will try to improve the notes in light of your feedback.

  • $\begingroup$ Thank you for the amazing notes! $\endgroup$ – Arrow Nov 29 '15 at 21:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.