Sets of Functions

Stream: new members

[Philipp SL Schäfer]

For some proof I need to define sets of functions, but in this little example

variable {α: Type u_1} {X Y : Set α}

def test_set : Set (X → ℕ) :=
  { f | f : (X → ℕ)}

def test_fun : X → ℕ := fun x ↦ 0

example : test_fun ∈ test_set := by
  rewrite [test_set, mem_setOf]
  use test_fun

I get the following error

don't know how to synthesize implicit argument
  @test_fun ?m.187 ?m.188
context:
α : Type u_1
X Y : Set α
⊢ Set ?m.187
when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processedLean 4
don't know how to synthesize implicit argument
  @test_fun ?m.187 ?m.188
context:
α : Type u_1

How can I fix this?

[Antoine Chambert-Loir]

The problem here is that test_set has an implicit argument Xwhich the elaborator of the example does not manage to fill in (that's what the ?m.113 indicates).

Another problem is a question of understanding the principles of type theory. Your test_set is basically the “set” of all functions X → ℕ, in other words, it is docs#Set.univ. And you're willing to prove that for f: X → ℕ, one has f ∈ Set.univ. That is docs#Set.mem_univ.

[Luigi Massacci]

@Philipp SL Schäfer, if you fix the implicit argument problem @Antoine Chambert-Loir told you about, your proof will work just fine. The point is that you can’t possibly expect Lean to guess the set X over which test_set and test_fun are defined. Keep in mind, they are both really functions. Look at the signature of test_set.{u_1}: {α : Type u_1} (X : Set α) : Set (↑X → ℕ) (as you can see by running #check test_set and #check test_fun).

With the curly brackets you are telling Lean “I won’t pass this information to you explicitly, infer it from the context” but this is clearly impossible in your case. You can solve it by making X explicit (then α can be inferred from X):

import Mathlib.Tactic
open Set

variable {α: Type u_1} (X Y : Set α)

def test_set : Set (X → ℕ) := {f | f : X → ℕ}
def test_fun : X → ℕ := fun x ↦ 0

#check test_set

example : test_fun X ∈ (test_set X) := by
  rewrite [test_set, mem_setOf]
  use test_fun X

[Philipp SL Schäfer]

Thanks a lot to both of you!

[Philipp SL Schäfer]

But I am still not sure how I can use this to proof that the power set exists for any set X, given the power set axiom:

(Power set axiom). Let X and Y be sets. Then there exists a set denoted as Yˣ,
which consists of all the functions from X to Y, thus f ∈ Yˣ ↔ (f is a function with domain X and codomain Y)

The idea for the proof is to start with the set {0, 1}ˣ and apply the replacement axiom, replacing each function f with the object f⁻¹({1}). With pen and paper, I get it, but I run into problems when defining the sets I need:

1) How to resolve "Problem 1: failed to synthesize instance OfNat (↑zero_one) 0" better than to define the arbitrary function to_zo.

2) How to best define the set {f ⁻¹' ({1}) | f ∈ { f | f : X → {0, 1} } }

This is what I have so far.

section
variable {α: Type u_1} (X: Set α) (SX: Set X)

def zero_one : Set ℕ := { n | n = 0 ∨ n = 1 }

def pset : Set (X → zero_one) := { f | f : X → zero_one}

-- Problem 1: failed to synthesize instance OfNat (↑zero_one) 0
def zo_fun_bad : X → zero_one := fun x ↦ (0 : zero_one)

-- Workaround? - define a function to explicitly convert natural numbers to zero_one
-- But this is not quite acurrate because #eval to_zo 3 returns 1
def to_zo (n : ℕ) : zero_one :=
  if n = 0 then ⟨0, Or.inl rfl⟩ else ⟨1, Or.inr rfl⟩

def zo_fun : X → zero_one := fun x ↦ to_zo 0

#check pset    -- pset.{u_1} {α : Type u_1} (X : Set α) : Set (↑X → ↑zero_one)
#check pset X  -- pset X : Set (↑X → ↑zero_one)

example : (zo_fun X) ∈ (pset X) := by
  rewrite [pset, mem_setOf]
  use (zo_fun X)

-- Define this set based on the replacement axiom as suggested
def set_1 : Set (Set X) := {f ⁻¹' ({to_zo 1}) | f ∈ (pset X)}

-- Define the power set
def set_2 (x : Set X) : Set (Set X) := {y : Set X | y ⊆ x}

#check set_1 X
#check set_2 X SX

[Ruben Van de Velde]

I would highly recommend you don't try to do set theory puzzles based on ZFC axioms

[Philipp SL Schäfer]

Why?

[Yaël Dillies]

because Lean isn't based on ZFC, so the first thing you would need to do is embed ZFC inside Lean's logic. See eg docs#ZFSet

[Dan Velleman]

Lean is based on type theory, not ZFC. They are different.

One thing you may be confused about is the difference between types and sets. In the notation Set X, X should be a type, not a set. In the notation X → Y, X and Y should be types, not sets. So when you have X : Set α, you probably don't want to write Set X or X → zero_one; that doesn't mean what you seem to think it means.

For example, you wrote:

def set_2 (x : Set X) : Set (Set X) := {y : Set X | y ⊆ x}

What would make more sense is:

def set_2 (x : Set α) : Set (Set α) := {y : Set α | y ⊆ x}

[Antoine Chambert-Loir]

Philipp SL Schäfer said:

Why?

The ZFC axioms are a minimal set of axioms from which one can elaborate the whole language of mathematics. But, as the exercises you are trying to do indicate, a lot of preliminary work is necessary, for example, to construct the set of functions $f\colon X\to Y$ from various other sets which are already defined.

Lean is built on another foundational system, type theory, which already contains all of these. If $X$ and $Y$ are types, for example, the system already knows about the type $X\to Y$ which embodies functions from $X$ to $Y$, and how it behaves, so there is no need of doing the kind of constructions required to start math from ZFC. Worse, these exercices would be very unnatural.

However, two things can be done, and are already done in mathlib if I'm not mistaken.

• Construct a way to talk about another axiom system, its language and terms, using Lean as a metamathematical tool
• Embed the ZF theory of sets into Lean by constructing a type which satisfies the axioms. This is what docs#ZFSet does.

[Philipp SL Schäfer]

Thanks everyone!

So how much sense does it generally make to use Lean to verify proofs for an introductory level course on real analysis (that is based on ZFC)? I am mainly doing it because I study alone (since I don't even study math); and Lean works perfectly to see if an idea for a proof works or not (if I manage to write it in Lean, which can fail in cases like this one).

[Patrick Massot]

Introductory level courses on real analysis are not based on ZFC or any other foundation.

[Mario Carneiro]

Usually the only part of real analysis that will touch on aspects of ZFC will be the appendix entitled "construction of the real numbers"

[Mario Carneiro]

and even that can be pretty faithfully reconstructed in type theory if you just stop at Nat instead of building it out of ordinals

[Philipp SL Schäfer]

Okay so I am going through Analysis I by Terence Tao, and I thought it is based on ZFC (since all these axioms are introduced in chapter 3).

[Mario Carneiro]

I think the point is more that you can just cross out the part that says "we assume a foundation of ZFC" or the like and the remainder of the book will be mostly unaffected

[Mario Carneiro]

most mathematics only pays lip-service to ZFC but doesn't use it in any nontrivial way

[Philipp SL Schäfer]

Okay that would be perfect for my purposes! So roughly speaking naive set theory is probably sufficient for what I want to learn, and I can just assume that some set exists?

[Mario Carneiro]

I would stop at the first part of the sentence

[Mario Carneiro]

type theory gives you the means to construct many types, not just "start at the empty set and build up to everything else"