2
$\begingroup$

I'm using Goldblatt's "Topoi: A categorical analysis of logic" as an introduction to topos logic. At the end of chapter 6, he defines the validity of propositional formulas (I'm not concerned with first-order) in a pretty straightforward way: a valuation $V$ assigns to each propositional variable $x_i$ a "truth-value", i.e., an arrow $V(x_i) : 1 \rightarrow \Omega$. He then extends this notion inductively to every formula in the following way:

  • $V(\neg \varphi) = \neg \circ V(\varphi)$
  • $V(\varphi_1 \lor \varphi_2) = \cup \circ \langle\varphi_1,\varphi_2\rangle$
  • $V(\varphi_1 \land \varphi_2) = \cap \circ \langle\varphi_1,\varphi_2\rangle$
  • $V(\varphi_1 \supset \varphi_2) = \Rightarrow \circ \langle\varphi_1,\varphi_2\rangle$

A formula $\varphi$ is said to be valid in a topos $\mathcal{C}$ if, for every possible valuation $V$, $V(\varphi) = \top$. If $\varphi$ is a propositional formula with $n$ variables, this construction gives us a way of attributing to $\varphi$ one and only one arrow $F(\varphi) : \Omega^n \rightarrow \Omega$, by "interpreting" the logical operators ($\lor,\land,\neg,\supset$) but not the variables.

Further, in section 7.4, it appears to me that he states that the validity of a formula $\varphi$ is equivalent to the commutativity of the following diagram: $$ \require{AMScd} \begin{CD} \Omega^n @>{id_{\Omega^n}}>> \Omega^n\\ @V{!}VV @VV{F(\varphi)}V\\ 1 @>>{\top}> \Omega \end{CD} $$

Now, if $\mathcal{C}$ is a well-pointed category, I can prove that this is in fact an equivalence, but I'm not being able to do it for a general topos. In fact, because his statements in section 7.4 are so vague, I'm not even sure this is true in general.

Has anyone thought about this?

Thanks in advance!

$\endgroup$
  • 1
    $\begingroup$ I agree that discussion in 7.4 is sort of vague, but what you say is nowhere stated there; on the contrary, a counterexample is given, for $\varphi(x)=x\lor\neg x$ in $M$-sets, where $M$ is a monoid which is not a group. In this topos $\Omega$ has only two elements, which implies that $\varphi$ is valid there in Goldblatt's sense. However the above diagram does not commute for $\varphi$ - the topos is not Boolean. Such pathologies are avoided in Kripke-Joyal semantics, where variables are interpreted by identity morphisms, and then the statement about the diagram becomes trivially true. $\endgroup$ – მამუკა ჯიბლაძე Dec 25 '16 at 21:14
  • 1
    $\begingroup$ To bolster @მამუკაჯიბლაძე's remark: it's more or less a mistake to consider only global points $1 \to \Omega$ as possible values in a valuation. The correct thing is to consider global points, i.e., morphisms $A \to \Omega$ for arbitrary $A$. Then things will work out correctly, including the equivalence you seek. Under special circumstances, one might be able to restrict to less general domains of points, for instance to $1$ in a well-pointed category or to the representables in a sheaf topos. In other words, pick up a newer book; Colin McLarty's "Elementary toposes" is not too daunting. $\endgroup$ – Andrej Bauer Dec 26 '16 at 15:18

Your Answer

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

Browse other questions tagged or ask your own question.