Zulip Chat Archive

Stream: new members

Topic: false constant


view this post on Zulip Huỳnh Trần Khanh (Feb 26 2021 at 10:27):

why can i write a proof of false when i declare a false constant? can i similarly write a proof of false using a definition that returns false and why?

view this post on Zulip Kevin Buzzard (Feb 26 2021 at 10:28):

if you use constant or axiom in Lean 3 you can do anything. That's the point of those keywords.

view this post on Zulip Kevin Buzzard (Feb 26 2021 at 10:28):

You can also prove false using meta, but it's only a meta proof.

view this post on Zulip Huỳnh Trần Khanh (Feb 26 2021 at 10:29):

oh, so constant declares a new axiom. kinda counterintuitive but thanks lol

view this post on Zulip Kevin Buzzard (Feb 26 2021 at 10:29):

Note that there is not a single instance of constant or axiom in src of mathlib (although for all I know they might exist in the test directory or other places)

view this post on Zulip Kevin Buzzard (Feb 26 2021 at 10:29):

I think constant = "cheat with a def" and axiom = "cheat with a theorem" in Lean 3.

view this post on Zulip Eric Wieser (Feb 26 2021 at 10:43):

Just to muddle things, doc-gen says docs#false is a constant

view this post on Zulip Huỳnh Trần Khanh (Feb 26 2021 at 10:43):

but it's of type prop not of type false lol

view this post on Zulip Eric Wieser (Feb 26 2021 at 10:43):

I guess constants of type Sort aren't cheating?

view this post on Zulip Mario Carneiro (Feb 26 2021 at 10:46):

Well false isn't the only constant, it comes with false.rec

view this post on Zulip Mario Carneiro (Feb 26 2021 at 10:47):

inductive types are axioms, don't let anyone tell you otherwise

view this post on Zulip Mario Carneiro (Feb 26 2021 at 10:47):

or rather, the whole collection of inductive types is one (rather complicated) axiom schema

view this post on Zulip Huỳnh Trần Khanh (Feb 26 2021 at 10:48):

hmm so where is AC in Lean?

view this post on Zulip Mario Carneiro (Feb 26 2021 at 10:48):

docs#classical.choice

view this post on Zulip Kevin Buzzard (Feb 26 2021 at 10:48):

Heh, yes, the inductive keyword gives you a new way of adding constants and axioms to the system :-) But this is a rather more controlled approach than the constant one! In particular, didn't some kid prove that it was equiconsistent with set theory at some point?

view this post on Zulip Kevin Buzzard (Feb 26 2021 at 10:51):

@Huỳnh Trần Khanh in programming languages you can just add new classes and methods etc. The inductive keyword lets you do the same sort of thing in Lean, however there is also this theorem proving part to Lean so you have to be careful not to let the user just add a random bunch of things and then prove 0 = 1, because that would break stuff. The inductive keyword (and its derivatives structure and class) lets the user add new classes to the system but is not logically strong enough to let them prove false. The constant and axiom keywords are much stronger, and indeed they are too strong if you want the system to remain consistent. But if you're just interested in writing code then consistency might not be something you're worried about.

view this post on Zulip Mario Carneiro (Feb 26 2021 at 10:53):

if you are just writing code you probably don't want to be using constant or axiom at all because they can't be executed

view this post on Zulip Mario Carneiro (Feb 26 2021 at 10:53):

(with the exception of meta constants that lean specifically overrides)

view this post on Zulip Kevin Buzzard (Feb 26 2021 at 10:54):

I'm running out of use cases for constant and axiom then.

view this post on Zulip Mario Carneiro (Feb 26 2021 at 10:54):

constant and axiom are good when you want to sorry a whole lot of things and don't want to apologize

view this post on Zulip Kevin Buzzard (Feb 26 2021 at 10:55):

Aah -- they are warning-removers. Replace "warning: you cheated" with an unseen cheat!

view this post on Zulip Mario Carneiro (Feb 26 2021 at 10:57):

It's a bit better to use hypotheses, but if you have hundreds of hypotheses that you are carrying around, and especially if you are trying to do a proof in an advanced area and aren't trying to build everything from scratch like mathlib, axioms are a good fit

view this post on Zulip Mario Carneiro (Feb 26 2021 at 10:57):

a lot of targeted formalization projects fall in this camp


Last updated: May 07 2021 at 00:30 UTC