Skip to main content
fixed broken link
Source Link
Todd Trimble
  • 53.3k
  • 6
  • 205
  • 322

If $T$ is the initial such theory (which according to Wraith is PRA), with generator denoted $N$, and if $f: T \to Set$ is the unique Lawvere theory morphism sending $N$ to $\mathbb{N}$, then the functorial map $\hom_T(N^n, N) \to \hom(f(N^n), f(N)) \cong \hom(\mathbb{N}^n, \mathbb{N})$ is a surjection onto the total $n$-ary primitive recursive functions on the standard natural numbers. Is is an injection? No. For example, consider the primitive recursive "function" $G: N \to N$ defined by $G(n) = 1$ if $n$ codes the proof of a contradiction in ZFC, and $G(n) = 0$ otherwise. (This is primitive recursive because no unbounded searches are required to verify the validity of a proof.) In the standard model of arithmetic living in the ZFC model $Set$, $G$ would be sent to the constant $0$ function mapping $\mathbb{N} \to \mathbb{N}$. But we could equally consider a model $\mathcal{M}$ of $ZFC + \neg Con(ZFC)$ and its natural number object $\mathbb{N}_\mathcal{M}$, in which $G$ would not be sent to the constant $0$ function. Thus $G$ and the constant $0$ function must be distinct in the category $T$. (Thanks to Zhen Lin Low for supplying this argument, herehere.)

If $T$ is the initial such theory (which according to Wraith is PRA), with generator denoted $N$, and if $f: T \to Set$ is the unique Lawvere theory morphism sending $N$ to $\mathbb{N}$, then the functorial map $\hom_T(N^n, N) \to \hom(f(N^n), f(N)) \cong \hom(\mathbb{N}^n, \mathbb{N})$ is a surjection onto the total $n$-ary primitive recursive functions on the standard natural numbers. Is is an injection? No. For example, consider the primitive recursive "function" $G: N \to N$ defined by $G(n) = 1$ if $n$ codes the proof of a contradiction in ZFC, and $G(n) = 0$ otherwise. (This is primitive recursive because no unbounded searches are required to verify the validity of a proof.) In the standard model of arithmetic living in the ZFC model $Set$, $G$ would be sent to the constant $0$ function mapping $\mathbb{N} \to \mathbb{N}$. But we could equally consider a model $\mathcal{M}$ of $ZFC + \neg Con(ZFC)$ and its natural number object $\mathbb{N}_\mathcal{M}$, in which $G$ would not be sent to the constant $0$ function. Thus $G$ and the constant $0$ function must be distinct in the category $T$. (Thanks to Zhen Lin Low for supplying this argument, here.)

If $T$ is the initial such theory (which according to Wraith is PRA), with generator denoted $N$, and if $f: T \to Set$ is the unique Lawvere theory morphism sending $N$ to $\mathbb{N}$, then the functorial map $\hom_T(N^n, N) \to \hom(f(N^n), f(N)) \cong \hom(\mathbb{N}^n, \mathbb{N})$ is a surjection onto the total $n$-ary primitive recursive functions on the standard natural numbers. Is is an injection? No. For example, consider the primitive recursive "function" $G: N \to N$ defined by $G(n) = 1$ if $n$ codes the proof of a contradiction in ZFC, and $G(n) = 0$ otherwise. (This is primitive recursive because no unbounded searches are required to verify the validity of a proof.) In the standard model of arithmetic living in the ZFC model $Set$, $G$ would be sent to the constant $0$ function mapping $\mathbb{N} \to \mathbb{N}$. But we could equally consider a model $\mathcal{M}$ of $ZFC + \neg Con(ZFC)$ and its natural number object $\mathbb{N}_\mathcal{M}$, in which $G$ would not be sent to the constant $0$ function. Thus $G$ and the constant $0$ function must be distinct in the category $T$. (Thanks to Zhen Lin Low for supplying this argument, here.)

updated to include precise references
Source Link
Todd Trimble
  • 53.3k
  • 6
  • 205
  • 322

It should be possible. This is going a bit outAccording to unpublished notes by Gavin Wraith ("Notes on a limb because I haven't gone through all the details carefullyarithmetic universes and Gödel incompleteness theorems" (1985)), but anyway it is my impression that PRA can be described as an equational theory or as a Lawvere theory, and is abstractly characterized as initial among all Lawvere theories whose generating object is a parametrized natural numbers object. (For some details on Wraith's notes, see Alan Morrison's Master's Thesis; see particularly chapter 5.)

I'm pretty confident that ifIf $T$ is the initial such theory (which I assertaccording to Wraith is PRA), with generator denoted $N$, and if $f: T \to Set$ is the unique Lawvere theory morphism sending $N$ to $\mathbb{N}$, then the functorial map $\hom_T(N^n, N) \to \hom(f(N^n), f(N)) \cong \hom(\mathbb{N}^n, \mathbb{N})$ is a surjection onto the total $n$-ary primitive recursive functions on the standard natural numbers. Is is an injection? No. For example, consider the primitive recursive "function" $G: N \to N$ defined by $G(n) = 1$ if $n$ codes the proof of a contradiction in ZFC, and $G(n) = 0$ otherwise. (This is primitive recursive because no unbounded searches are required to verify the validity of a proof.) In the standard model of arithmetic living in the ZFC model $Set$, $G$ would be sent to the constant $0$ function mapping $\mathbb{N} \to \mathbb{N}$. But we could equally consider a model $\mathcal{M}$ of $ZFC + \neg Con(ZFC)$ and its natural number object $\mathbb{N}_\mathcal{M}$, in which $G$ would not be sent to the constant $0$ function. Thus $G$ and the constant $0$ function must be distinct in the category $T$. (Thanks to Zhen Lin Low for supplying this argument, here.)

It should be possible. This is going a bit out on a limb because I haven't gone through all the details carefully, but anyway it is my impression that PRA can be described as an equational theory or as a Lawvere theory, and is abstractly characterized as initial among all Lawvere theories whose generating object is a parametrized natural numbers object.

I'm pretty confident that if $T$ is the initial such theory (which I assert is PRA), with generator denoted $N$, and if $f: T \to Set$ is the unique Lawvere theory morphism sending $N$ to $\mathbb{N}$, then the functorial map $\hom_T(N^n, N) \to \hom(f(N^n), f(N)) \cong \hom(\mathbb{N}^n, \mathbb{N})$ is a surjection onto the total $n$-ary primitive recursive functions on the standard natural numbers. Is is an injection? No. For example, consider the primitive recursive "function" $G: N \to N$ defined by $G(n) = 1$ if $n$ codes the proof of a contradiction in ZFC, and $G(n) = 0$ otherwise. (This is primitive recursive because no unbounded searches are required to verify the validity of a proof.) In the standard model of arithmetic living in the ZFC model $Set$, $G$ would be sent to the constant $0$ function mapping $\mathbb{N} \to \mathbb{N}$. But we could equally consider a model $\mathcal{M}$ of $ZFC + \neg Con(ZFC)$ and its natural number object $\mathbb{N}_\mathcal{M}$, in which $G$ would not be sent to the constant $0$ function. Thus $G$ and the constant $0$ function must be distinct in the category $T$. (Thanks to Zhen Lin Low for supplying this argument, here.)

According to unpublished notes by Gavin Wraith ("Notes on arithmetic universes and Gödel incompleteness theorems" (1985)), PRA can be described as an equational theory or as a Lawvere theory, and is abstractly characterized as initial among all Lawvere theories whose generating object is a parametrized natural numbers object. (For some details on Wraith's notes, see Alan Morrison's Master's Thesis; see particularly chapter 5.)

If $T$ is the initial such theory (which according to Wraith is PRA), with generator denoted $N$, and if $f: T \to Set$ is the unique Lawvere theory morphism sending $N$ to $\mathbb{N}$, then the functorial map $\hom_T(N^n, N) \to \hom(f(N^n), f(N)) \cong \hom(\mathbb{N}^n, \mathbb{N})$ is a surjection onto the total $n$-ary primitive recursive functions on the standard natural numbers. Is is an injection? No. For example, consider the primitive recursive "function" $G: N \to N$ defined by $G(n) = 1$ if $n$ codes the proof of a contradiction in ZFC, and $G(n) = 0$ otherwise. (This is primitive recursive because no unbounded searches are required to verify the validity of a proof.) In the standard model of arithmetic living in the ZFC model $Set$, $G$ would be sent to the constant $0$ function mapping $\mathbb{N} \to \mathbb{N}$. But we could equally consider a model $\mathcal{M}$ of $ZFC + \neg Con(ZFC)$ and its natural number object $\mathbb{N}_\mathcal{M}$, in which $G$ would not be sent to the constant $0$ function. Thus $G$ and the constant $0$ function must be distinct in the category $T$. (Thanks to Zhen Lin Low for supplying this argument, here.)

Source Link
Todd Trimble
  • 53.3k
  • 6
  • 205
  • 322

It should be possible. This is going a bit out on a limb because I haven't gone through all the details carefully, but anyway it is my impression that PRA can be described as an equational theory or as a Lawvere theory, and is abstractly characterized as initial among all Lawvere theories whose generating object is a parametrized natural numbers object.

This statement may take a bit of unpacking. Lawvere theories are a way of doing universal algebra categorically. Formally, a Lawvere theory is a category $T$ with finite products together with a product-preserving functor $\Phi: \text{Fin}^{op} \to T$ that is a bijection on objects. Here $\text{Fin}$ is the category whose objects are finite cardinals $k = \{0, \ldots, k-1\}$ and whose morphisms are functions between them. The cardinal $1$ generates (the objects of) $\text{Fin}$ by taking finite coproducts of copies of $1$; similarly it generates $\text{Fin}^{op}$ under finite products. Thus the special object $x = \Phi(1)$ generates the objects of $T$ by taking finite products: every object of $T$ is of the form $x^n$. General morphisms $x^n \to x^m$ are $m$-tuples of morphisms $x^n \to x$; we think of the morphisms $x^n \to x$ in $T$ as parametrizing the definable $n$-ary operations of an equational theory. [This categorical description of equational theories is closely related to the concept of clone. If you accept that every equational theory gives rise to a finitary monad on $Set$, then the corresponding Lawvere theory is the category opposite to the finitary Kleisli category consisting of finitely generated free objects. But this is a somewhat hurried discussion which I'll cut short here.] A morphism $F: S \to T$ is a product-preserving functor which is compatible with the given product-preserving functors $\text{Fin}^{op} \to S$ and $\text{Fin}^{op} \to T$.

A parametrized natural numbers object in a category with finite products $\mathbf{C}$ is an object $N$ that comes equipped with maps $z: 1 \to N$ (here $1$ denotes the terminal object, and read '$z$' as 'zero') and $s: N \to N$ (successor), such that given any objects $A, X$ of $\mathbf{C}$ and maps $f: A \to X$, $g: X \to X$, there exists a unique map $h: N \times A \to X$ such that the following diagram commutes:

$$\begin{array}{ccc} A & \stackrel{\langle z \circ !, 1_A\rangle}{\to} & N \times A & \stackrel{s \times 1_A}{\leftarrow} & N \times A \\ & f \searrow & \downarrow h & & \downarrow h \\ & & X & \underset{g}{\leftarrow} & X \end{array}$$

(here $!$ denotes the unique map $A \to 1$). This axiom is what you need to internalize primitive recursion in a category with finite products.

So now the Lawvere theories we are interested in are those for which the generator $x = \Phi(1)$ is a parametrized natural numbers object. A concrete example of such is the full subcategory of $Set$ whose objects are finite powers $\mathbb{N}^n$ of the set of natural numbers. For that matter, for any category with finite products and a natural numbers object $N$ (for example, a Grothendieck topos), you can cook up a Lawvere theory by considering the full subcategory consisting of finite powers of $N$. Or, the subcategory needn't be full: just retain enough arrows to retain finite product structure and primitive recursive structure guaranteed by the axiom of parametrized NNO's.

Finally, we are interested in the initial such Lawvere theory. As is the case with any initial algebraic object, the explicit construction is syntactic: we start with $N$ and $z: 1 \to N$ and $s: N \to N$ and use the axiom of parametrized NNO's together with finite cartesian product structure (products of copies of $N$, projection maps, diagonal maps) and categorical composition to generate formally all the arrows. (As a simple exercise, show how to construct formal addition and formal multiplication on $N$.) One thing to check is that morphisms $1 \to N$ (the definable constants of the equational theory, considered up to provable equality) correspond bijectively to standard natural numbers.

I'm pretty confident that if $T$ is the initial such theory (which I assert is PRA), with generator denoted $N$, and if $f: T \to Set$ is the unique Lawvere theory morphism sending $N$ to $\mathbb{N}$, then the functorial map $\hom_T(N^n, N) \to \hom(f(N^n), f(N)) \cong \hom(\mathbb{N}^n, \mathbb{N})$ is a surjection onto the total $n$-ary primitive recursive functions on the standard natural numbers. Is is an injection? No. For example, consider the primitive recursive "function" $G: N \to N$ defined by $G(n) = 1$ if $n$ codes the proof of a contradiction in ZFC, and $G(n) = 0$ otherwise. (This is primitive recursive because no unbounded searches are required to verify the validity of a proof.) In the standard model of arithmetic living in the ZFC model $Set$, $G$ would be sent to the constant $0$ function mapping $\mathbb{N} \to \mathbb{N}$. But we could equally consider a model $\mathcal{M}$ of $ZFC + \neg Con(ZFC)$ and its natural number object $\mathbb{N}_\mathcal{M}$, in which $G$ would not be sent to the constant $0$ function. Thus $G$ and the constant $0$ function must be distinct in the category $T$. (Thanks to Zhen Lin Low for supplying this argument, here.)