An induction principle for consequence in arithmetic universes.

*(English)*Zbl 1253.03099An arithmetic universe is a pretopos in which there is an object \(\mathsf{List}(A)\) with the obvious constructors and a recursion predicate, all of them encoded as suitable arrows. In this context, the article proves that, given two predicates \(\phi\) and \(\psi\) for natural numbers satisfying a base case \(\phi(0) \to \psi(0)\) and an induction step that, for generic \(n\), the hypothesis \(\phi(n) \to \psi(n)\) allows one to deduce \(\phi(n + 1) \to \psi(n + 1)\), then it is already true in that arithmetic universe that \((\forall n)(\phi(n) \to \psi(n))\). Since arithmetic universes, being pretoposes, do not have exponentiation in general, this induction principle is substantially harder to prove than in a topos. The development is interesting in itself as it analyses a notion of “subspace” of an arithmetic universe, including open and closed subspaces and a Boolean algebra generated by them. Hence, the work provides some “topological” insight in the theory of arithmetic universes which could be of interest beyond the specific result in the article. The paper concludes with the application of the induction principle to locatedness of Dedekind sections: once again, the topological nature of the induction principle in the considered context becomes evident, making the example both clarifying and potentially inspiring.

Reviewer: Marco Benini (Buccinasco)

##### MSC:

03G30 | Categorical logic, topoi |

03F50 | Metamathematics of constructive systems |

54B40 | Presheaves and sheaves in general topology |

PDF
BibTeX
XML
Cite

\textit{M. E. Maietti} and \textit{S. Vickers}, J. Pure Appl. Algebra 216, No. 8--9, 2049--2067 (2012; Zbl 1253.03099)

Full Text:
DOI

**OpenURL**

##### References:

[1] | Barr, M.; Wells, C., Toposes, triples and theories, (1984), Springer-Verlag, reissued as [2] · Zbl 0567.18001 |

[2] | M. Barr, C. Wells, Toposes, Triples and Theories, Reprints in Theory and Applications of Categories, no. 12, Theory and Applications of Categories, Mount Allison University, 2005, originally published as [1]. |

[3] | Claßen, I.; Große-Rhode, M.; Wolter, U., Categorical concepts for parameterized partial specifications, Mathematical structures in computer science, 5, 2, 153-188, (1995) · Zbl 0909.18002 |

[4] | Cockett, J.R., List-arithmetic distributive categories: locoi, Journal of pure and applied algebra, 66, 1-29, (1990) · Zbl 0715.18005 |

[5] | Johnstone, P.T., Stone spaces, () · Zbl 0586.54001 |

[6] | Johnstone, P.T., () |

[7] | Johnstone, P.T., () |

[8] | A. Joyal, The Gödel incompleteness theorem: a categorical approach, Cahiers de Topologie et Géométrie Différentielle Catégorique 16 (2005), no. 3, Short abstract of the talk given at the International Conference Charles Ehresmann: 100 ans, Amiens, 7-9 October 2005. |

[9] | Joyal, A.; Tierney, M., An extension of the Galois theory of Grothendieck, Memoirs of the American mathematical society, 309, (1984) · Zbl 0541.18002 |

[10] | Lambek, J.; Scott, P.J., Introduction to higher-order categorical logic, (1986), Cambridge University Press · Zbl 0596.03002 |

[11] | Maietti, Maria Emilia, Modular correspondence between dependent type theories and categories including pretopoi and topoi, Mathematical structures in computer science, 15, 6, 1089-1149, (2005) · Zbl 1093.03042 |

[12] | Maietti, Maria Emilia, Joyal’s arithmetic universe as List-arithmetic pretopos, Theory and applications of categories, 24, 3, 39-83, (2010) · Zbl 1245.03111 |

[13] | Maria Emilia Maietti, Subspaces of arithmetic universes via type theory, Available via http://www.math.unipd.it/ maietti/, 2010. · Zbl 1245.03111 |

[14] | Maria Emilia Maietti, Giuseppe Rosolini, Quotient completion for the foundation of constructive mathematics, Logica Universalis (2012), (in press) Available via http://arxiv.org/abs/1202.1012. · Zbl 1288.03049 |

[15] | Palmgren, Erik; Vickers, Steven, Partial Horn logic and Cartesian categories, Annals of pure and applied logic, 145, 3, 314-353, (2007) · Zbl 1109.03022 |

[16] | G. Sambin, The Basic Picture and Positive Topology. New structures for Constructive Mathematics, Oxford University Press, (in press). |

[17] | Sambin, Giovanni, Some points in formal topology, Theoretical computer science, 305, 347-408, (2003) · Zbl 1044.54001 |

[18] | Street, Ross, Limits indexed by category-valued 2-functors, Journal of pure and applied algebra, 8, 149-181, (1976) · Zbl 0335.18005 |

[19] | Taylor, Paul, Inside every model of abstract stone duality lies an arithmetic universe, (), 247-296 · Zbl 1272.03165 |

[20] | Vickers, Steven, Topical categories of domains, Mathematical structures in computer science, 9, 569-616, (1999) · Zbl 0946.18001 |

[21] | Vickers, Steven, Locales and toposes as spaces, (), 429-496 |

[22] | Vickers, Steven, Sublocales in formal topology, Journal of symbolic logic, 72, 2, 463-482, (2007) · Zbl 1132.03033 |

[23] | Vickers, S.J.; Townsend, C.F., A universal characterization of the double powerlocale, Theoretical computer science, 316, 297-321, (2004) · Zbl 1047.06006 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.