> Prop vs Decidable - I vaguely understand the distinction, but can use more examples. Also would like to know does this relate to the noncomputable property.

My path to this subject was tortured, so sorry if I don’t account for Polysemy etc.

With Prop, I think what you need to dig into is ‘non-computational’ not ‘non-computable’.

Mere propositions is probably best viewed with Homotopy Type Theory[0]

Two proofs (t1,t2) of the same proposition (p:Prop) which are definitionally equal are proof irrelevant, meaning that all they carry is the proof p is true.

This paper [1] may be helpful but the difference between groupoids and subsingletons with classical mathematics is challenging for many of us.

Hopefully this helps in your journey.

Also remember that with classical set theory the internal and external proposition truths are different, the Curry–Howard correspondence is to constructivist from lambda calculus, you don’t have PEM etc…

Remember DGM[2] shows that finite indexing or projection is PEM

Good luck and I hope you continue to share your journey.

[0] https://homotopytypetheory.org/wp-content/uploads/2013/03/ho...

[1] https://jesper.sikanda.be/files/definitional-proof-irrelevan...

[2] https://ncatlab.org/nlab/show/Diaconescu-Goodman-Myhill+theo...

> With Prop, I think what you need to dig into is ‘non-computational’ not ‘non-computable’.

Here's another way to explain this:

As you state, Prop has to do with proof-irrelevance. When doing constructive mathematics, proofs are programs (meaning they carry computational content), but sometimes it's useful to treat any two proofs of the same proposition as equal. As a consequence, proofs cannot be inspected or run as programs, and you get back the Law of Excluded Middle from classical mathematics.

Decidable has to do with decidability. This means that given some proposition P, there is an algorithm that can either produce a proof of P, or a proof of ~P. This is usually useful when P is a predicate, so that at each x, P(x) either has a proof or a disproof.

In classical mathematics, the Law of Excluded Middle holds for all propositions. In constructive mathematics, the Law of Excluded Middle only holds for decidable propositions. If P is decidable, it is safe to constructively assume P or ~P because an algorithm can produce the answer.