Skip to main content
added 6 characters in body
Source Link
Alex Kruckman
  • 5k
  • 2
  • 24
  • 33

Given any theory $T$, we have a hyperdoctrine $H(T)$ (the "syntactic hyperdoctrine for $T$"), where (in the single sorted case) the $n^{\text{th}}$ lattice is the lattice of formulas in $n$ free variables, up to equivalence modulo $T$.

As Zhen Lin's answer shows, in fact every hyperdoctrine is the syntactic hyperdoctrine for some theory (the "full theory" of the hyperdoctrine).

Now what is a morphism of hyperdoctrines? It's an interpretation of theories. That is, a morphism of hyperdoctrines $H(T)\to H(T')$ gives a translation of formulas relative to $T$ into formulas relative to $T'$, which preserves the logical structure, i.e., an interpretation of $T$ in $T'$. More generally, any morphism of hyperdoctrines $H\to H'$ can be viewed as an interpretation of the full theory of $H$ in the full theory of $H'$.

When we view a traditional model $M$ of $T$ as a hyperdoctrine under $H(T)$, we form the hyperdoctrine $H(M)$ where (in the single sorted case) the $n^{\text{th}}$ lattice is $\mathcal{P}(M^n)$. And we get a morphism of hyperdoctrines $H(T)\to H(M)$ mapping a formulas relative to $T$ to its evaluation in $M$ (the set of tuples in $M$ satisfying the formula). Note that we can also view this as an interpretation of $T$ in the full theory of $M$: This theory has relation symbols for every subset of $M^n$ for all $n$, and the interpretation sends a formula to the relation symbol naming its evaluation in $M$. This is one of the features of categorical logic: it puts the notion of "model of a theory" and "interpretation of theories" on the same footing.

Ok, so addressing your question: if a "hyperdoctrine for $\mathsf{PA}$" is a hyperdoctrine $H$ equipped with a morphism $H(\mathsf{PA})\to H$, then we have initial hyperdoctrine for $\mathsf{PA}$ (which is the syntactic hyperdoctrine $H(\mathsf{PA})$ itself) and all the standard models of $\mathsf{PA}$ in the form $H(M)$. What else? Well, we have a "hyperdoctrine for $\mathsf{PA}$" for every interpretation of $\mathsf{PA}$ into a theory $T$. For example, the standard interpretation of $\mathsf{PA}$ in $\mathsf{ZFC}$ gives a morphism of hyperdoctrines $H(\mathsf{PA})\to H(\mathsf{ZFC})$. And in a precise sense, every hyperdoctrine for $\mathsf{PA}$ has this form, since every morphism of hyperdoctrines can be viewed as an interpretation of theories. The terminal hyperdoctrine for $\mathsf{PA}$ is the interpretation of $\mathsf{PA}$ in the inconsistent theory.

So typical hyperdoctrines for $\mathsf{PA}$ include things like $H(T)$ where $T$ is a stronger theory than $\mathsf{PA}$ (obtained by adding axioms) or $H(T)$ where $T$ is an expansion of $\mathsf{PA}$ to include extra structure. In the comments, you wrote that you were hoping for something like "there's a hyperdoctrine for $\mathsf{PA}$ of only the decidable predicates". This doesn't make sense, since any hyperdoctrine for $\mathsf{PA}$ must interpret all the predicates definable in $\mathsf{PA}$, not just the decidable ones.

I've been intentionally vague about some details here (like what counts as a morphism of hyperdoctrines), hoping that a more high level view will help get your thinking on the right track.

Given any theory $T$, we have a hyperdoctrine $H(T)$ (the "syntactic hyperdoctrine for $T$"), where (in the single sorted case) the $n^{\text{th}}$ lattice is the lattice of formulas in $n$ free variables, up to equivalence modulo $T$.

As Zhen Lin's answer shows, in fact every hyperdoctrine is the syntactic hyperdoctrine for some theory (the "full theory" of the hyperdoctrine).

Now what is a morphism of hyperdoctrines? It's an interpretation of theories. That is, a morphism of hyperdoctrines $H(T)\to H(T')$ gives a translation of formulas relative to $T$ into formulas relative to $T'$, which preserves the logical structure, i.e., an interpretation of $T$ in $T'$. More generally, any morphism of hyperdoctrines $H\to H'$ can be viewed as an interpretation of the full theory of $H$ in the full theory of $H'$.

