Suppose in an arithmetic universe we have two predicates ϕ and ψ for natural numbers, satisfying a base case ϕ(0)→ψ(0) and an induction step that, for generic n, the hypothesis ϕ(n)→ψ(n) allows one to deduce ϕ(n+1)→ψ(n+1). Then it is already true in that arithmetic universe that (∀n)(ϕ(n)→ψ(n)). This is substantially harder than in a topos, where cartesian closedness allows one to form an exponential ϕ(n)→ψ(n). The principle is applied to the question of locatedness of Dedekind sections. The development analyses in some detail a notion of “subspace” of an arithmetic universe, including open or closed subspaces and a Boolean algebra generated by them. There is a lattice of subspaces generated by the open and the closed, and it is isomorphic to the free Boolean algebra over the distributive lattice of subobjects of 1 in the arithmetic universe.

### An induction principle for consequence in arithmetic universes.

#### Abstract

Suppose in an arithmetic universe we have two predicates ϕ and ψ for natural numbers, satisfying a base case ϕ(0)→ψ(0) and an induction step that, for generic n, the hypothesis ϕ(n)→ψ(n) allows one to deduce ϕ(n+1)→ψ(n+1). Then it is already true in that arithmetic universe that (∀n)(ϕ(n)→ψ(n)). This is substantially harder than in a topos, where cartesian closedness allows one to form an exponential ϕ(n)→ψ(n). The principle is applied to the question of locatedness of Dedekind sections. The development analyses in some detail a notion of “subspace” of an arithmetic universe, including open or closed subspaces and a Boolean algebra generated by them. There is a lattice of subspaces generated by the open and the closed, and it is isomorphic to the free Boolean algebra over the distributive lattice of subobjects of 1 in the arithmetic universe.
##### Scheda breve Scheda completa Scheda completa (DC)
2012
File in questo prodotto:
Non ci sono file associati a questo prodotto.
##### Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: `https://hdl.handle.net/11577/2524868`
• ND
• 6
• 4