It is clear to me that it should be impossible to prove :

exclMidl = isProp A → ((A) ⊎ (¬ A))

Because it would give deciding oracle for every Proposition.

My question is about the following Types:

exclMidl' = isProp A → ∥ ((A) ⊎ (¬ A)) ∥ 


exclMidl'' = isProp A → ∥ ((A ≡ Unit) ⊎ (A ≡ Empty)) ∥

Are they provable in cubical Agda? What HoTT can say about them?

Those types would only state that propositions are either True or False but would hide information about actual Truthness of A, preventing us from constructing universal oracle, but allowing, for example, to do a proof for both cases even for undecidable propositions.

Is my intuition about such types correct?


The only way to prove ∥ X ∥ is to prove X (unless you admit some other axiom). So, assuming P is a proposition, there is no way to prove ∥ ((A) ⊎ (¬ A)) ∥ if you cannot prove ((A) ⊎ (¬ A)).

It is not a correct intuition that undecidable propositions are either true or false, just we do not know about it.

A formal system S with an undecidable proposition P can always be extended either in S'=(S,p:P), or S''=(S,p:¬ P) where p is taken as a new axiom. Both S' and S'' are then consistent formal systems, provided S is. If P were already true or false in S, then either S' or S'' would be inconsistent.

A formal system is meant to be interpreted, and can usually be interpreted in different ways. Undecidable propositions in a formal system are propositions that can be true in some interpretations, and false in other interpretations. A proposition is said to be true (resp. false) within a formal system when it is true (resp. false) in all possible interpretations. So there are lots of propositions that are neither true nor false within the formal system.

The confusion comes from the different meanings for 'true': the truth within the formal system usually does not match exactly the truth in the interpretation (or intuition) that you have in mind when you are working with the formal system...

| cite | improve this answer | |

Another thing you should know is that those truncations don't hide anything. For instance, it is relatively simple to prove the lemma:

$$\mathsf{isProp}\ A → \mathsf{isProp}\ (A \uplus ¬ A)$$

which means that we can extract the evidence from $\| A \uplus ¬A \|$. I think the same is true of the $A \equiv \mathsf{Unit}$ version, because all types involved are easily shown to be in:

$$\mathsf{HProp} = Σ_{A : \mathsf{Type}}\ \mathsf{isProp}\ A$$

which is itself a set, and thus its paths are propositions. So your two latter formulations allow deriving the first.

I don't think you should think of the propositional truncation as 'freeing' you from needing (positive) computataional evidence for things, or covering up the fact that you don't have any. In fact, that is one of the things that makes truncation rather different from double negation (which also turns things into propositions). Truncation is still constructive, and if you add non-constructive axioms that result in truncated things, you are in general still making the logic non-constructive.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.