I can give you some intution as to why (¬¬P)∨(¬P) isn’t provable. The essense of a proof of a disjunction A ∨ B is to either have a proof of A or a proof of B

I can give you some intution as to why (¬¬P)∨(¬P) isn’t provable. The essense of a proof of a disjunction A ∨ B is to either have a proof of A or a proof of B – as well as a label telling if we proved the left or the right hand side. So, to have a proof for every P that (¬¬P)∨(¬P) means that for every P you can either cough up a proof that ¬¬P or a proof of ¬P. This is impossible. Your final paragraph mixes object level and meta-level in a way I am not quite able to decipher. But there are results in a similar vein, but restricted to particular theories: The Gödel—Gentzen translation[0] translates formulas of Peano artithmetic into formuals in Heyting arithmetic in a way which preserves provability. But there are quite limited which theories this works for. For instance, such a translation does not exist in set theory between, say, ZFC and CZF. So there is in general no way for a constructivist to give meaning a classical proof. [0]: https://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_negative_translation https://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_neg...