Here's the quote justifying my weird username. It's from Dedekind's "Was sind und was sollen die Zahlen" ("What are numbers and what are they good for?").
"But I know that, in the shadowy forms which I bring before him, many a reader will scarcely recognize his numbers which all his life long have accompanied him as faithful and familiar friends; he will be frightened by the long series of simple inferences corresponding to our step-by-step understanding [ger. Treppenverstand], by the matter-of-fact dissection of the chains of reasoning on which the laws of numbers depend [...]"
The term thus characterizes our capability of reasoning to be restricted to discrete steps and is meant to contrast the rather informal, intuition-based proofs that were the norm back in 1888 when the paper was written.
It is also a very funny sounding word.
But just spelling this out already makes it clear that that's *way* too good to be true. At least it's nice to know that all the recursive ordinals I need to care about are path's through Kleene's O...
Sadly, the proof is not effective. It would slap if I could just pass decidable well-ordering to some function and it would compute me a Kleene ordinal coding of the order type.
Erratum: looking at my source (logicomix), Hilbert said "In mathemathics, there is no ignorabimus", meaning there is no "we shall not know". Leibniz says calculemus.
The modern computerized-proof world is such a delicious mashup of the arch-rivals Hilbert and Poincare.
Hilbert had a grand dream that when two people disagreed, they could just say "calculamebus" (let us calculate), yet this was married to the "analytic" viewpoint of set theory. Poincare had a disdain for logic, and yet still championed a "synthetic" viewpoint that was key for the development of constructive mathematics!
The modern proof assistant owes a debt to both.
@ionchy well, I think the idea isn't that what we find is absolute truth but rather that there is some abstract absolute truth. think of the sense of wonder you first experienced when discovering curry-howard, connections between seemingly unrelated areas. isn't it compelling to think that there is some higher abstract form of mathematical truth which escapes us and our models? I don't think like this myself, but I am tempted to every now and then..
Grothendieck revolutionized mathematics. Then he disappeared. He became a hermit, living in a stone hut and taking a vow of silence.
There's a great story about him here. And a conference about him next week!
(1/n)
I have been convinced to give the presentation. I just hope they won't be mean to my face about it!
RT @blackpooltower
Love this Le Guin quote in @jamesbridle fascinating new book, which explores “an ecology of technology”
(cc @CarbonCycleKate )
I'm a real logician now! • recovering computer scientist • interested in proof theory + constructive mathematics + type theory • will only write code that compiles into a pdf document or doubles as proof
trans rights + against all unjust hierarchies