> I get that in such logic you can't deduce "P is false" directly from "Not-P is true"
It's actually the other way around; if not-P is true, then P is false, but not conversely. (The computer-flavoured example that comes to mind is that it is not possible to decide equality of functions (so `P or not-P` fails), but any two functions either are (`P` is true) or are not (`P` is false) equal. Again, this confusion between truth and decideability is, I think, not quite rigorous, but it gets at the essential idea.)
> I keep telling myself that I should learn more about constructive logic, as my own intuitions tend to it.
Indeed, Brouwer's precursor of constructive logic was called "intuitionistic logic" precisely because he felt that it better captured an intuitive, rather than formalist, approach to reasoning. (I'm not sure I agree ….)
For me, the important intuition in this regard is that, for any mathematical theory to be useful, you need to create a process where you can prove properties about its objects in a finite number of steps. You can handle infinite objects (like sets), but at some point you need to define a finite process that produces some knowledge about the object (for example, deciding if a particular word is a member of an infinite grammar).
Working with infinite objects is like using lazy computations in a functional language - you only use as many steps as needed, even if the process does not have a termination step. (I'm not sure to what degree constructive logics handle this intuition - as I said, I don't know much about them).
I've seen that some models exist for mathematical proofs containing infinite steps, but those don't seem to be widespread - and the models are themselves defined through a finite description; so I think even this extreme case validates my intuition that in the end, the mathematician needs to include just a limited number of clauses in their day-to-day work to get something done, even if those clauses are used to describe infinite objects.
I get that in such logic you can't deduce "P is false" directly from "Not-P is true", and you have to build an explicit derivation for the former?