I’m attempting to follow along in Coq with this paper showing that the statement of the Cantor-Bernstein Theorem implies the law of excluded middle (but using coinductively defined conatural numbers rather than the definition of ℕ∞ given in the paper), and I’m hitting a wall right around Lemma 3.5:
Let Q ∈ 2^ℕ∞ be given. If Q(ω) = 1 and ∀n ∈ ℕ. Q(n) = 1, then ∀p ∈ 2^ℕ∞. Q(p) = 1.
My understanding is that this statement remains ‘true’ constructively because, even if without EM there may be multiple infinite conaturals, no definable predicate should ever be able to distinguish them; hence Q(ω) = 1 implies Q(n) = 1 for all infinite n. Which leads me to the following development:
CoInductive conat: Set :=
| Zero: conat
| Succ: conat → conat.
CoInductive Eq: conat → conat → Prop :=
| Eq_0: Eq Zero Zero
| Eq_S: ∀ a a', Eq a a' → Eq (Succ a) (Succ a').
CoFixpoint ω := Succ ω.
(* ...and after proving some basic properties... *)
Lemma ω_indiscernibility: ∀ (p: conat → bool), ∀ a, Eq ω a → p ω = p a.
Proof.
(* ??? *)
I’m really not sure how to go about proving this, or even whether it is provable. I can’t use a cofixpoint since I’m not producing a value of a coinductive type, and I can’t really use a fixpoint either since all my inputs are coinductive, which doesn’t leave much to work with and makes me wonder if this is just impossible without extra axioms. Is that the case?
(Note: The proof in the paper presumes functional extensionality, which is reasonable since it is a paper about set theory and so the functions are in fact sets. I could assume extensionality if necessary, at least as an added hypothesis, but would like to know first that it really is necessary.)
(Also note: I know positive-syntax coinductive definitions are somewhat disreputable now, so there’s no need to inform me)
To expand a bit on the SE post regarding your question: your lemma is basically the equivalent of function extensionality for a coinductive type, so most of what applies to funext applies here too. The lemma is not provable in vanilla Coq, but it is in other type theories, and it is a very reasonable axiom to assert if you need it. Just as with funext, there is also the alternative of using bisimilarity (what you called Eq) as you primary notion of “equality” (this is the equivalent of using pointwise equality of functions) and to juggle a bit to try and avoid using the axiom. Depending on what you want to do this might be doable, or be too much of a hassle, in which case assuming the axiom probably is the way to go.
Well, good to know it’s not provable so I can stop trying to prove it, at least. I had read (indeed had already read before posting) the SE discussion linked but didn’t think it quite answered my question, since it seemed the statement I was trying to prove was quite a bit weaker than on-the-nose equality. And indeed it is a bit weaker, but I guess still not weak enough to be provably true!
I’d like it if you could expand on the statement that this hypothesis is equivalent to functional extensionality, because it seems to me more like a sort of dual or converse thereof (it says that bisimilarity implies indiscernibility, not the other way around). This distinction, along with my inability to imagine a model where the hypothesis fails, is why I had thought it might actually be possible to prove.
For now I can already see that the proof I’m reading should go through if I admit this one hypothesis, in effect becoming a proof of “Cantor-Bernstein + [this axiom] => excluded-middle” rather than just “Cantor-Bernstein => excluded-middle”. I’m still interested in whether the latter is the case for Coq, so I might still spend some time seeing if it’s possible to work around it.
First, note that equality is a way to internalize indiscernability, since we can easily prove forall (A : Type) (x y : A), x = y <-> (forall (P : A -> Prop), P x -> P y). One direction of the equivalence is the induction principle of equality, while the other is obtained by taking P to be fun y => x = y and proving P x by reflexivity.
But you are right, I misread your lemma: using bool restricts to those propositions that can be expressed as a boolean, which is weaker than indiscernability in the propositional sense above. So indeed your statement is weaker than full bisimilarity-implies-equality.
To see the link of this with functional extensionality, the idea is the following: in both cases it says that two objects that are “observationally the same” (in the case of funext, applying the functions to equal arguments leads to equal outputs, in your case Eq says that you will always have the same observation = constructor on both sides) are actually equal. Counter-models to funext are models where functions contain some “intentional” content, ie two functions can be distinguished even if they output the same values. A very simple such model (presented in The next 700 syntactical models of type theory - Inria) interprets the function type A -> B as the type (A -> B) × bool, so that a function now contains a boolean. This boolean is discarded when applying functions, so that you cannot observe it this way, but still two functions can be extensionally equal but disagree on the boolean, making them non-equal. The exact same game can be played with co-inductive types such as your conat, interpreting it as conat × bool. Here the conaturals in the model (Zero,true) and (Zero,false) would be related by Eq since they have the same constructor, but they are not equal.
Regarding your last point : if I understood correctly, the proof you are reading is already a proof of “Cantor-Bernstein + funext => EM”, no? If this is the case, you might think of your axiom as replacing/extending the extensionality axiom expected by the proof? But I agree that this might be a bit unsatisfying, and you might be able to avoid it. The general idea is that while your lemma is not provable for an arbitrary p, it will still hold for specific p, so what you would have to do is to prove it on a by-case basis rather than in a general way.
I wrote a long reply to this trying to make clear just what I was still not totally understanding, and in the process of writing it convinced myself that I did understand it after all. My problem was never with the idea that “observationally the same” objects might be unequal–such as in the invisible-attached-boolean model you gave. What did surprise me at first what that we could safely postulate a total functionp: conat -> bool that, I guess, peeks at the invisible boolean value and tells us what it is! But, on further reflection, we postulate that sort of thing all the time in classical mathematics (e.g. whenever we talk about the characteristic function of some set whose membership is undecidable) and this case is no stranger than those. I suppose I got too hung up on the constructive, computational interpretation of terms to realize that immediately.
At any rate, it sounds likely I will need to assume some additional axioms to get this proof to go through. (I may be able to turn it into a proof that a sort of “Cantor-Bernstein for setoids” implies EM, which is not quite the same thing but would still be interesting.)
I guess the weird part is not that much about postulating the function by itself (after all, it could very well be the constant function), but what you postulate on top of its existence, say on its value on some inputs, to reflect the fact that it is really “peaking at the invisible boolean”. Things get trickier there… I actually wonder what parts of the existence of an “invisible boolean” you can reflect from the model into the source theory.
Just out of curiosity since I also did this proof in Coq a while ago: do you expect that you can derive EM for all propositions from Cantor-Bernstein or only for the proof-irrelevant ones? Because I did not only assume function extensionality but also proof irrelevance to simulate their IZF setting. But in any case it would be interesting to see a setoid generalisation working around these assumptions
Yes, I didn’t mention it here since it wasn’t germane to my original question, but I did realize after having asked it that the proof also depends on proof-irrelevance, in that it works in a theory with “real” subsets as opposed to Σ-types. So as you said, by assuming functional extensionality or some variation thereon one can follow the paper to prove forall P, Squash (P \/ ~P) but not forall P, P \/ ~P without also assuming proof irrelevance in Prop. If there is a way around this I haven’t thought of it… as far as I know the theory of Coq puts no upper bound on the possible cardinality of a Prop, does it? (I’ve never heard of anyone proposing a “proof countability” axiom, so would actually find it pretty funny if it turned out to suffice here!)
Since you’ve already completed this exercise—and so have I, modulo a few “admit” lines that I can easily replace with the needed axioms—I think it would be interesting to continue by formulating a “Cantor-Bernstein for setoids” axiom, and seeing if that axiom alone suffices to prove excluded middle, so that’s probably what I’ll do.
