define empty set

Stream: new members

[Fames Yasd]

I am completely new to lean.
I want to do something like this:
Axiom : exists single b, forall x x not in b.
And after that by some magic that I can't figure out how to do this in Lean and Coq (you can do this in mizar though)
I should be able to define a constant "the emtpy set" and have two theorems about it:
first that forall x x not in "the empty set" and second that forall y if forall x x not in y then y = "the empty set"
Can someone type what I want in Lean and copy the code here?
I just want to see how does one do it.
The same thing goes with functions too.
For example in maths one can prove a theorem "forall x in \mathbb{R}_{>= 0} exists single y in R such that y^2 = x and after that you can define a function "sqrt" from nonnegative reals to R such that the following theorem holds "forall x in \mathbb{R}_{>= 0} (sqrt x)^2 = x".

[Kenny Lau]

Your theorem is in ZFC, which is not Lean's foundation

[Kenny Lau]

Lean uses dependent type theory

[Alex J. Best]

Lean (and coq) are based on type theory rather than set theory, every term has a type. So in a statement like $\forall x, ...$ the variable $x$ implicitly has a type, which is "a set that it lives in".
The analogue of the empty set would be the empty type, so one cannot form x : EmptyType.

In lean you can form subsets of terms of a given type, and those can be empty, so you can make an empty subset of any type, like
\emptyset : set \N
would give you the empty subset of naturals and then you can say \forall (x : \N), \not x \mem y, \to y = \emptyset.

[Reid Barton]

As others have said, Lean is not based on set theory so the empty set example does not translate well.
For the sqrt example, one possibility is something like this (not necessarily a good style, but hopefully illustrative).

import data.real.basic

lemma exists_sqrt : ∀ (x : ℝ), x ≥ 0 → ∃ (y : ℝ), y * y = x := sorry

