choukh (Dec 03 2020 at 09:58): choukh (Dec 03 2020 at 09:58):∀ P, (∀ x, ∃ y, P x y) → ∃ F, ∀ x, P x (F x)
Yannick Forster (Dec 03 2020 at 10:01):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?
choukh (Dec 03 2020 at 10:05):Thank you Forster. Maybe as general as possible. Type -> Type -> Prop
Yannick Forster (Dec 03 2020 at 10:07):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
Yannick Forster (Dec 03 2020 at 10:07):Maybe let's take it from the other side: Why do you need such a function?
Christian Doczkal (Dec 03 2020 at 10:10):@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
choukh (Dec 03 2020 at 10:13):So we need additional axiom to prove this? What if ∀ P, (∀ x, ∃! y, P x y) → ∃ F, ∀ x, P x (F x)
choukh (Dec 03 2020 at 10:15):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.
Yannick Forster (Dec 03 2020 at 10:22):Aha, it's helpful to know what you're after :) @Dominik Kirst can help you out here!
Dominik Kirst (Dec 03 2020 at 10:29):@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?
choukh (Dec 03 2020 at 10:37):Yes! I assume a type of sets. At first I tried this form
choukh (Dec 03 2020 at 10:37):Parameter Repl : (set → set) → set → set.
Axiom ReplAx : ∀ y F X, y ∈ Repl F X ↔ ∃ x, x ∈ X ∧ F x = y.
choukh (Dec 03 2020 at 10:38):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.
choukh (Dec 03 2020 at 10:40):I wonder thay are somehow equivalent
Dominik Kirst (Dec 03 2020 at 10:57):Ah I see, this looks familiar ;-)
Indeed, both variants are equivalent exactly iff you have unique choice on your set type.
Dominik Kirst (Dec 03 2020 at 10:58):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
choukh (Dec 03 2020 at 11:37):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?
Christian Doczkal (Dec 03 2020 at 12:06):@Dominik Kirst Nice to see that this was extended into a journal paper.
Dominik Kirst (Dec 03 2020 at 12:58):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.
Dominik Kirst (Dec 03 2020 at 13:02):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.
choukh (Dec 03 2020 at 14:18):So if I want ZF I better use functional replacement with unique choice or just propositional replacement without any choice?
Dominik Kirst (Dec 03 2020 at 15:00):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 :)
choukh (Dec 03 2020 at 15:36):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.
Dominik Kirst (Dec 03 2020 at 16:38):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.
Christian Doczkal (Dec 03 2020 at 16:57):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.
Dominik Kirst (Dec 03 2020 at 17:10):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).
Christian Doczkal (Dec 03 2020 at 17:13):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:
Dominik Kirst (Dec 03 2020 at 17:16)::grinning_face_with_smiling_eyes:
Christian Doczkal (Dec 03 2020 at 17:17):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.
Dominik Kirst (Dec 03 2020 at 17:20):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...
Christian Doczkal (Dec 03 2020 at 17:21):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...
Yannick Forster (Dec 03 2020 at 17:25):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.
Christian Doczkal (Dec 03 2020 at 17:30):@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.
Dominik Kirst (Dec 03 2020 at 17:53):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:
Dominik Kirst (Dec 03 2020 at 17:58):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.
Christian Doczkal (Dec 03 2020 at 18:23):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.
choukh (Dec 04 2020 at 00:00):It would be really great if there was a set theory library.
Yannick Forster (Dec 04 2020 at 08:44):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)?
Christian Doczkal (Dec 04 2020 at 09:03):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.
Notification Bot (May 14 2022 at 07:56):choukh has marked this topic as resolved.
Last updated: Oct 01 2023 at 19:01 UTC