∀ P, (∀ x, ∃ y, P x y) → ∃ F, ∀ x, P x (F x)

Hey chouck, just like that it might not be possible to construct such a function. It all depends on the type of `P`

. So what's the type of `P`

?

Thank you Forster. Maybe as general as possible. Type -> Type -> Prop

That's not really as general as possible. For instance `P (n : nat) (m : nat) := m = 2 * n`

is not covered by this type anymore

Maybe let's take it from the other side: Why do you need such a function?

@choukh Assuming you mean `P : T1 -> T2 -> Prop`

for (to be quantified) types `T1`

and `T2`

, this is just the axiom of choice: https://coq.inria.fr/library/Coq.Logic.ClassicalChoice.html

So we need additional axiom to prove this? What if ∀ P, (∀ x, ∃! y, P x y) → ∃ F, ∀ x, P x (F x)

Actually, I'm trying to formalize Axiom schema of replacement of set theory and trying to choose the right form. whether using prop or just function to represent the replacement rule.

Aha, it's helpful to know what you're after :) @Dominik Kirst can help you out here!

@choukh even your second version assuming that P is functional is not provable, that's now one version to state the unique choice axiom in Coq.

Interesting that this popped up when formulating the replacement axiom, can give a bit more detail how your representation looks like? Do you assume a type of sets satisfying the ZF axioms?

Yes! I assume a type of sets. At first I tried this form

Parameter Repl : (set → set) → set → set.

Axiom ReplAx : ∀ y F X, y ∈ Repl F X ↔ ∃ x, x ∈ X ∧ F x = y.

But later realize that it might be not enough to prove transfinite recursion theorem. So I change it like this.

Parameter Repl : (set → set → Prop) → set → set.

Axiom ReplAx : ∀ (P : set → set → Prop) A,

(∀ x, x ∈ A → ∃! y, P x y) →

∀ y, y ∈ Repl P A ↔ ∃x ∈ A, P x y.

I wonder thay are somehow equivalent

Ah I see, this looks familiar ;-)

Indeed, both variants are equivalent exactly iff you have unique choice on your set type.

This is btw discussed in Section 2.3 of our paper on higher-order set theory:

https://www.ps.uni-saarland.de/Publications/documents/KirstSmolka_2018_Categoricity.pdf

Thank you very much Kirst. I have so much to learn. May I ask one further question here?

Is the set theory with choice on type equivalent to the one without it but with AC on set side?

@Dominik Kirst Nice to see that this was extended into a journal paper.

That's a very good question and, roughly, the answer is yes. Assuming the type-theoretic choice axiom you have formulated above on your set type is equivalent to assuming that this model satisfies the usual set-theoretic AC. You'll find one direction as Fact 48 in the linked paper.

However, note that this correspondence really relies on your higher-order formulation of replacement, where you quantify over all binary relations P. This is much stronger than the usual first-order scheme, where you only quantify over those relations that can be represented as a first-order formula. With just the first-order replacement axiom, the connection of choice on type level and set level is lost/avoided.

So if I want ZF I better use functional replacement with unique choice or just propositional replacement without any choice?

Hm as both are interdefinable it doesn't make a big difference, I'd probably say that relational (or propositional as you say) replacement looks more similar to the usual scheme. And if you want to really axiomatise ZF and not a stronger higher-order variant, I see no way around making the first-order syntax explicit :)

Well, I'm just trying to figure out how the set theory I build inside coq is different from those in textbook. What I now understand is that what inside coq is inevitably in higher-order while those in textbook are usually just in first-order.

I see, in my opinion exploring set theory in Coq's type theory is a very interesting topic :)

As you say, the natural axiomatisation in Coq is higher-order and so you encounter all the usual side-effects of the first-order vs. higher-order question. Probably most strikingly, up to height you only have one model of ZF2 while ZF admits all these peculiar non-standard models. In particular the single ZF2 model is uncountable since the cardinality notions on both levels coincide, so the Löwenheim-Skolem theorem doesn't apply to ZF2.

choukh said:

