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.
Finishing within the desired timeframe is completely out of question now. Please kill me.
Also, taking @bruceiv's advice to heart, I made an additive scoring system for the big proof exercise. This saved me tons of time because now I could just spend 3 minutes scanning for the 7 things you had to do to get the points instead of having to spend 10 minutes to parse all of the proof (oftentimes 3-4 pages). At least in the 85% of cases where the proof strategy was somewhat orthodox. Can recommend and will do it like this again!
OK, I found something better now. I suppose I can learn all of this in one day. Let's put this aside until the weekend (which is super close already :/)
So, it seems the lecture notes the professor uses are only half finished and in broken English (with some French bits remaining). Less than ideal.
Makes me wonder how one actually decides intuitionistic (propositional) tautologies. Tableaux won't work, right? I guess we can just search through the cut-free sequents for a formula? As far as I know, there is no nicely canonical Heyting algebra analogous to "the" Booleans we can check validity on, right?
Just asking "Hey, do you know someone who still does this that I could talk to?" seems kind of rood.
So, I've basically made no progress at all yet, except realizing that I actually made very little progress.
studying mathematical logic • ex-CS student • interested in type theory + constructive mathematics + game semantics + non-economic games • will only write code that doubles as proof
trans rights + against all unjust hierarchies