Stream: new members

Topic: define empty set

Fames Yasd (Sep 02 2020 at 16:44):

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 (Sep 02 2020 at 17:01):

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

Kenny Lau (Sep 02 2020 at 17:01):

Lean uses dependent type theory

Alex J. Best (Sep 02 2020 at 17:01):

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 (Sep 02 2020 at 17:04):

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 (Sep 02 2020 at 17:10):

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 (Sep 02 2020 at 17:12):

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 (Sep 02 2020 at 17:12):

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 (Sep 02 2020 at 17:13):

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

Reid Barton (Sep 02 2020 at 17:14):

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

Fames Yasd (Sep 02 2020 at 17:15):

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

Reid Barton (Sep 02 2020 at 17:15):

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

Reid Barton (Sep 02 2020 at 17:16):

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

Fames Yasd (Sep 02 2020 at 17:17):

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

Andrew Ashworth (Sep 02 2020 at 17:17):

what is set

Fames Yasd (Sep 02 2020 at 17:17):

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

no

Fames Yasd (Sep 02 2020 at 17:17):

what if you postulate that it exists

Andrew Ashworth (Sep 02 2020 at 17:18):

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

Andrew Ashworth (Sep 02 2020 at 17:18):

but then why would you use Lean instead of Mizar

Fames Yasd (Sep 02 2020 at 17:21):

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 (Sep 02 2020 at 17:21):

Have you looked at Isabelle/ZFC?

no, I haven't

Andrew Ashworth (Sep 02 2020 at 17:23):

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

Andrew Ashworth (Sep 02 2020 at 17:24):

or even Metamath, whew

Fames Yasd (Sep 02 2020 at 17:55):

Andrew Ashworth said:

Have you looked at Isabelle/ZFC?

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

Johan Commelin (Sep 02 2020 at 18:00):

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

Johan Commelin (Sep 02 2020 at 18:00):

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 (Sep 02 2020 at 18:28):

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 (Sep 02 2020 at 18:53):

@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 (Sep 03 2020 at 14:47):

@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 (Sep 03 2020 at 14:55):

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 (Sep 03 2020 at 15:21):

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 (Sep 03 2020 at 15:22):

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

Fames Yasd (Sep 03 2020 at 15:23):

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 (Sep 03 2020 at 15:26):

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 (Sep 03 2020 at 15:28):

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 (Sep 03 2020 at 15:30):

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 (Sep 03 2020 at 15:30):

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

Reid Barton (Sep 03 2020 at 15:30):

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 (Sep 03 2020 at 15:31):

Well, "okay" is up to you

Fames Yasd (Sep 03 2020 at 15:31):

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

Reid Barton (Sep 03 2020 at 15:32):

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 (Sep 03 2020 at 15:33):

Yeah, you are right.

Fames Yasd (Sep 03 2020 at 15:36):

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

Kenny Lau (Sep 03 2020 at 15:39):

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

Kenny Lau (Sep 03 2020 at 15:39):

which is done in flypitch

yeah, I got that

Fames Yasd (Sep 05 2020 at 07:41):

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

Scott Morrison (Sep 05 2020 at 07:46):

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

Michael Beeson (Sep 05 2020 at 15:31):

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 (Sep 05 2020 at 15:37):

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

Last updated: May 13 2021 at 22:15 UTC