tildedave
Joined 16 years ago
Joined 16 years ago
Everything gets qualified with "assuming ZFC consistent" or "assuming Peano consistent" because any inconsistent theory proves any statement. More of a proof technicality than anything too profound.
There is a construction of a model of Peano arithmetic, so it is consistent, as long as you accept the system used in the proof: https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof
Not sure if this sheds light on the parent commentator's question ... the terminology can be quite tricky.
Can't blame them missing the forest for the trees when you spend all your time writing the reducers and connectors vs the actions themselves.
I really enjoy how the subject is divorced from a lot of the modern attention demands and encourages more of a 'zen' thinking style.
As others have highlighted, it can be difficult. I work full-time as a software engineer and at the end of the day there's usually not much left in the tank in terms of "creative work". The morning is usually more productive for me - generally I'll spend 10-15 minutes on the commute in reading over the proof of some lemma or working through some computational exercise.
Things that have helped me:
- Focusing on a particular problem area rather than just "mathematics". The classical problems of Gauss and Euler tend to be more my speed than the modern mathematical problems of Hilbert or beyond. What started my journey was looking into the insolubility of the general quintic polynomial equation, something you learn in high school as a random factoid but has a lot of depth.
- Studying from small textbooks that I can fit in a backpack, so I can "make progress" during my commute. Dummit + Foote might be a great algebra reference but it's just too bulky to transport.
- Limiting the scope of how I think about the activity - my goal isn't to master these concepts on the level of a mathematics graduate student, it's more on the order of Sudoku. If I don't get something, that's okay. People spend their whole lifetimes learning this material and I'm just trying to fit this into whatever creative time I have left after the full-time job is done.
(The other answer to your question is more complete but also a bit more advanced, figured this was worth surfacing.)
Software person in RDU. It's a good life. Coq, number theory, Clojure, Golang, Ursula K. Le Guin, dad.
[ my public key: https://keybase.io/tildedave; my proof: https://keybase.io/tildedave/sigs/IE4HGc-JZRlvDHl5-o7iiIbJBzBLJH_eOu_00iF6tlU ]