## Stream: new members

### Topic: Off by one in types

#### Brandon Wu (Jul 07 2020 at 02:03):

Why does this proof not work out? I have something of an "off by one" in my types, where I'm expecting something of type A, but instead I provided something that simply was A. It's my impression that, in the example that I am trying to prove, A should be quantified over all propositions.

example (A : Prop) : ∀ A, ¬ ¬(¬ ¬ A ∨ ¬ ¬ ¬ A) := assume A, assume h : ¬ (¬ ¬ A ∨ ¬ ¬ ¬ A), show false, from h (or.inl (assume h2 : ¬ A, show false, from h2 A))

#### Bryan Gin-ge Chen (Jul 07 2020 at 02:14):

The (A : Prop) and the ∀ A have nothing to do with each other. Are you sure you want them both?

#### Bryan Gin-ge Chen (Jul 07 2020 at 02:19):

I think you just took a wrong turn near the end of your proof. This works:

example (A : Prop) : ¬ ¬(¬ ¬ A ∨ ¬ ¬ ¬ A) :=
assume h : ¬ (¬ ¬ A ∨ ¬ ¬ ¬ A),
show false, from
h (or.inl (assume h2 : ¬ A,
show false, from h (or.inr (assume h3 : ¬ ¬ A,
show false, from h3 h2))))


#### Brandon Wu (Jul 07 2020 at 02:25):

Oh, I see what happened. I got mistaken with quantifying the A : Prop for having a term of type A. My goal in the end was fundamentally flawed from the start. Thank you!

#### Bryan Gin-ge Chen (Jul 07 2020 at 02:42):

Well, this is exactly equivalent:

example : ∀ A, ¬ ¬(¬ ¬ A ∨ ¬ ¬ ¬ A) :=
assume A : Prop,
assume h : ¬ (¬ ¬ A ∨ ¬ ¬ ¬ A),
show false, from
h (or.inl (assume h2 : ¬ A,
show false, from h (or.inr (assume h3 : ¬ ¬ A,
show false, from h3 h2))))


Last updated: Dec 20 2023 at 11:08 UTC