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)
?