Regarding the internalization of mathematics to a particular category as in the nLab article: [Internal Logic](http://ncatlab.org/nlab/show/internal+logic), there is a peculiar table mentioned in the section on [Categorical Semantics](http://ncatlab.org/nlab/show/internal+logic#CategoricalSemantics) in which there is a corresponding category-theoretic construction to the regular logical operators in a theory. In particular, $\wedge$ corresponds to a pullback of a cospan, $\top$ corresponds to the top element (A itself), $\wedge$ corresponds to union, $\bot$ corresponds to the bottom element (strict initial object), $\Rightarrow$ corresponds to the Heyting implication, $\exists$ corresponds to the left adjoint to a pullback (I'm not sure which pullback in particular?), and $\forall$ corresponds to the right adjoint to a pullback (what pullback is this also?).


Would it be possible to define the modal operators of $\Box$ and $\Diamond$ as the right adjoint of a pushout (similarly to how $\forall$ is the right adjoint to a pullback) and the left adjoint of a pushout (similarly to how $\exists$ is the left adjoint to a pullback), respectively? Or, if this does not work, could it be possible to define modal operators in internal logic using some other category theoretic construction?



Adjoint of Pushout as Modal Operators in Internal Logic
Probably you should get a hold of a textbook on categorical logic for some of these questions. Of the references given in the [Wikipedia article](http://en.wikipedia.org/wiki/Categorical_logic), the one by Lambek & Scott and the two with Lawvere as an author might be a good start. A study of these would probably help make the table in the nLab seem less "peculiar". 


I see that Wouter Stekelenburg has posted an answer just as I started this, but it wouldn't hurt to amplify. The propositional connectives (on predicates of a given type $A$) are interpreted as operations on the poset of subobjects $Sub(A)$ (e.g., the pullback of two subobjects of $A$ is another subobject of $A$ which corresponds to the meet). Next, each morphism $f: B \to A$ in the category induces an inverse image operation $f^{-1}: Sub(A) \to Sub(B)$, formally defined by taking a pullback: if $i: U \to A$ is a monomorphism, then the pullback of the cospan $(f, i)$ is given by a pair of maps $(g: V \to U, j: V \to B)$ where one may show easily from general properties of pullbacks that $j$ is a monomorphism, thus giving a subobject of $B$. In the classical case where $f$ is a projection map $\pi: X \times A \to A$, you can think of the inverse image $\pi^{-1}: Sub(A) \to Sub(X \times A)$ as interpreting the operation which takes a predicate $\phi$ of type $A$ and forming a predicate of type $X \times A$ by harmlessly adjoining a variable of type $X$, e.g., by taking $\phi \wedge [x = x]$. 


Then quantifiers $\exists\_f$, $\forall\_f$ are operations $Sub(B) \to Sub(A)$ that are left and right adjoint (respectively) to $f^{-1}: Sub(A) \to Sub(B)$. It might help to consider the classical case where $f$ is the projection $\pi: X \times A \to A$. Here the left adjoint $\exists\_f$ takes a subobject of $X \times A$ (that interprets a predicate $\phi(x, a)$ of type $X \times A$) to one of type $A$, interpreting the predicate that is usually denoted $\exists\_x \phi(x, a)$. (In other words, classical quantification has to do with adjoints to puling back along projection maps $\pi$.) The adjunction between $\exists\_{\pi}$ and $\pi^{-1}$ corresponds to the inference rule 


$$\exists\_x \phi(x, a) \vdash \psi(a) \qquad \mathrm{iff} \qquad \phi(x, a) \vdash \psi(a) \wedge [x = x]$$ 


where the entailment symbols are interpreted as subobject inclusions in the appropriate posets $Sub(A)$, $Sub(X \times A)$. (Normally one isn't so fussy as to write $\psi(a) \wedge [x = x]$; one usually writes simply $\psi(a)$, but keeping in mind that $\psi$ is here being considered a predicate of type $X \times A$, so that the types match.) 


Your guesses about the modalities are a little off. There are lots of places to read about categorical semantics of modal logic; one nice place (for S4 necessity) is in the [paper](http://philpapers.org/rec/AWOTAM-2) by Awodey and Kishida. It might help first to be familiar with the topological semantics of "necessity" as a topological interior operation on power sets $\Box = \mathrm{int}: P(A) \to P(A)$, due originally to Tarski. 


