On the nlab page for internal logic it says
The Internal Logic as a Functor
As described above, a model of a given theory $T$ in a category $C$ consists of an assignment
\begin{array}{|c|c|c|} \hline & & \\ \hline \text{types of $T$} & \to & \text{objects of $C$} \\ \hline \text{function symbols of $T$} & \to & \text{morphisms of $C$} \\ \hline \text{relation symbols of $T$} & \to & \text{subobjects in $C$} \\ \hline \text{axioms of $T$} & \to & \text{containments in $C$} \\ \hline \end{array}
What exactly does it mean that "axioms of $T$" are "containments in $C$"?
Can someone give an example in the syntactic category of $PA$ or $HA$?
Let's say we have a free monoidal category out of a category with one object $*$ (so objects are lists of this one context $*$, i.e: arities), and we may have morphisms
- $0:1\rightarrow*$
- $S:*\rightarrow*$
- $+:*\otimes*\rightarrow*$
- $\cdot:*\otimes*\rightarrow*$
- $=:*\hookrightarrow*\otimes*$
- $<:*\hookrightarrow*\otimes*$
(You may comment if you think there's a more natural way to think of the syntactic category. Ultimately I was thinking the most natural way was with operads/multicategories, and abstracting the subobject functor to a contravariant functor as with hyperdoctrines, but I have no idea how that behaves with multicategories so I don't want to get into that right now even if it's interesting; expecting that to work nicely for predicates. But you may comment if you think I'm overcomplicating things here.)
Then how do the axioms of $PA$ or $HA$ look internally?
Say as an example the axiom $\forall x.\ S\ x = x \rightarrow \bot$.
(It doesn't seem to say what "containment" refers to exactly in the nlab page, and the references seem too hard for me right now and for my purposes. I'm realizing right now that it must mean being related in the poset of subobjects, for some object.)
Thanks in advance!
For the purposes of this nlab page, an axiom is something of the form "$\Gamma \mid \varphi \vdash \psi$". This is to be interpreted as
For instance, in the theory of groups, we have an axiom "$x:G, y:G, z:G \mid \top \vdash (xy)z = x(yz)$". The context "$\Gamma = x:G, y:G, z:G$" tells us which variables we're using (and what their types are), the antecedent $\top$ tells us what we're assuming, and the consequent "$(xy)z = x(yz)$" tells us what we expect to be true whenever the antecedent is.
In this case, we're not assuming anything (since $\top$ is always true), so we're saying that the consequent always holds. That is, multiplication is always associative.
Now what does this have to do with containment? A formula $\varphi$ is a subobject of its context $\Gamma$. Indeed, we can identify $\varphi$ with "$\{ \gamma \in \Gamma \mid \varphi(\gamma) \}$" (for now think of this as informal, but the internal logic lets us make it precise in many settings).
Then we interpret an axiom "$\Gamma \mid \varphi \vdash \psi$" as saying that "whenver $\varphi$ is true, $\psi$ is true too". That is, for every $\gamma$, if $\varphi(\gamma)$, then $\psi(\gamma)$. But this says exactly that $\{ \gamma \mid \varphi \} \subseteq \{ \gamma \mid \psi \}$! Precisely now, our subobject lattice $\text{Sub}(\Gamma)$ comes with a partial ordering $\leq$, and we say that the axiom "$\Gamma \mid \varphi \vdash \psi$" holds if and only if $\varphi \leq \psi$ in this order.
For your example, if you wanted to interpret the axiom "$x : \mathbb{N} \mid Sx = x \vdash \bot$", this is asking that the subobject $Sx = x$ of $\mathbb{N}$ (which you should think of as $\{ x \in \mathbb{N} \mid Sx = x \}$) be contained in $\bot$ (which you should think of as $\emptyset$). Hopefully this lines up with your intuition for how axioms "should" behave.
I hope this helps ^_^