## Stream: new members

### Topic: Proving ¬(p ↔ ¬p) without classical logic

#### Kritixi Lithos (Feb 27 2021 at 17:18):

(From here) I would like hints for this. So I understand I have to get a function with type signature (p ↔ ¬p) → false, so the function has to start with (λhpnp:(p↔¬p), ) and then prove false by getting a contradiction by reaching a term and its negation. I thought doing hpnp.mp hpnp, but hpnp is not of type p. How do I proceed?

#### Kevin Buzzard (Feb 27 2021 at 17:31):

Does this link link to the top of it? That might be a better place to start.

#### Kritixi Lithos (Feb 27 2021 at 17:55):

Thanks @Kevin Buzzard (yes it links to the top of it) and @Bryan Gin-ge Chen. I had forgotten the lambda resulting from proving false from assumption hp:p is itself of type ¬p. So converting your proof to lambda functions gives the following

example : ¬(p ↔ ¬p) := (λhpnp,absurd(hpnp.mpr(λhp:p,absurd hp(hpnp.mp hp)))(λhp:p,((absurd hp(hpnp.mp hp)))))


Edit: also searching for ¬(p ↔ ¬p) using the search tool doesn't yield any results for me

#### Bryan Gin-ge Chen (Feb 27 2021 at 18:05):

If you're fond of term mode proofs, this post of mine shows how you can derive a proof like that by "chasing underscores".

#### Thomas Browning (Feb 27 2021 at 18:05):

Is it possible to do better than 31 characters?

example (p : Prop) : ¬(p ↔ ¬p) :=
λ⟨a,b⟩,(λ c,a c c)$b$λ c,a c c


#### Kevin Buzzard (Feb 27 2021 at 18:06):

example (p : Prop) : ¬(p ↔ ¬p) :=
by simp


#### Ruben Van de Velde (Feb 27 2021 at 18:06):

Probably any proof is "better", even if it's not shorter :)

#### Johan Commelin (Feb 27 2021 at 18:07):

@Thomas Browning you don't need the spaces after the lambdas, right?

#### Damiano Testa (Feb 27 2021 at 18:08):

This is a dangerous game...

#### Thomas Browning (Feb 27 2021 at 18:09):

:grinning: Oh, good point. I thought that it wouldn't work since the lambda changes color in VS Code.

example (p : Prop) : ¬(p ↔ ¬p) :=
λ⟨a,b⟩,(λc,a c c)$b$λc,a c c


#### Damiano Testa (Feb 27 2021 at 18:09):

I wonder if Kolmogorov would approve of simp.

#### Thomas Browning (Feb 27 2021 at 18:21):

Down to 27:

--27
example (p : Prop) : ¬(p ↔ ¬p) :=
λa,(λc:¬p,c$a.2c)$λc,a.1c c

--28
example (p : Prop) : ¬(p ↔ ¬p) :=
λa,(λc,a.1c c)$a.2$λc,a.1c c

--28
example (p : Prop) : ¬(p ↔ ¬p) :=
λ⟨a,b⟩,(λc,a c c)$b$λc,a c c


#### Huỳnh Trần Khanh (Feb 28 2021 at 07:02):

i think yes, the kolmogorov complexity is an information theoretic argument and has nothing to do with what is available in the language

information theoretic laws are perpetual and there is no way to break them :joy:

(deleted)

#### Mario Carneiro (Feb 28 2021 at 08:44):

Information theoretic laws are also only asymptotic and say nothing about the capabilities of the language. Really it doesn't apply to the lean proof task at all, because as kevin showed by simp works here, and one can imagine a souped up version of simp that proves every provable statement by enumeration, so lean proofs can be O(1) no matter the statement. In fact, even if you ban tactics, it's possible to get rfl to do this too, although I don't know if it's possible to get unbounded recursion during reduction, so it's really something like O(inverse ackermann) (except even slower than that, it's the inverse of the fastest growing functions in DTT which are truly stupendous).

Last updated: May 14 2021 at 05:20 UTC