Proving ¬(p ↔ ¬p) without classical logic

Stream: new members

[Kritixi Lithos]

(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?

[Bryan Gin-ge Chen]

This is a frequently asked question, see e.g. this thread.

[Kevin Buzzard]

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

[Kritixi Lithos]

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]

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]

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]

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

[Ruben Van de Velde]

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

[Johan Commelin]

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

[Damiano Testa]

This is a dangerous game...

[Thomas Browning]

: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]

I wonder if Kolmogorov would approve of simp.

[Thomas Browning]

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]

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:

[Huỳnh Trần Khanh]

(deleted)

[Mario Carneiro]

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).