# How to get an element from an existential proposition in Type theory proof assistant (Lean prover)

I am trying to implement set theory in type theory from scratch, just for self pedagogical purposes. Specifically, I'm using the Lean Prover, and defining the element-of relation from scratch using the symbol $$\epsilon$$, just for pedagogical purposes.

## What I'm trying to do

However, I'm unsure how to even define the notion of inductive set in this way. I am using the definition of inductive set:

a set $$S$$ is inductive if $$\emptyset \in S \land \forall x\in S, x\cup \{x\} \in S$$. The axiom of infinity then states that there exists an inductive set.

Where I'm getting stuck is at even defining the set $$\{x\}$$ in Lean. I know from the axiom of pairing, that there exists a set, which we denote by $$\{x\}$$, which is shorthand for $$\{x,x\}$$, such that $$\forall u, (u\in \{x,x\} \iff u = x \lor u = x)$$.

## What goes wrong

However, in type theory this axiom doesn't give me the actual set, it gives me an inhabitant of the existential proposition type. I've tried to use the "let" command to extract from this the actual set, but I get the error: "invalid match/convoy expression, expected type is not known". This makes me suspect I shouldn't be using this command here at all (I think it's only intended for proofs).

Maybe instead I should be using the axiom of choice?

## My code

constant Set : Type
constant In : Set → Set → Prop
infix  ε:50  := In

axiom pairing : ∀X:Set, ∀Y:Set, ∃S:Set, ∀u, u ε S ↔ u = X ∨ u = Y
axiom union : ∀X, ∀Y, ∃S, ∀u, u ε S ↔ u ε X ∨ u ε Y
infix U:49 := union

definition inductiveset (S:Set) : Prop := ∀x:Set,
let ⟨ (Q:Set), (h: ∀u, u ε S ↔ (u = x ∨ u = x) ) ⟩ := (pairing x x) in
x ε S → (x U Q) ε S

axiom infinity : ∃S, inductiveset S


## Summary

So basically:

• How do I actually define the inductive set property in Lean?

• Can I just extract a function $$f:X\to Y$$ from proof of a proposition $$\forall x:X,\exists y:Y, ...$$?

• should I use the axiom of choice here?

## Edit: Defining an operation from an existence theorem.

unique existence case. Suppose I have the following:

constant T:Type
constants P:T → T → Prop
axiom ....
......
%Now, after 5 pages of lemmas, I prove:
theorem uniqueexistence : ∀t:T, ∃u:T, ( P t u ∧ ∀v:T, ¬v=u → ¬(P t v) )
:= λ t:T, complicated_proof lemma238 t


Suppose I have a Lean file like the one above, How do I then create an operator F:T → T together with a theorem that ∀t:T, P t (F t)?

nonuniqueness case. Similarly, if instead I don't have uniqueness, how do I randomly pick such an operator?

theorem nonuniqueexistence : ∀t:T, ∃u:T, P t u
:= λ t:T, complicated_proof lemma238 t


How do I randomly (using the axiom of choice) pick an operator F:T → T together with a theorem that ∀t:T, P t (F t)?

The existential form of the axioms of set theory is convenient for the meta-theoretic explorations of set theory, such as forcing etc., where it is important to have a minimal language to worry about (only $$\in$$ relation). But even just stating the axioms of set theory without any constants and operation symbols is pretty haunting, see this gist of mine.

If you want a workable set theory you will have to rephrase your axioms so that they are not existential statements but rather operations. For example, define a union : Set → Set → Set operation and an axiom which states that u ε union X Y ↔ u ε X ∨ u ε Y. Formally, set theory does not have these operations, but every single development of set theory relies on the meta-theorem which says that introducing such constants is conservative (they can be eliminated). Also for the inductive set, introduce a constant S : Set and the axiom inductiveset S.

As a general advice, when formalizing mathematics in a proof assistants, one has to be quite flexible about organization of material. Traditional organization is good for teaching and writing textbooks, and so it may not align well with the demands of formalization.

For example, it looks to me at first sight that you would benefit by formalizing not only sets, but also classes. The class comprehension notation $$\{ x \mid \phi(x) \}$$ is very expressive and convenient, and easily formalized in terms of propositional functions on $$\mathsf{Set}$$. With it, you can define many operations on classes and then state that they are sets in terms of axioms. For example, rather than axiomatizing a union operation we just define union X Y to be the class {u | u ε X ∨ u ε Y} and then state that this class is a set. I suppose you could look at Von Neumann–Bernays–Gödel set theory.

• Interesting. This leaves me with two questions: 1. You state that if I want a "workable set theory", then it's better to use operations. But if one actually wants to do set theory (as opposed to using it), in type theory, would that still hold? I'm reminded of Voevodsky remark that all of mathematics might be implemented in type theory one day, and when that happens, would a set theorist (working in type theory) want to introduce these operators, or just work with the axioms? – user56834 Apr 9 at 7:23
• 2. Suppose your operation $F:Set\to Set$ is based on a theorem rather than an axiom, so that (I think) you can't really state $F$ as a constant and then prove a theorem about it. In that case I think you can only state, $\forall X:Set, \exists Y:Set, \phi(X,Y)$, but you can't prove that the constant $F(X)$ returns an element $Y$ s.t. $\phi(X,Y)$, right? – user56834 Apr 9 at 7:27
• @user56834: I am just observing that every set theorist works with operations but claims that they are only a meta-theoretical device. Be that as it may, a formalization will have to account for those operations as well, in one way or another. And I'll live it to the set-theory fans to figure out how to use set theory as a foundation in practice. – Andrej Bauer Apr 9 at 7:28
• Even if you want to "do set theory" (by which I understand you want to study set theory as an object of interest, rather than you use it as a foundation for algebra, analysis, etc.) then you need to deal with the fact that the axioms of set theory are not practically expressible without having some operations available. – Andrej Bauer Apr 9 at 7:31
• You could also use an automatic translation from set theory with operations into one without and foralize the axioms that way (just like I did in the gist I linked to), but good luck with that. – Andrej Bauer Apr 9 at 7:33