Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
at axiom of choice into the section In dependent type theory I have moved the explicit statement taken from the entry of dependent type theory (see there for what I am talking about in the following).
One technical question: do we need the
: true
at the very end of the formal statement of the theorem?
One conceptual question: I feel inclined to add the following Remark to that, on how to think about the fact that the axiom of choice is always true in this sense in type theory. But please let me know what you think:
Heuristically, the reason that the axiom of choice is always true when formulated internally this way in dependent type theory is due to the fact that its assumption thereby is stated in constructive mathematics:
Stated in informal but internal logic, the axiom of choice says:
If $B \to A$ is a map all whose fibers are inhabited, then there is a section.
But now if we interpret the assumption clause
a map all whose fibers are inhabited
constructively, we have to provide a constructive proof that indeed the fibers are inhabited. But such a constructive proof is a choice of section.
So constructively and internally the axiom is reduced to “If there is a section then there is a section.” And so indeed this is always true.
Would you agree that this captures the state of affairs?
The thing appearing on the right-hand side of a turnstyle $\vdash$ must always be a judgment. If we left off the $:true$ then we would have a type or a proposition, not a judgment. A proposition $P$ gives rise to a judgment “$P$ is true” which apparently someone has notated here as “$P:true$”. I’ve never seen that notation elsewhere – it seems odd since “true” is not a type to which “P” belongs; instead I’ve seen that judgment written as “$P$ true”. Another, probably even better, option would be to say that there is a term $t$ such that $...\vdash t:P$.
Your Remark is probably something that constructivists who believe in calling this “a proof of the axiom of choice” would agree with. But I am not such a constructivist, and I disagree with it. To me, it is perfectly possible to give a constructive proof that the fibers are all inhabited without giving a section. It is the difference between giving a section of $B\to A$ and giving a section of its (-1)-truncation.
Okay, so how would you say in words what is going on in that “type-theoretic proof of the axiom of choice”?
A map that has a section of its (-1)-truncation also has a section itself.
?
Hm, but maybe I misunderstood what you were saying. You are actually disagreeing with calling
$\Gamma \vdash (\forall x : A) (\exists y : B(x)) C(x, y) \to (\exists f : (\Pi x : A)B(x) )(\forall x : A) C(x, \mathrm{apply}(f, x)) \; \mathrm{true}$
a statement of an axiom of choice, right?
And there is no (-1)-truncation in this statement, actually, you were just referrring to my use of the word “inhabited”, which, I guess, you would demand to see for something that actually deserves to be called a statement of the axiom of choice. Is that right?
Finally, while, therefore, my heuristics about proving “if there is a section then there is a section” would therefore not apply to a statement that actually involves a (-1)-truncation, it does capture what the above formal expression actually expresses, right?
You are actually disagreeing with calling […] a statement of an axiom of choice, right?
Yes. I would state that theorem as “if there is a function assigning to each $x:A$ an element $y:B$ together with an element $z:C(x,y)$, then there is a function $f$ assigning to each $x:A$ an element $f(x):B$, and also another function $g$ assigning to each $x:A$ an element $g(x):C(x,f(x))$. It’s basically the statement that a (dependent) function with two outputs (one dependent on the other) can be broken apart into two (dependent) functions with one ouput each (with the type of the second involving the first). Useful, certainly, but I think calling it “the axiom of choice” is an insult to the deep mathematics surrounding the latter.
Oh, I see. I assumed (without checking) that you put that paragraph into the entry Martin-Löf dependent type theory. This has been there for ages. I was staring at it and trying to understand the terminology. That’s where my question above arises from.
Okay, so then I now remove again the copy of that discussion which I had moved to “axiom of choice” and you please see if you find a minute to do something about the paragraph in the Martin-Löf dependent type theory entry.
I have googled around a bit:
the interpretation of that statement as an internal axiom of choice is promoted on this page here:
It seems that Bell is referring to some text
for that formulation of the axiom of choice, the one that you are objecting to. He calls it the “logical form of the axiom of choice”, abbreviated ACL.
Well, you may know all this. But eventually we need to make sure that the reader of the $n$Lab entry knows it, too.
After editing it I see that what now is remark 2 here refers to this issue. I didn’t even see that remark before. Somehow I find it a bit vague, because the discussion seems to be mixing the informal question of what deserves to be called the axiom of choice with other formal matters.
But all right, I leave this the way it is now, need to be doing something else.
1 to 8 of 8