false constant

Stream: new members

[Huỳnh Trần Khanh]

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]

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

[Kevin Buzzard]

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

[Huỳnh Trần Khanh]

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

[Kevin Buzzard]

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]

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

[Eric Wieser]

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

[Huỳnh Trần Khanh]

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

[Eric Wieser]

I guess constants of type Sort aren't cheating?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Huỳnh Trần Khanh]

hmm so where is AC in Lean?

[Mario Carneiro]

docs#classical.choice

[Kevin Buzzard]

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]

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

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

a lot of targeted formalization projects fall in this camp