Specker sequence
http://dbpedia.org/resource/Specker_sequence
Une suite de Specker est un contre-exemple dans les mathématiques constructives à certains théorèmes établis dans l'analyse classique. Il s'agit d'une suite de nombres rationnels qui est calculable, croissante, et majorée, mais dont la limite n'est pas un nombre réel calculable, ce qui (en mathématiques constructives) contredit le théorème de la limite monotone. Ces suites furent découvertes en 1949 par le mathématicien zurichois Ernst Specker (1920-2011).
rdf:langString
In der Berechenbarkeitstheorie ist die Specker-Folge eine berechenbare, monoton wachsende, beschränkte Folge von rationalen Zahlen, deren Supremum keine berechenbare reelle Zahl ist. Das erste Beispiel einer solchen Folge wurde 1949 von Ernst Specker konstruiert. Die Supremumseigenschaft wurde auch im Bereich der reversen Mathematik untersucht, wo ihre genaue Stärke bestimmt wurde. In der Sprache der Disziplin ausgedrückt ist die Supremumseigenschaft äquivalent zu ACA0 über RCA0.
rdf:langString
In computability theory, a Specker sequence is a computable, monotonically increasing, bounded sequence of rational numbers whose supremum is not a computable real number. The first example of such a sequence was constructed by Ernst Specker (1949).
rdf:langString
rdf:langString
Specker-Folge
rdf:langString
Suite de Specker
rdf:langString
Specker sequence
xsd:integer
21535918
xsd:integer
1093027785
rdf:langString
In der Berechenbarkeitstheorie ist die Specker-Folge eine berechenbare, monoton wachsende, beschränkte Folge von rationalen Zahlen, deren Supremum keine berechenbare reelle Zahl ist. Das erste Beispiel einer solchen Folge wurde 1949 von Ernst Specker konstruiert. Die Existenz von Specker-Folgen hat Konsequenzen für die . Die Tatsache, dass es solche Folgen gibt, bedeutet, dass die Klasse der berechenbaren reellen Zahlen nicht die aus der reellen Analysis bekannte Supremumseigenschaft aufweist, selbst dann, wenn man sich dabei auf berechenbare Folgen beschränkt. Ein üblicher Weg, dieses Problem zu lösen, ist, nur berechenbare Folgen versehen mit einem berechenbaren Konvergenzmodul zu betrachten. Keine Specker-Folge hat einen berechenbaren Konvergenzmodul, das bedeutet: Jeder Konvergenzmodul einer Specker-Folge wächst schneller als jede berechenbare Funktion, sonst ließe sich auf berechenbare Weise abschätzen, nach wie vielen Folgengliedern die ersten Stellen feststehen, und damit wäre das Supremum eine berechenbare reelle Zahl. Die Supremumseigenschaft wurde auch im Bereich der reversen Mathematik untersucht, wo ihre genaue Stärke bestimmt wurde. In der Sprache der Disziplin ausgedrückt ist die Supremumseigenschaft äquivalent zu ACA0 über RCA0.
rdf:langString
Une suite de Specker est un contre-exemple dans les mathématiques constructives à certains théorèmes établis dans l'analyse classique. Il s'agit d'une suite de nombres rationnels qui est calculable, croissante, et majorée, mais dont la limite n'est pas un nombre réel calculable, ce qui (en mathématiques constructives) contredit le théorème de la limite monotone. Ces suites furent découvertes en 1949 par le mathématicien zurichois Ernst Specker (1920-2011).
rdf:langString
In computability theory, a Specker sequence is a computable, monotonically increasing, bounded sequence of rational numbers whose supremum is not a computable real number. The first example of such a sequence was constructed by Ernst Specker (1949). The existence of Specker sequences has consequences for computable analysis. The fact that such sequences exist means that the collection of all computable real numbers does not satisfy the least upper bound principle of real analysis, even when considering only computable sequences. A common way to resolve this difficulty is to consider only sequences that are accompanied by a modulus of convergence; no Specker sequence has a computable modulus of convergence. More generally, a Specker sequence is called a recursive counterexample to the least upper bound principle, i.e. a construction that shows that this theorem is false when restricted to computable reals. The least upper bound principle has also been analyzed in the program of reverse mathematics, where the exact strength of this principle has been determined. In the terminology of that program, the least upper bound principle is equivalent to ACA0 over RCA0. In fact, the proof of the forward implication, i.e. that the least upper bound principle implies ACA0, is readily obtained from the textbook proof (see Simpson, 1999) of the non-computability of the supremum in the least upper bound principle.
xsd:nonNegativeInteger
5123
