Set-theoretical semantics vs categorical semantics

267 Views Asked by At

Yo! I'm trying to understand the relation between set theoretical models (in the usual Tarskian sense) and categorical models. I don't care whether you gonna use the hyperdoctrine of the subobjects or the one given by the slice categories. I'm fine with an answer using any of these.

I will use arithmetic as a toy model to test such relation.

Let $\mathcal{C}_{HA}$ be the syntactic category of the Heyting arithmetic $HA$.

Explicitly, $\mathcal{C}_{HA}$ has one object $N$ all finite products, a morphism $0: 1 \rightarrow N$ and a morphism $s (n) : 1 \rightarrow N$ for every $n : 1\rightarrow N$.

At first, it looks like that $\mathcal{C}_{HA}$ is very the analogous of the standard model of the natural numbers, but this is obviously false as $\mathcal{C}_{HA}$ validates only what's already provable.

Externally, by definition, every $1 \rightarrow N$ is necessarily of the form $s^m (0) : 1 \rightarrow N$ for some (metatheorical) natural number $m$. However one can't prove it internally as it would infer that $HA$ can prove its consistency. So categorical semantics is somehow more theoretical than usual set theoretical semantics.

Take for instance, the Gödel sentence $G \cong \forall (n : N) (\neg Prov (n, [G]))$. Then the usual proof that it's valid on the standard naturals is by validating each instance $\neg Prov (0, [G])$, $\neg Prov (1, [G])$, $\neg Prov (2, [G])$ etc. That is the $\forall$ is external and it's somehow preserved by the "morphism" from the metatheory to the theory (the theory of the categorical interpretation underlying the standard natural numbers).

In contrast, in categorical semantics the $\forall$ is strictly internal and given by the right adjoint of the change of variables functor.

Another difference is that the standard natural numbers model is initial among the set-theoretical models, however, as noticed above, it cannot be initial among the categorical models.

So the general question is

1) What's the relation between set-theoretical semantics and categorical semantics?

It seems that simply restricting to the $\mathbf{Set}$ valued categorical interpretations wouldn't answer the question as $\mathbf{Set}$ always validates the excluded middle.

The minor questions are

2) What's the categorical version of the standard natural numbers model?

There seems to be a problem if such model is simply given by the obvious set valued interpretation given by setting the object $N$ (as above in the case of $\mathcal{C}_{HA}$) equals to the standard natural numbers as an object of $\mathbf{Set}$. The problem is that it seems to validate that every natural is canonical, which seems to imply consistency of the theory underlying such category. Furthermore such model if interpreted in $\mathbf{Set}$ would always validate the excluded middle as $\mathbf{Set}$ is Boolean.

3) What's the initial model for set theoretical semantics in general (for any theory)?

In the categorical case, it's always given by the syntactic category, however I have no idea about the set theoretical case.

Thanks in advance.