Stream: new members
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?
Bryan Gin-ge Chen (Feb 27 2021 at 17:29):
This is a frequently asked question, see e.g. this thread.
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
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:
Huỳnh Trần Khanh (Feb 28 2021 at 07:16):
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