An induction principle for consequence in arithmetic universes (Q456884): Difference between revisions
From MaRDI portal
Created a new Item |
Changed an Item |
||
Property / review text | |||
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. | |||
Property / review text: 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. / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: Marco Benini / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03G30 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F50 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 54B40 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
Property / zbMATH DE Number: 6094163 / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
arithmetic universes | |||
Property / zbMATH Keywords: arithmetic universes / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
induction principles | |||
Property / zbMATH Keywords: induction principles / rank | |||
Normal rank |
Revision as of 12:50, 30 June 2023
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | An induction principle for consequence in arithmetic universes |
scientific article |
Statements
An induction principle for consequence in arithmetic universes (English)
0 references
16 October 2012
0 references
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.
0 references
arithmetic universes
0 references
induction principles
0 references