Nontrivial example of topos in the context of logic I am reading Awodey's paper Structure in Mathematics and Logic: A Categorical Perspective and he is currently (p. 228-9) talking about how propositions, that is, elements $1\rightarrow P$, correspond to subobjects of $1$.  Thus he constructs conjunction by saying that the conjunction of two elements of $P$ corresponds to the product of the corresponding subobjects of $1$.  I am playing this all back in my head with the only model I know, which is the topos $\textrm{Set}$.  Here the subobjects of $1$ form the small category $2$, so the formalism lacks resolution.  Can someone give me another topos with logical semantics to try these things out on where we can really see what is going on, e.g. where the product looks more like a product?
 A: I'll admit I did not look at Awodey's paper, but you might be interested in the (Grothendieck) topoi that arise in first order categorical logic. A good place to read about these is 


*

*Victor Harnik - Model theory vs. categorical logic: two approaches to pretopos completion (a.k.a. $\mathrm{T}^{\mathrm{eq}}$)


Let me just sketch the main construction, and why it seems to relate to your question. Fix a first order theory $\mathbb{T}$ in some language $\mathcal{L}$, and define $\mathcal{S}(\mathbb{T})$ to be the category with


*

*Objects: $[\phi]$, where $\phi$ is a formula in $\mathcal{L}$ in some free variables $x_1,\ldots,x_n$,

