Study Theorem 3.2.2 #14

New issue

Open

opened 2024-05-20 20:22:40 +00:00 by michael · 2 comments

michael commented

2024-05-20 20:22:40 +00:00

Owner

Theorem 3.2.2. It is not the case that for all A : \mathcal{U} we have ¬(¬A) → A.

This is a pretty long proof and involves many moving parts. I don't understand how all of it works

> **Theorem 3.2.2.** It is not the case that for all $A : \mathcal{U}$ we have $¬(¬A) → A$. This is a pretty long proof and involves many moving parts. I don't understand how all of it works

michael referenced this issue

2024-05-20 20:23:25 +00:00

Chapter 3: Sets and logic #9

michael added this to the (deleted) project 2024-05-20 20:23:35 +00:00

michael commented

2024-05-20 21:26:16 +00:00

Author

Owner

I have most of the proof written down, but the biggest thing that confuses me is:

Thus, applying (3.2.4) to f(\mathbf{2})(u) and (3.2.3), we obtain an element of \mathbf{0}.

This means the result is still contingent on already having a value u : \neg \neg \mathbf{2}, but the type of the overall theorem is:

theorem3∙2∙2 : ((A : Set) → ¬ ¬ A → A) → ⊥

where the \neg \neg A part is still negative.

I have most of the proof written down, but the biggest thing that confuses me is: > Thus, applying (3.2.4) to $f(\mathbf{2})(u)$ and (3.2.3), we obtain an element of $\mathbf{0}$. This means the result is still contingent on _already_ having a value $u : \neg \neg \mathbf{2}$, but the type of the overall theorem is: ``` theorem3∙2∙2 : ((A : Set) → ¬ ¬ A → A) → ⊥ ``` where the $\neg \neg A$ part is still negative.

michael modified the project from (deleted) to research

2024-05-24 01:34:36 +00:00

michael commented

2024-07-11 13:05:38 +00:00

Author

Owner

Actually, creating a value of u : \neg \neg \mathbf{2} is easy:

u : ¬ ¬ bool
u = λ p → p (lift true)

Still have these parts to prove though:

allsamef : ∀ {l} {bool : Set l} → (u v : ¬ ¬ bool) → u ≡ v
huhh : (Σ.fst e) (fbool u) ≡ fbool u

Actually, creating a value of $u : \neg \neg \mathbf{2}$ is easy: ``` u : ¬ ¬ bool u = λ p → p (lift true) ``` Still have these parts to prove though: ``` allsamef : ∀ {l} {bool : Set l} → (u v : ¬ ¬ bool) → u ≡ v huhh : (Σ.fst e) (fbool u) ≡ fbool u ```