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!

Improve this question
$\endgroup$
2
  • 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$
    – მამუკა ჯიბლაძე
    Commented Dec 25, 2016 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
    Commented Dec 26, 2016 at 15:18

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .