nLab arithmetic pretopos

Redirected from "list-arithmetic pretoposes".
Contents

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Arithmetic

Contents

Idea

An arithmetic pretopos is a pretopos CC with a parameterized natural numbers object. A list-arithmetic pretopos is a pretopos with all parameterized list objects (Maietti 10, 2.6).

Using the (equivalent) definition given in Cockett 1990, a parameterized list object is a W-type for the polynomial functor B+A×():CCB+ A\times(-)\colon C\to C. This definition makes sense since a pretopos has finite products and disjoint coproducts (here denoted “++”).

Discussion via its internal language, which is a dependent type theory… (Maietti 05, Maietti 10, p.6).

Maietti (05,10) proposed that list-arithmetic pretoposes serve as the arithmetic universes that André Joyal (cf. Joyal 05) once suggested to use for discussion of incompleteness theorems (cf. van Dijk/Oldenziel 2020); they are used directly as the definition of arithmetic universes e.g. in (Maietti-Vickers 2012).

First-order Peano arithmetic

In classical logic, first-order Peano arithmetic is often called “PA”. Unlike second-order Peano arithmetic, this theory does not have a unique model up to isomorphism in the category of sets: there is an initial model, called the ‘standard’ model of the natural numbers, but also others called ‘nonstandard’. It is interesting to ask how we can rephrase and also generalize PA using the concept of arithmetic pretopos. The following is a tentative proposal put forth by Sridhar Ramesh:

Let me expand on why the initial Heyting/Boolean pretopos with a parametrized NNO is equivalent to first-order intuitionistic/classical PA. [By intuitionistic PA, I mean the same thing as what is standardly called Heyting Arithmetic.]

Remember, intuitionistic/classical PA is the first-order intuitionistic/classical theory with a sort NN, a zero element 0:N0 : N, a successor function S:NNS : N \to N, operations +:N×NN+ : N \times N \to N and ×:N×NN\times : N \times N \to N, axioms stating that SS is injective, 00 is not in the range of SS, recurrence identities x+0=xx + 0 = x, x+S(y)=S(x+y)x + S(y) = S(x + y), x×0=0x \times 0 = 0, x×S(y)=x×y+xx \times S(y) = x \times y + x, and the induction schema, which says any definable (in the sense of first-order definable in this language by a relation with parameters) subset of NN which contains 00 and is closed under SS must contain all of NN.

So, let’s see that a Heyting/Boolean pretopos with parameterized NNO proves everything first-order intuitionistic/classical PA proves: An NNO is an initial algebra for the T1+TT \mapsto 1 + T endofunctor, and thus by Lambek’s lemma, we obtain an isomorphism between 1+N1 + N and NN, where NN is the carrier of the NNO and the isomorphism is given by the combination of zero and successor. This being an isomorphism says in the internal language of the pretopos that every element of NN is precisely one of zero or a successor (not both; thus, 00 is not in the range of the successor map) and that the successor map is injective.

Furthermore, our recurrence identities for ++ and ×\times directly describe how to define unique operators satisfying those recurrences on a parametrized NNO.

Finally, note that Heyting pretoposes are “closed under” first-order definability, so to speak (this is their raison d’être as a concept), so that any first-order definable relation R(n,x)R(n, x) on NN and some other tuples of sorts XX in this language will correspond to some subobject of N×XN \times X in this pretopos. The set {x:XR(0,x)n:N(R(n,x)R(S(n),x))}\{x : X \mid R(0, x) \wedge \forall n : N \left( R(n, x) \Rightarrow R(S(n), x) \right) \} is first-order definable as a subobject of XX in this pretopos, and by passing to the slice category over it, we obtain another pretopos, where NN remains an NNO. In this slice pretopos, {n:NR(n,x)}\{n : N \mid R(n, x) \} is a subobject of NN which contains 00 and is closed under SS; thus, a sub-algebra of NN as algebras for the T1+TT \mapsto 1 + T endofunctor. But as NN is an initial algebra, it is isomorphic to this subalgebra (any subobject of an initial object is isomorphic to the initial object). Thus, in this slice pretopos over {x:XR(0,x)n:N(R(n,x)R(S(n),x))}\{x : X \mid R(0, x) \wedge \forall n : N \left( R(n, x) \Rightarrow R(S(n), x) \right) \}, we have established n:N,R(n,x)\forall n : N, R(n, x), which amounts to having established the parametrized induction schema in our original pretopos.

Given the closure of Heyting/Boolean pretoposes under the derivations of first-order intuitionistic/classical logic, this concludes showing that a Heyting/Boolean pretopos with parametrized NNO proves in its internal language everything that first-order intuitionistic/classical PA does.

In the other direction, it’s well-known how any first-order intuitionistic/classical logical theory gives rise to a Heyting/Boolean pretopos as its “syntactic category” in a suitable sense. We’ve just seen that when we apply this construction to first-order intuitionistic/classical PA, we get something “no stronger” than the initial Heyting/Boolean pretopos with a parametrized NNO. But what may not be obvious is that these are indeed equal; that we actually get the full structure of an NNO in the syntactic category for PA.

The induction schema guarantees the uniqueness aspect of algebra maps out of NN, but their existence is not obvious. This existence however is granted by Gödel’s Chinese remainder theorem trick showing how “primitive recursions” of functions from naturals to tuples of naturals can be defined in a first-order way using ++ and ×\times.

References

Last revised on May 28, 2024 at 16:45:05. See the history of this page for a list of all contributions to it.