An induction principle for consequence in arithmetic universes
An 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.
- Universal Induction and True Universal Arithmetic
- scientific article; zbMATH DE number 1163362
- Induction rules in bounded arithmetic
- Enumerative induction and semi-uniform convergence to the truth
- Publication:4487300
- Inductive consequences in the calculus of constructions
- Independent Recursive Axiomatizability in Arithmetic
- Consistency of Heyting arithmetic in natural deduction
- Conditionals, quantification, and strong mathematical induction
- A universal characterization of the double powerlocale
- An extension of the Galois theory of Grothendieck
- Categorical concepts for parameterized partial specifications
- Handbook of Spatial Logics
- scientific article; zbMATH DE number 5695342 (Why is no real title available?)
- scientific article; zbMATH DE number 3904807 (Why is no real title available?)
- scientific article; zbMATH DE number 3940199 (Why is no real title available?)
- scientific article; zbMATH DE number 3959364 (Why is no real title available?)
- scientific article; zbMATH DE number 1840601 (Why is no real title available?)
- Inside every model of abstract Stone duality lies an arithmetic universe
- Limits indexed by category-valued 2-functors
- List-arithmetic distributive categories: Locoi
- Modular correspondence between dependent type theories and categories including pretopoi and topoi
- Partial Horn logic and Cartesian categories
- Quotient completion for the foundation of constructive mathematics
- Some points in formal topology.
- Sublocales in formal topology
- Topical categories of domains
- Exploring mathematical objects from custom-tailored mathematical universes
- Continuity and geometric logic
- Universal Induction and True Universal Arithmetic
- Aspects of categorical recursion theory
- Point-free construction of real exponentiation
- Fibrations of AU-contexts Beget fibrations of toposes
- Categorical structure in coherent theory of arithmetic
This page was built for publication: An induction principle for consequence in arithmetic universes
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q456884)