*Morphisms: a morphism $[\phi]\rightarrow[\psi]$, where $\phi$ is a formula in free variables $x_1,\ldots,x_n$ and $\psi$ is a formula in free variables $y_1,\ldots,y_m$, is an equivalence class of formulas $\chi$ in free variables $x_1,\ldots,x_n,y_1,\ldots,y_m$ which $\mathbb{T}$ proves is a map from $\phi$ to $\psi$; explicitly, $\mathbb{T}\vdash (\forall \vec{x},\vec{y}.(\chi(\vec{x},\vec{y})\rightarrow \phi(\vec{x})\wedge \psi(\vec{y}))\wedge(\forall \vec{x}(\phi(\vec{x})\rightarrow \exists ! \vec{y}. \chi(\vec{x},\vec{y}))$. Here, two formulas are equivalent if $\mathbb{T}$ proves that they define the same function.
Here are some features of $\mathcal{S}(\mathbb{T})$:


*

*$\mathcal{S}(\mathbb{T})$ has finite limits,

*Every map $X\rightarrow Z$ factors as $X\xrightarrow{g}Y\xrightarrow{f}Z$ where $g$ is an effective epimorphism and $f$ is a monomorphism. (Here, $Y$ is the image of $g$, which is definable).

*For every $X\in\mathcal{S}(\mathbb{T})$, the poset $\mathrm{Sub}(X)$ is a distribute lattice; and for every $f\colon X\rightarrow Y$, the pullback map $f^\ast\colon \mathrm{Sub}(Y)\rightarrow\mathrm{Sub}(X)$ is a map of distributive lattices.
These facts are true also of the category of sets (they are the axioms of a coherent category), and the subcategory of $\mathrm{Fun}(\mathcal{S}(\mathbb{T}),\mathrm{Set})$ of functors preserving this structure is equivalent to the category of models of $\mathbb{T}$ and elementary embeddings.
The terminal object of $\mathcal{S}(\mathbb{T})$ is $[\top]$ (no free variables), and a subobject of the terminal object is a sentence $[\phi]$. The logical semantics are quite clear here: in the poset $\mathrm{Sub}([\top])$, we have $[\phi]\vee [\psi] \cong [\phi\vee\psi]$ and $[\phi] \wedge [\psi] \cong [\phi\wedge \psi]$. For example, $[\phi] \cong [\bot]$ precisely when $\mathbb{T}\vdash \neg \phi$. 
You might object, because $\mathcal{S}(\mathbb{T})$ is not a topos. However, $\mathcal{S}(\mathbb{T})$ admits a Grothendieck topology generated by the effective epimorphisms. (Concretely, $\{X_i\rightarrow Z\}_{i\in I}$ is a cover when there exists a finite subset $F\subset I$ such that if we factor $X_i\rightarrow Y_i\rightarrow Z$ with $Y_i\rightarrow Z$ monic, then $\bigvee_{i\in F}Y_i \cong Z$). If $\mathcal{C}(\mathbb{T}) = \mathrm{Shv}(\mathcal{S}(\mathbb{T}))$, then:


*

*The Yoneda embedding $\mathcal{S}(\mathbb{T})\rightarrow\mathcal{C}(\mathbb{T})$ induces an isomorphism $\mathrm{Sub}([\top])\cong \mathrm{Sub}(1)$,

*A model of $\mathbb{T}$ is a point of $\mathcal{C}(\mathbb{T})$, i.e. a functor $F\colon \mathcal{C}(\mathbb{T})\rightarrow\mathrm{Set}$ which preserves colimits and finite limits.
So $\mathcal{C}(\mathbb{T})$ retains the logical semantics of $\mathcal{S}(\mathbb{T})$.
A: One source of toposes with easily understandable internal logic is to take a complete Heyting algebra $H$ and form a topos in the following way:


*

*The objects are pairs $\langle X,\sim\rangle$ where $\sim$ is a function $X\times X\to H$ such that for any $x,y\in X$, $x\sim y=y\sim x$ and $x\sim y\wedge y\sim z\leq x\sim z$ (where "$\wedge$" is the meet operation of $H$). That is, the objects are sets with $H$-valued partial equivalence relations.

*The morphisms $\langle X,\sim\rangle\to\langle Y,\approx\rangle$ are equivalence classes of functions $F:X\times Y\to H$ such that the following hold:


*

*$F(x,y)\wedge x\sim x'\wedge y\approx y'\leq F(x',y')$

*$F(x,y)\leq x\sim x\wedge y\approx y$ (these first two just make sure $F$ plays nicely with equality)

*$F(x,y)\wedge F(x,y')\leq y\approx y'$ ($F$ is functional)

*$x\sim x\leq \bigvee_{y\in Y}F(x,y)$ ($F$ is defined everywhere on its domain)



That this is a topos is proved in Borceux's Handbook of Categorical Algebra, vol 3 (there called $\Omega$-sets), and in a more general form in Ch. 6 of Jacobs's Categorical Logic and Type Theory. As it happens, the topos resulting from the construction above is equivalent to the category of sheaves on $H$; but this construction is neat because it puts the logic first.
Subobjects of $\langle X,\sim\rangle$ correspond to functions $P:X\to H$ such that $P(x)\leq x\sim x$ and $x\sim x'\wedge P(x)\leq P(x')$ (such a $P$ is usually called a "strict predicate"), and the subobject classifier is the object $\langle H,\Leftrightarrow\rangle$ together with the strict predicate $-\Leftrightarrow\top$. In fact, for any $h\in H$, the strict predicate $-\Leftrightarrow h$ is the same as a morphism $1\to\langle H,\Leftrightarrow\rangle$, and for distinct elements of $H$, the associated predicate will be distinct. So the "propositions" of this topos, in the sense referred to in the original post, are essentially just the elements of $H$. Finally, operations on subobjects, and hence on propositions, come from the Heyting operations of $H$.
So the point of that is that if you want a richer propositional structure, you can pick the open sets of any topological space that seems reasonably transparent, and there is a topos that will have those as its lattice of propositions. On the other hand, for any topos $\hom(1,\Omega)$ will have the structure of a Heyting algebra (the proof of this is lengthy and standard, so I omit it), so when it comes merely to propositions in the sense of morphisms $1\to\Omega$, there's not much more to say in general than there is to say about Heyting algebras in general.
It's worth noting, though, that in a topos that is not well-pointed, there may be more to say about $\Omega$ than the Heyting structure of the propositions. For example, in the category of directed multigraphs, the terminal object is the graph with one vertex and one looped edge, so there are only three morphisms $1\to\Omega$. But in this category $\Omega$ actually has two vertices and five edges, which is structure you'd never see only looking at points.
