An induction principle for consequence in arithmetic universes

Research output: Contribution to journalArticlepeer-review

Standard

An induction principle for consequence in arithmetic universes. / Vickers, Steven; Maietti, Maria Emilia.

In: Journal of Pure and Applied Algebra, Vol. 216, No. 8-9, 01.08.2012, p. 2049-2067.

Research output: Contribution to journalArticlepeer-review

Harvard

APA

Vancouver

Author

Vickers, Steven ; Maietti, Maria Emilia. / An induction principle for consequence in arithmetic universes. In: Journal of Pure and Applied Algebra. 2012 ; Vol. 216, No. 8-9. pp. 2049-2067.

Bibtex

@article{518aa30dc4034b8fa506235f329198b3,
title = "An induction principle for consequence in arithmetic universes",
abstract = "Suppose in an arithmetic unverse 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 opens and the closeds, and it is isomorphic to the free Boolean algebra over the distributive lattice of subobjects of 1 in the arithmetic universe.",
author = "Steven Vickers and Maietti, {Maria Emilia}",
year = "2012",
month = aug,
day = "1",
doi = "10.1016/j.jpaa.2012.02.040",
language = "English",
volume = "216",
pages = "2049--2067",
journal = "Journal of Pure and Applied Algebra",
issn = "0022-4049",
publisher = "Elsevier",
number = "8-9",

}

RIS

TY - JOUR

T1 - An induction principle for consequence in arithmetic universes

AU - Vickers, Steven

AU - Maietti, Maria Emilia

PY - 2012/8/1

Y1 - 2012/8/1

N2 - Suppose in an arithmetic unverse 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 opens and the closeds, and it is isomorphic to the free Boolean algebra over the distributive lattice of subobjects of 1 in the arithmetic universe.

AB - Suppose in an arithmetic unverse 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 opens and the closeds, and it is isomorphic to the free Boolean algebra over the distributive lattice of subobjects of 1 in the arithmetic universe.

U2 - 10.1016/j.jpaa.2012.02.040

DO - 10.1016/j.jpaa.2012.02.040

M3 - Article

VL - 216

SP - 2049

EP - 2067

JO - Journal of Pure and Applied Algebra

JF - Journal of Pure and Applied Algebra

SN - 0022-4049

IS - 8-9

ER -