Well, I'm just trying to figure out how the set theory I build inside coq is different from those in textbook. What I now understand is that what inside coq is inevitably in higher-order while those in textbook are usually just in first-order.

This is not entirely true. You can surely encode first-order formulas and hence the usual ZF in Coq. However, this requires a deep embedding of FOL in Coq and may thus not be an easy theory to work with. IIRC, Isabelle/ZF is based on Isabelle/FOL and as such yields the original ZF set theory. @Dominik Kirst probably knows whether this has been done in Coq already or not.

This is of course right, encoding first-order ZF in Coq can be done, and in fact I have done it recently to mechanise an undecidability/incompleteness proof of ZF. I'd say it's just not the rendering of set theory you'd come up with if you start from scratch in Coq, since then most likely you'll find the higher-order axioms more natural (and maybe even don't notice they are stronger).

Dominik Kirst said:

... (and maybe even don't notice they are stronger).

IIRC, this "maybe" has quite a few instances among the (former) employees of a certain professor in Saarbrücken. :grinning_face_with_smiling_eyes:

:grinning_face_with_smiling_eyes:

But yes, you most certainly want to turn the "replacement" scheme into a single axiom, and the second-order version almost suggests itself. It just happens to be "wrong" if your intention is to talk about the textbook ZF.

And even if you want to express a result from textbook ZF it's probably a reasonable way to use ZF2 and handwave why your proof in principle could have been done in ZF...

But then, if your starting point is type theory, then you probably don't consider FOL+ZF to be *the* foundation of mathematics. From there on those are just two theories. Admittedly, ZF2 is a bit "shallow" as witnessed by choice leaking into and out of the theory...

For sure, when mechanising a textbook proof in ZF2 and then handwaving that it can be done in ZF the overall amount of handwaving is less than what is used in the textbook proof. So mechanising more textbook proofs in ZF2 is a step in the right direction.

@Dominik Kirst by the way, is your work in ZF2 readily installable via OPAM? I'm thinking that this might actually be a candidate for inclusion in coq-community.

At the moment the developments aren't fully unified, the recent proof of Sierpinski's theorem in ZF2 with Felix Rech is based on a slightly different axiomatisation. I plan to unify this with the rest on categoricity and model constructions in near future though. In particular if you think that would be a good idea I'll certainly find the motivation to do this :wink:

I mostly agree to your judgement, if one accepts such a strong type theory as Coq, there is not much reason to then take the detour and fall back to weaker set theories. On the other hand ZF2 is a really nice way to make a lot of ideas explicit that are somewhat implicit in first-order ZF, like inductive and recursive definitions or higher-order quantification that suffer from first-order encodings. So many set-theoretic results have more direct formal counterparts in ZF2 and there is at least some historic evidence that Zermelo intended the original axioms to be understood higher-order.

Dominik Kirst said:

At the moment the developments aren't fully unified, the recent proof of Sierpinski's theorem in ZF2 with Felix Rech is based on a slightly different axiomatisation. I plan to unify this with the rest on categoricity and model constructions in near future though. In particular if you think that would be a good idea I'll certainly find the motivation to do this :wink:

Well, there are two things here: I think set theory is important enough to want an easily installable (and maintained) package, so that not everyone needs to roll their own. Also I think your results are nice and instructive and definitely worth preserving. To be in coq-community, you need to find a maintainer (which can be you, of course), but you can also try to find co-maintainers. Also coq-community mandates a CI setup, so you will know when things break, and might have an easier time getting help, if needed.

It would be really great if there was a set theory library.

Christian Doczkal said:

To be in coq-community, you need to find a maintainer (which can be you, of course), but you can also try to find co-maintainers. Also coq-community mandates a CI setup, so you will know when things break, and might have an easier time getting help, if needed.

What's the advantage of having the repo in `coq-community`

rather than in an organisation (e.g. our `uds-psl`

GitHub organisation)?

I suppose the main advantage is visibility, in particular as it comes to a potential "maintainer wanted" issue down the road. In anyevent, the first step is a unified development with OPAM packages and a CI setup. Where the repository is located is secondary.

choukh has marked this topic as resolved.

Last updated: Jun 18 2024 at 00:02 UTC