Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Feb 27 2021 at 17:29):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 27 2021 at 18:06):

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

view this post on Zulip Ruben Van de Velde (Feb 27 2021 at 18:06):

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

view this post on Zulip Johan Commelin (Feb 27 2021 at 18:07):

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

view this post on Zulip Damiano Testa (Feb 27 2021 at 18:08):

This is a dangerous game...

view this post on Zulip 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)$bc,a c c

view this post on Zulip Damiano Testa (Feb 27 2021 at 18:09):

I wonder if Kolmogorov would approve of simp.

view this post on Zulip 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.2c,a.1c c

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

view this post on Zulip 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:

view this post on Zulip Huỳnh Trần Khanh (Feb 28 2021 at 07:16):

(deleted)

view this post on Zulip 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