When we view a traditional model $M$ of $T$ as a hyperdoctrine under $H(T)$, we form the hyperdoctrine $H(M)$ where (in the single sorted case) the $n^{\text{th}}$ lattice is $\mathcal{P}(M^n)$. And we get a morphism of hyperdoctrines $H(T)\to H(M)$ mapping a formulas relative to $T$ to its evaluation in $M$ (the set of tuples in $M$ satisfying the formula). Note that we can also view this as an interpretation of $T$ in the full theory of $M$: This theory has relation symbols for every subset of $M^n$ for all $n$, and the interpretation sends a formula to the relation symbol naming its evaluation in $M$. This is one of the features of categorical logic: it puts the notion of "model of a theory" and "interpretation of theories" on the same footing.

Ok, so addressing your question: if a "hyperdoctrine for $\mathsf{PA}$" is a hyperdoctrine $H$ equipped with a morphism $H(\mathsf{PA})\to H$, then we have initial hyperdoctrine for $\mathsf{PA}$ (which is the syntactic hyperdoctrine $H(\mathsf{PA})$ itself) and all the standard models of $\mathsf{PA}$ in the form $H(M)$. What else? Well, we have a "hyperdoctrine for $\mathsf{PA}$" for interpretation of $\mathsf{PA}$ into a theory $T$. For example, the standard interpretation of $\mathsf{PA}$ in $\mathsf{ZFC}$ gives a morphism of hyperdoctrines $H(\mathsf{PA})\to H(\mathsf{ZFC})$. And in a precise sense, every hyperdoctrine for $\mathsf{PA}$ has this form, since every morphism of hyperdoctrines can be viewed as an interpretation of theories.

So typical hyperdoctrines for $\mathsf{PA}$ include things like $H(T)$ where $T$ is a stronger theory than $\mathsf{PA}$ (obtained by adding axioms) or $H(T)$ where $T$ is an expansion of $\mathsf{PA}$ to include extra structure. In the comments, you wrote that you were hoping for something like "there's a hyperdoctrine for $\mathsf{PA}$ of only the decidable predicates". This doesn't make sense, since any hyperdoctrine for $\mathsf{PA}$ must interpret all the predicates definable in $\mathsf{PA}$, not just the decidable ones.

I've been intentionally vague about some details here (like what counts as a morphism of hyperdoctrines), hoping that a more high level view will help get your thinking on the right track.

Given any theory $T$, we have a hyperdoctrine $H(T)$ (the "syntactic hyperdoctrine for $T$"), where (in the single sorted case) the $n^{\text{th}}$ lattice is the lattice of formulas in $n$ free variables, up to equivalence modulo $T$.

As Zhen Lin's answer shows, in fact every hyperdoctrine is the syntactic hyperdoctrine for some theory (the "full theory" of the hyperdoctrine).

Now what is a morphism of hyperdoctrines? It's an interpretation of theories. That is, a morphism of hyperdoctrines $H(T)\to H(T')$ gives a translation of formulas relative to $T$ into formulas relative to $T'$, which preserves the logical structure, i.e., an interpretation of $T$ in $T'$. More generally, any morphism of hyperdoctrines $H\to H'$ can be viewed as an interpretation of the full theory of $H$ in the full theory of $H'$.

When we view a traditional model $M$ of $T$ as a hyperdoctrine under $H(T)$, we form the hyperdoctrine $H(M)$ where (in the single sorted case) the $n^{\text{th}}$ lattice is $\mathcal{P}(M^n)$. And we get a morphism of hyperdoctrines $H(T)\to H(M)$ mapping a formulas relative to $T$ to its evaluation in $M$ (the set of tuples in $M$ satisfying the formula). Note that we can also view this as an interpretation of $T$ in the full theory of $M$: This theory has relation symbols for every subset of $M^n$ for all $n$, and the interpretation sends a formula to the relation symbol naming its evaluation in $M$. This is one of the features of categorical logic: it puts the notion of "model of a theory" and "interpretation of theories" on the same footing.

Ok, so addressing your question: if a "hyperdoctrine for $\mathsf{PA}$" is a hyperdoctrine $H$ equipped with a morphism $H(\mathsf{PA})\to H$, then we have initial hyperdoctrine for $\mathsf{PA}$ (which is the syntactic hyperdoctrine $H(\mathsf{PA})$ itself) and all the standard models of $\mathsf{PA}$ in the form $H(M)$. What else? Well, we have a "hyperdoctrine for $\mathsf{PA}$" for every interpretation of $\mathsf{PA}$ into a theory $T$. For example, the standard interpretation of $\mathsf{PA}$ in $\mathsf{ZFC}$ gives a morphism of hyperdoctrines $H(\mathsf{PA})\to H(\mathsf{ZFC})$. And in a precise sense, every hyperdoctrine for $\mathsf{PA}$ has this form, since every morphism of hyperdoctrines can be viewed as an interpretation of theories. The terminal hyperdoctrine for $\mathsf{PA}$ is the interpretation of $\mathsf{PA}$ in the inconsistent theory.

