Stream: new members

Topic: false constant

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?

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.

Kevin Buzzard (Feb 26 2021 at 10:28):

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

Huỳnh Trần Khanh (Feb 26 2021 at 10:29):

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

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)

Kevin Buzzard (Feb 26 2021 at 10:29):

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

Eric Wieser (Feb 26 2021 at 10:43):

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

Huỳnh Trần Khanh (Feb 26 2021 at 10:43):

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

Eric Wieser (Feb 26 2021 at 10:43):

I guess constants of type Sort aren't cheating?

Mario Carneiro (Feb 26 2021 at 10:46):

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

Mario Carneiro (Feb 26 2021 at 10:47):

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

Mario Carneiro (Feb 26 2021 at 10:47):

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

Huỳnh Trần Khanh (Feb 26 2021 at 10:48):

hmm so where is AC in Lean?

Mario Carneiro (Feb 26 2021 at 10:48):

docs#classical.choice

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?

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.

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

Mario Carneiro (Feb 26 2021 at 10:53):

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

Kevin Buzzard (Feb 26 2021 at 10:54):

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

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

Kevin Buzzard (Feb 26 2021 at 10:55):

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

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

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