Is False → p an axiom in Lean 4 ?

Stream: lean4

[Valentin Vinoles]

Hello

The implication False → p is "true" in Lean 4 :

theorem False_implies_everything (p : Prop) : False → p :=
  by tauto

I am wondering if it is an axiom or if it is provable.

If one thinks about False as the empty proposition (as written in the documentation), then a proof of False → p would be the "empty function" $\varnothing \to p$, more precisely the function defined by the triplet $(\varnothing,p,\varnothing)$ (see here).

But I do not know how to define such function in Lean 4 . Is it possible to do so ?

[Patrick Massot]

You can use show_term tauto to see the proof found by tauto.

[Patrick Massot]

And please don't read that Wikipedia page if you don't want to be utterly confused since it is all about set theoretic foundations.

[Patrick Massot]

There is nothing like a function defined by a triplet in Lean.

[Patrick Massot]

As explained in the documentation that you refer to, the proof is simply False.rec.

[Riccardo Brasca]

It's not an explicit axiom by itself, it is a consequence of the rules of type theory. The definition of False is the following

inductive False : Prop

so it is an inductive proposition with no constructors. Now, every time we define an inductive object, Lean adds it's "eliminator", in this case it adds False.rec, you can check it's type

#check False.rec
--False.rec.{u} (motive : False → Sort u) (t : False) : motive t

So False.rec allows you to produce a term of any given type from a term of type False. It is produced automatically following the rules of type theory.

What is the reason behind it? In general rec says that to define a function out of an inductive type T one has to specify the image of all the constructors, and in this case there are no constructors, so there is nothing to do. (Of course the precise rule is complicated to state, but the point is that this is a special case of the general construction of an inductive type.)

[Patrick Massot]

There are a lot more explanation here and there.

[Yury G. Kudryashov]

#8190 relates functions to "function-like" relations (works better than sets in the product with Mathlib).

[Kyle Miller]

@Yury G. Kudryashov It seems like that message was meant for another topic?

[Yury G. Kudryashov]

@Riccardo Brasca No, this PR was partially inspired by

Patrick Massot said:

There is nothing like a function defined by a triplet in Lean.

[Yury G. Kudryashov]

BTW, should we make choose use this lemma for ExistsUnique input?

[Valentin Vinoles]

Thanks @Patrick Massot @Riccardo Brasca , it is clearer.

[Filippo A. E. Nuccio]

Patrick Massot said:

You can use show_term tauto to see the proof found by tauto.

Well, in this case I am not sure that this is really the best way to sort it out. Indeed,

theorem False_implies_everything' (p : Prop) : False → p := by
  show_term{tauto}

results in the suggestion

Try this: exact let_fun em := Classical.propDecidable;
fun a => False.casesOn (fun x => p) a

On a one hand, there is a Classical.propDecidable showing up and then, even worse,

theorem False_implies_everything' (p : Prop) : False → p := by
    exact
      let_fun em := Classical.propDecidable;
      fun a => False.casesOn (fun x => p) a
--application type mismatch
--  False.casesOn ?m.39 fun x => p
--argument
 -- fun x => p
-- has type
--  ?m.41 → Prop : Sort (max 1 ?u.40)
-- but is expected to have type
--  False : Prop

results in an error. The easiest solution (which is basically the one proposed by @Riccardo Brasca ) is

theorem False_implies_everything (p : Prop) : False → p :=
    @False.casesOn (fun _ => p)

[Patrick Massot]

Not it isn't, see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Is.20False.20.E2.86.92.20p.20an.20axiom.20in.20Lean.204.20.3F/near/400304968