Alexander Kuklev (Dec 16 2022 at 21:19): Alexander Kuklev (Dec 16 2022 at 21:19):I've just read “Impredicative Observational Equality” by @Loïc P and @nicolas tabareau and I'm wondering whether it is possible to show (a slight extension of) their Observational Construction Calculus CC_obs to be a conservative extension of ZFC.
It is certainly possible to extend CC_obs by the inductive type V of iterative sets (Aczel’s 1978 model of set theory in type theory) and it seems to be possible to extend the set-theoretical model of CC_obs presented in the paper to model the sets in V directly as sets in the model.
I might be missing something obvious, but it also seems possible to introduce the non-constructive modality on the impredicative universe of definitionally proof-irrelevant types Ω without compromising the computational properties of the CC_obs. One possible form of such modality can be introduced as type former ‖_‖ᶜ : ∗ → Ω such that
Γ, eps : {T} → ‖T‖ᶜ → T ⊢ prf : P
───────────────────────────────────
Γ ⊢ |prf| : ‖P‖ᶜ
That is, ‖P‖ᶜ is populated by proofs of P possibly involving the Lean-style choice operator eps.
If both assumptions turn out to be correct, it should be possible to show that derivable ZFC propositions coincide with derivable CC_obs propositions of the form ‖P‖ᶜ with all quantifiers running over V, where V plays the role of the class of all sets.
Are there any obvious obstacles to this construction?
Loïc P (Dec 16 2022 at 22:32):Hi! I have two minor observations on what you say:
1 - The ZFC equality does not coincide with the observational equality between Aczel sets. You would have to quotient V by Aczel's extensional equality.
2 - If you are able to define V and then show that all ZFC axioms hold in V, then this means that you can prove consistency in ZFC, and you can rephrase this as a statement about V. So for this reason, you are not conservative over ZFC.
Loïc P (Dec 16 2022 at 22:39):Also, you might be interested in the paper "Sets in types, types in sets" by Benjamin Werner, if you don't know it already.
In this paper, Werner explains how to encode ZFC in the Calculus of Inductive Constructions with excluded middle, and two other axioms that he calls TTDA and TTCA. He also gave a formal Coq proof here: https://github.com/coq-contribs/zfc .
It seems to me that EM, TTDA and TTCA are derivable if you use your non-constructive modality ‖_‖ᶜ.
I imagine that you can reproduce Werner's construction and obtain that CC^obs+‖_‖ᶜ with one universe can be encoded in ZFC with one Grothendieck universe, which can be encoded in CC^obs+‖_‖ᶜ with two universes, which can be encoded in ZFC with two universes, etc
Last updated: Dec 06 2023 at 15:01 UTC