noncomputable def sqrt : {x : ℝ // x ≥ 0} → ℝ :=
λ ⟨x, hx⟩, classical.some (exists_sqrt x hx)

lemma sqrt_def : ∀ x : {x : ℝ // x ≥ 0}, sqrt x * sqrt x = x :=
λ ⟨x, hx⟩, classical.some_spec (exists_sqrt x hx)

[Fames Yasd]

Reid Barton said:

λ ⟨x, hx⟩, classical.some (exists_sqrt x hx)

λ ⟨x, hx⟩, classical.some_spec (exists_sqrt x hx)

what do these two strings do?

[Andrew Ashworth]

Have you read https://leanprover.github.io/theorem_proving_in_lean? Explaining how Lean handles the axiom of choice is a bit involved.

[Fames Yasd]

can you prove the following theorem: forall x in \mathbb{R}_{>= 0} forall y in R if y^2 = x then y = sqrt(x) (which comes also with the definition of sqrt)

[Reid Barton]

That's equivalent to saying that the y whose existence is asserted by exists_sqrt is also unique

[Reid Barton]

i.e. it's really just a fact about the real numbers, which you had to prove independently of defining sqrt

[Fames Yasd]

okay
can't you do the same style with the definition of the empty set?

[Reid Barton]

There aren't any "sets" in the first place, in a sense that would allow a meaning for "the empty set"

[Reid Barton]

There also isn't a global membership relation $\in$.

[Fames Yasd]

like lemma exists_empty_set : exists (b : set), forall (x : set), not (x in b) := sorry

[Andrew Ashworth]

what is set

[Fames Yasd]

can't you define a new type called set or something?

[Andrew Ashworth]

no

[Fames Yasd]

what if you postulate that it exists

[Andrew Ashworth]

if you want to do ZFC axiomatically and model it Lean, that is possible

[Andrew Ashworth]

but then why would you use Lean instead of Mizar

[Fames Yasd]

Mizar has very little documentation on it and it takes some time to get an answer from them through e-mail. Also it has some very nasty thing where you have to prove that every type is inhabited or something like that.

[Andrew Ashworth]

Have you looked at Isabelle/ZFC?

[Fames Yasd]

no, I haven't

[Andrew Ashworth]

I would try that before Coq / Lean, which are very definitely based on dependent type theory.

[Andrew Ashworth]

or even Metamath, whew

[Fames Yasd]

Andrew Ashworth said:

Have you looked at Isabelle/ZFC?

Isabelle/ZFC is the same thing as Isabelle or something different?

[Johan Commelin]

@Fames Yasd Would the empty type be interesting to you?

[Johan Commelin]

It's not the empty set, but for all practical purposes, I find it just as interesting... (But I'm not a set theorist, nor a logician.)

[Yakov Pechersky]

Just an exercise for me, to define sqrt with the uniqueness:

import data.real.basic

lemma exists_sqrt : ∀ (x : ℝ), x ≥ 0 → ∃! (y : ℝ), y * y = x := sorry

noncomputable def sqrt : {x : ℝ // x ≥ 0} → ℝ :=
λ ⟨x, hx⟩, (exists_sqrt x hx).exists.some

lemma sqrt_def : ∀ x : {x : ℝ // x ≥ 0}, sqrt x * sqrt x = x :=
λ ⟨x, hx⟩, (exists_sqrt x hx).exists.some_spec

lemma sqrt_unique : ∀ x : {x : ℝ // x ≥ 0}, ∀ y z : ℝ, y * y = x → z * z = x → y = z :=
λ ⟨x, hx⟩ y z, (exists_sqrt x hx).unique

[Patrick Massot]

@Fames Yasd This conversation may be pointless as long as long as you don't tell us what you actually want to do with a proof assistant. If you are interested in formalizing ZF set theory for the sake of it then you can have a look at https://github.com/leanprover-community/mathlib/blob/57463fa/src/set_theory/zfc.lean but you won't get much out of it if you haven't learn anything about Lean yet (see https://leanprover-community.github.io/learn.html if you want to learn). But indeed you would probably be better off with a system which is more foundation agnostic such that metamath, or directly based on ZF set theory like Mizar or Isabelle/ZF (which is an exotic member of the Isabelle family, so the answer to your question "is this the same thing as Isabelle?" is both "it's a subset of Isabelle" and "no, this isn't what people usually call Isabelle which is the main member Isabelle/HOL of the family). If you actually want to formalize maths but only asked about defining the empty set because you thought this was a basic math question then you would take a much better start by thinking about less foundational stuff (since foundational stuff is very dependent on your foundations of course).

[Fames Yasd]

@Patrick Massot I want to formalize a couple of chapters from Jech's book on set theory. That is, to introduce zfc axioms, to define basic set theoretic concepts like union/bigcap/ordered pair/cartesian products/set-theoretic functions/natural numbers/integers and prove some basic properties about them that he has in his book. But I want to do that in a style similar to a classical mathematical reasoning. One postulates initial axioms and then makes new definitions (introduces new set-theoretic functions/functional symbols/constants) via proving theorems: for example one can prove exists! x P(x) to introduce a constant 'c' such that P(c) holds and prove forall a,b exists! y P(a,b,y) to introduce a function f(a,b) such that forall a,b P(a,b,f(a,b)) holds.
I'm looking for a prover that allows for this approach and also has a tolerable learning curve.

[Reid Barton]

This is not so straightforward because ZFC has axiom schemas quantifying over all formulas.
You may be interested in the Flypitch project (paper).

[Fames Yasd]

Reid Barton didn't really get what's the point of that paper and how it could help with my approach.
Can't you simply write specification axiom using type Prop or something like that? I believe Lean can quantify over predicates.

[Reid Barton]

It can quantify over all predicates, but not just the ones that are defined by formulas of ZF

[Fames Yasd]

but if I will be doing zfc from scracth, would not all predicates be precisely the ones defined by formulas of ZF?
I want to do everything from scratch.

[Reid Barton]

so, for example, you could try to start off like this:

structure model_of_zfc (U : Type) [has_mem U U] :=
(extensionality : ∀ (s t : U), (∀ x, x ∈ s ↔ x ∈ t) → s = t)
(exists_empty : ∃ (e : U), ∀ x, ¬ x ∈ e)
-- ...
(separation : ∀ (s : U), ∀ (p : U → Prop), ∃ (t : U), ∀ x, x ∈ t ↔ (x ∈ s ∧ p x))
-- ...

[Reid Barton]

but this separation axiom is too strong--for example I think that even if you don't include choice as an axiom, it will still follow from this separation, because you can construct a choice function in Lean and then import it into your model using separation

[Reid Barton]

The problem is U → Prop is Lean's function type, which is the wrong thing to quantify over. You want to quantify over formulas. That means you need to define what a formula is (or at least what the possible classes defined by formulas are).

[Fames Yasd]

No, I don't think I'm planning to refer to anyhing outside of this model
Should then be okay, right?

[Reid Barton]

Or, you could decide you don't really care about this detail and carry on regardless, but in that case you're not technically working with the first order theory ZFC

[Reid Barton]

Well, "okay" is up to you

[Fames Yasd]

Well, that model that you just wrote seems perfect for me.

[Reid Barton]

I think you'll find it impossible not to refer to anything outside the model--at a minimum you would probably need various logical connectives from Lean to form the sort of p you are interested in

[Fames Yasd]

Yeah, you are right.

[Fames Yasd]

How does one do proofs here? Can you show me an example of some simple proof?

[Kenny Lau]

if you want to quantify over formulas of ZF you might need to start defining formulas and their evaluations

[Kenny Lau]

which is done in flypitch

[Fames Yasd]

yeah, I got that

[Fames Yasd]

on a second thought, can I do ZFC using Lean's library or is it restricted in some way?

[Scott Morrison]

There is a model of ZFC inside Lean, under set_theory/zfc.lean.

[Michael Beeson]

Reid, why did you use "structure" instead of "class"? (I am doing something similar for Quine's New Foundations, and I used "class"). It's working just fine.

[Reid Barton]

No particular reason--I tend to use structure by default and here it illustrated the issue equally well.