Once upon a time there was a king who had three sons, two of whom were clever and intelligent, but the third one did not talk very much, was simple minded, and the only name they gave him was the Simpleton …
Just a few words are enough to transport us into a world of thoughts where exciting adventures with happy or sad twists await us. Even small children possess the necessary ability to remember the characters and their characteristics and relationships to one another, and it doesn’t bother us at all that the characters are described very briefly, without specifying their height, clothing, or hair color—in fact, it allows more freedom to mentally replace them with real or fictional characters.
Exactly the same skills are needed when reading a definition or a theorem with its corresponding proof in mathematics, because these are also stories: Let K be a set and let A, B, S ⊂ K. Furthermore, let A and B be countable and S be finite …
In the metalanguage \(\mathbb{M}\)ATh, mathematical stories (so-called settings) are important basic structures. They are described by one or more names for the main characters of the story (the parameters of the setting), a list of their assumed properties and interrelations in the form of mathematical statements, and a list of consequences that follow for the parameters and the objects formed from them. These basic structures can then be used to encode sets, functions, definitions, theorems, models, and theories in a common form.
For the structure of the metric space, the setting looks like this:
setting metricSpace given X:Set given d:X^2 --> X assume fact Ax1 := [forall x,y:X holds d(x,y)=0 <=> x=y] assume fact Ax2 := [forall x,y:X holds d(x,y)=d(x,y)] assume fact Ax3 := [forall x,y,z:X holds d(x,y) <= d(x,z) + d(z,y)]end
A continuation of the story then consists of additional definitions and proven statements.
develop metricSpace
prove [forall x,y:X holds d(x,y) >= 0] .. (directly) // proof steps suppressed
qed
def B(r:Rpos, x:X) := {y:X with d(y,x) < r}end
Leave a Reply