It would be nice to digest the essential works on constructive mathematics and logic. Which works are the most interesting examples of the constructive view on math? Which ones could be the most interesting for a neophyte?
Posted Aug 5, 2018, 11:44 AM UTC
This really depends on what you're interests are in relation to constructive mathematics. I can't speak too well on the philosophical view other than to say read bishop although he is outdated.
Anything on intuitionistic logic and the curry-howard correspondence/isomorphism and lambda calculus, should be a basic start for getting you in the door.
Also, and I'm a little biased in this regard but categorical logic is where it's at, an introduction to higher order categorical logic by Phillip Scott is decent in this regard allbet also old and I'm sure there are better newer books out there. Basic categorical constructions fit the bill for modeling constructive logic perfectly.
[deleted]
Well, I'm quite familiar with the logic part, I've read these books by Lof and Girard. What is really a terra incognita for me is everything beyond reasoning about integers and simple inductive types. Elements of Intuitionism also seems quite like what I was looking for.
If what you're interested in is types, I'd recommend giving the Homotopy Type Theory Book a read. It's not a good introduction to the philosophy of constructive mathematics nor does it develop things like constructive analysis in depth, but it's super interesting and will give you a good understanding of modern type theory (modernish, since it doesn't cover the newest hotness like cubical type theory)
There are also Notes on Constructive Set Theory by Azcel and Rathjen, and Real Analysis: A Constructive Approach by Bridger. For a more informal approach, you could try Constructivism: A Realistic Approach by Maloney. As a different sort of read, one of the big differences with intuitionism is the lack of the Axiom of Choice. There's a book called The Axiom of Choice by Jech. You could look into that to see some things that are no longer provable.
You could just read the homotopy type theory book
That's a pretty broad question.
Introductory (for the most part) and strictly about constructive mathematics:
[paper, 18 pages] Five Stages Of Accepting Constructive Mathematics by Andrej Bauer. (start with that and the online article)
[online article] Internet Encyclopedia of Philosophy - Constructive Mathematics
[book] Constructivism in Mathematics, an Introduction by A.S. Troelstra and D. Van Dalen
[book] Foundations of Constructive Mathematics by Michael J. Beeson
[book] Foundations of Constructive Analysis by E. Bishop
[paper, 32 pages] History of constructivism in the 20th century by A.S. Troelstra
[paper, 19 pages] Relationship between Constructive, Predicative and Classical Systems of Analysis by Solomon Feferman
More advanced and/or relevant/related:
[book] Proofs and types by Jean-Yves Girard
[paper] Constructive Mathematics And Computer Programming by Per Martin-Löf
[lecture notes] Intuitionistic Type Theory by Per Martin-Löf, Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980
[book] From Sets and Types to Topology and Analysis, edited by L. Crosilla and P. Schuster
[paper] From intuitionistic to formal topology: some remarks on the foundations of homotopy theory by S. Lindström et a.
[paper] 100 years of Zermelo's axiom of choice: What was the Problem with it? by Per Martin-Löf
[lecture notes] Realizability as the Connection between Computable and Constructive Mathematics by Andrej bauer
[dissertation] From Constructive Mathematics to Computable Analysis via the Realizability Interpretation by P. Lietz
https://homotopytypetheory.org/book/
That's quite comprehensive, thanks.
If you can't access any of the resources listed above, you can PM me