Doing mathematics constructively / intuitionisticly

[u/fdpth]

Are there any books and/or introductory texts about doing mathematics constructively (for research purposes)? I think I'd like to do two things, for which I'd need guidance:

1. train my brain to not use law of excluded middle without noticing it
2. learn how to construct topoi (or some other kind of constructive model, if there are some), to prove consistency of a certain formula with the theory, similar to those where all real functions are continuous, all real functions are computable, set of all Dedekind cuts is countable, etc.

Is this something one might turn towards after getting a PhD in another area (modal logic), but with a postgraduate level of understanding category theory and topos theory?

I have a theory which I'd like to see if I could do constructively, which would include finding proofs of theorems, for which I need to be good at (1.), but also if the proof seems to be tricky, I'd need to be good at (2.), it seems.

[u/gopher9]

train my brain to not use law of excluded middle without noticing it

That's easy: just learn a proof assistant based on dependent types, like Coq or Agda (even Lean is fine). If you internalized Curry–Howard correspondence, then doing things constructively should come naturally.

People do a lot of constructive stuff in these systems, like if you are interested in HoTT, you can look at https://github.com/agda/cubical.

[u/djao → u/gopher9]

Seconded. I care little for constructive mathematics in real life or research, but when I really want to understand a proof, proving it in Rocq (Coq has now been officially renamed to Rocq, I believe) makes constructive mathematics automatic. You can also fall back to classical mathematics with LEM if you want, but it becomes a conscious choice that you are aware of, rather than a blind spot, and Rocq will readily tell you whether or not you have used LEM in any given proof or its dependencies.

[u/aardaar]

Beeson's book Foundations of Constructive Mathematics, and Troelstra/Van Dalen's Constructivism in Mathematics are excellent resources, though they won't have much about topoi.

[u/TESanfang]

My knowledge of this is very limited, but I'm currently doing my bachelor's thesis about HoTT and in the HoTT book things are mostly proven constructively in Martin Loefs type theory (if they aren't, then they show explicitly where the "nonconstrutivism" comes from). It's really cool, and because there's a notion of proof relevance (proofs are themselves mathematical objects), they sometimes show multiple proofs for the same fact or translate them from english into their flavour of lambda calculus

[u/Holiday_Ad_3719]

Locale theory: Peter Johnstone's Stone Spaces rarely uses the excluded middle as he was well aware of Topos theoretic applications when he wrote it.

[u/Ok_Buy2270]

Maybe of A Primer of Infinitesimal Analysis - John Lane Bell. Read the preface to see what i mean. The book concerns the following topic: https://en.wikipedia.org/wiki/Smooth_infinitesimal_analysis

[u/evincarofautumn]

As a computer scientist I’m interested in constructive proofs because they correspond to programs that compute actual objects. So, I don’t know if this appeals to you, but I find it very helpful to have a computer check my logic for me, by using the executable subset of proof-assistant languages (Lean, Agda) or the total subset of functional programming languages (Idris, Haskell).

From the perspective of category theory and topology, I would definitely recommend John Bell’s A Primer of Infinitesimal Analysis (Google Books), a short book about smooth infinitesimal analysis. Excluding LEM lets us define infinitesimals as objects ε so that ¬(ε = 0) yet ε² = 0. I think it gives a good introduction to a lot of useful concepts for doing constructive math beyond computing.

If you’re into modal logic, linear logic (Wikipedia, Stanford) should feel somewhat familiar. It helps with being rigorous about constructiveness by distinguishing an additive disjunction [A or B]—“some of these are provable”—from a multiplicative disjunction [A par B]—“not all of these are refutable”. A paper I like about this is Affine logic for constructive mathematics by Michael Shulman (arXiv) though I couldn’t say how much it’ll help you where you’re at.