So typical hyperdoctrines for $\mathsf{PA}$ include things like $H(T)$ where $T$ is a stronger theory than $\mathsf{PA}$ (obtained by adding axioms) or $H(T)$ where $T$ is an expansion of $\mathsf{PA}$ to include extra structure. In the comments, you wrote that you were hoping for something like "there's a hyperdoctrine for $\mathsf{PA}$ of only the decidable predicates". This doesn't make sense, since any hyperdoctrine for $\mathsf{PA}$ must interpret all the predicates definable in $\mathsf{PA}$, not just the decidable ones.

I've been intentionally vague about some details here (like what counts as a morphism of hyperdoctrines), hoping that a more high level view will help get your thinking on the right track.

Source Link
Alex Kruckman
  • 5k
  • 2
  • 24
  • 33

Given any theory $T$, we have a hyperdoctrine $H(T)$ (the "syntactic hyperdoctrine for $T$"), where (in the single sorted case) the $n^{\text{th}}$ lattice is the lattice of formulas in $n$ free variables, up to equivalence modulo $T$.

As Zhen Lin's answer shows, in fact every hyperdoctrine is the syntactic hyperdoctrine for some theory (the "full theory" of the hyperdoctrine).

Now what is a morphism of hyperdoctrines? It's an interpretation of theories. That is, a morphism of hyperdoctrines $H(T)\to H(T')$ gives a translation of formulas relative to $T$ into formulas relative to $T'$, which preserves the logical structure, i.e., an interpretation of $T$ in $T'$. More generally, any morphism of hyperdoctrines $H\to H'$ can be viewed as an interpretation of the full theory of $H$ in the full theory of $H'$.

When we view a traditional model $M$ of $T$ as a hyperdoctrine under $H(T)$, we form the hyperdoctrine $H(M)$ where (in the single sorted case) the $n^{\text{th}}$ lattice is $\mathcal{P}(M^n)$. And we get a morphism of hyperdoctrines $H(T)\to H(M)$ mapping a formulas relative to $T$ to its evaluation in $M$ (the set of tuples in $M$ satisfying the formula). Note that we can also view this as an interpretation of $T$ in the full theory of $M$: This theory has relation symbols for every subset of $M^n$ for all $n$, and the interpretation sends a formula to the relation symbol naming its evaluation in $M$. This is one of the features of categorical logic: it puts the notion of "model of a theory" and "interpretation of theories" on the same footing.

Ok, so addressing your question: if a "hyperdoctrine for $\mathsf{PA}$" is a hyperdoctrine $H$ equipped with a morphism $H(\mathsf{PA})\to H$, then we have initial hyperdoctrine for $\mathsf{PA}$ (which is the syntactic hyperdoctrine $H(\mathsf{PA})$ itself) and all the standard models of $\mathsf{PA}$ in the form $H(M)$. What else? Well, we have a "hyperdoctrine for $\mathsf{PA}$" for interpretation of $\mathsf{PA}$ into a theory $T$. For example, the standard interpretation of $\mathsf{PA}$ in $\mathsf{ZFC}$ gives a morphism of hyperdoctrines $H(\mathsf{PA})\to H(\mathsf{ZFC})$. And in a precise sense, every hyperdoctrine for $\mathsf{PA}$ has this form, since every morphism of hyperdoctrines can be viewed as an interpretation of theories.

So typical hyperdoctrines for $\mathsf{PA}$ include things like $H(T)$ where $T$ is a stronger theory than $\mathsf{PA}$ (obtained by adding axioms) or $H(T)$ where $T$ is an expansion of $\mathsf{PA}$ to include extra structure. In the comments, you wrote that you were hoping for something like "there's a hyperdoctrine for $\mathsf{PA}$ of only the decidable predicates". This doesn't make sense, since any hyperdoctrine for $\mathsf{PA}$ must interpret all the predicates definable in $\mathsf{PA}$, not just the decidable ones.

I've been intentionally vague about some details here (like what counts as a morphism of hyperdoctrines), hoping that a more high level view will help get your thinking on the right track.