Learning Lean through developing ZFC set theory

Stream: maths

[JULIÁN CALDERÓN ALMENDROS]

I'm developing ZFC axiomatic set theory. So far, I've integrated the axioms of extension, existence, comprehension, and pairs. The problem is that I developed ordered pairs using Kuratowski's definition, with the idea that the functions 'fst' and 'snd' on pairs are 'calculable' without using methods like "Classical.choose" of existential type. When I try to formulate a theorem of the type
math \forall (w : U), isOrderedPair w \iff w = \< (fst w) , (snd w)) \>
Which I call "OrderedPair_is_WellConstructed," I have no way to do it. How can I get help? Can I attach the "*.lean" files?
Existence.lean
Extension.lean
Pairing.lean
Specification.lean

[Kenny Lau]

@JULIÁN CALDERÓN ALMENDROS there's #26804 if you want to refer to something; there's basically no need to use ordered pairs

[JULIÁN CALDERÓN ALMENDROS]

@Kenny Lau Thanks. I have to study Mathlib.ModelTheory.Syntax.

[Kenny Lau]

@JULIÁN CALDERÓN ALMENDROS do you plan to do it via the first order logic approach? if not then you should start from the second half of that PR

[Kenny Lau]

we essentially have two definitions of "ring" here, is what I'm trying to say

[Kenny Lau]

you can state the axioms of ring in the logic approach, or you can look at the "actual" class called Ring in lean

[JULIÁN CALDERÓN ALMENDROS]

By now, I'll continue with the exercise I'm doing, but I don't try the theorem that I mentioned. When I finalize this exercise, I'll study the library of language of first order logic and I'll rewrite the ZFC library to approx the mathlib library.

[Kenny Lau]

My point is that using the language of FOL is not necessary unless you want to do FOL.

[Kenny Lau]

you can follow the approach of Ring perfectly fine

[JULIÁN CALDERÓN ALMENDROS]

Ok. My problem is referenced in https://github.com/leanprover-community/mathlib4/pull/26804 from the line 249 to line 268, but the language in https://github.com/leanprover-community/mathlib4/pull/26804/commits/50beedb184cb6166b234acdbc866b78b1e8d2fd6#diff-1edc0416dee77ebc6df2836445d63e6cb38dbbe3e425e97ba8aee2d1716b8f5a is very new for me.

[Terence Tao]

I have a formalization of ZF set theory (with atoms) at Chapter 3 of https://github.com/teorth/analysis that you might find of interest. Ordered pairs are introduced in Section 3.5.