Das Kalenderblatt 091103

Our contemporary orthodoxy: to show that there are so-and-sos is to
prove "so-and-sos exist" from the axioms of set theory. {{Man beachte:
contemporary = heutig, zeitgenössisch, modern - im Gegensatz zu
dauerhaft, zeitlos, unveränderlich}}
[Penelope Maddy: "Mathematical Existence", Bull. Symbolic Logic 11
(2005) 351]
http://www.jstor.org/pss/1578738

Inspired by Whitehead and Russell's monumental Principia Mathematica,
the Metamath Proof Explorer has over 8,000 completely worked out
proofs, starting from the very foundation that mathematics is built on
and eventually arriving at familiar mathematical facts and beyond.
Each proof is pieced together with razor-sharp precision {{schon mal
eine Rasierklinge unter dem Mikroskop betrachtet?}} using a simple
substitution rule that practically anyone (with lots of patience) can
follow, not just mathematicians. Every step can be drilled down deeper
and deeper into the labyrinth until axioms of logic and set theory—the
starting point for all of mathematics {{Das ist pure Ideologie. Die
Behauptung ist ebenso tendenziös wie falsch und galt allenfalls
solange "die Mitläufer Bourbakis das Sagen in der Mathematik hatten
mit dem Schlachtruf: Alle Mathematik ist Mengenlehre. Diese Auffassung
von der Mathematik beherrschte aber bisher nur eine relativ kurze
Episode von einem Jahrhundert in der langen Geschichte der
Mathematik" [D. Laugwitz: "Zahlen und Kontinuum", BI (1988) p. 99]}} —
will ultimately be found at the bottom. You could spend literally days
exploring the astonishing tangle of logic leading, say, from the
seemingly mundane theorem 2+2=4 back to these axioms.
Essentially everything that is possible to know in mathematics can be
derived from a handful of axioms known as Zermelo-Fraenkel set theory,
{{including the binary tree? Da scheint's noch zu hapern - wie
überall, wo Widersprüche lauern}} which is the culmination of many
years of effort to isolate the essential nature of mathematics and is
one of the most profound achievements of mankind {{why should not
another see it as a joke? (Wittgenstein) - wieder andere betrachten es
als einen Schandfleck auf der Geistesgeschichte der Menschheit.}}
The Metamath Proof Explorer starts with these axioms to build up its
proofs. There may be symbols that are unfamiliar to you, but we show
in detail how they are manipulated in the proofs, and in principle you
don't have to know what they mean. In fact, there is a philosophy
called formalism which says that mathematics is a game of symbols with
no intrinsic meaning. {{In fact there is a philosophy called
MatheRealism which says that formalism is not a philosophy.}} With
that in mind, Metamath lets you watch the game being played and the
pieces manipulated according to simple and precise rules, one step at
a time. {{Was nützt die Präzision, wenn das Ergebnis falsch ist? Was
nützen die Beteuerungen der Henne, wenn das Ei faul ist?}}
http://us.metamath.org/mpegif/mmset.html
http://us.metamath.org/mpegif/mmset.html
http://www.topology.org/sci/maths.html

Gruß, WM
[ Auf dieses Posting antworten ]