axiom of choice and Martin-Löf Intuitionistic Set Theory

[juan_gandhi]

So, I took a look at this clarification from Stanford texts.

And so, it seems like yes, the axiom of choice as formulated in his so-called intuitionistic set theory is actually the corollary of what one could call axiomatics of the intuitionistic set theory if there were one. What there is is a set of vague intuitive assumptions.

Intuitive is not intuitionistic, you know.

And AC implies Boolean logic, in case you did not know.

So, I think now that it is all wrong.

Basically, there's no such thing as Intuitionistic Set Theory.

But a funny, although hardly provable, corollary of all this is that dependent types imply booleanness. In the form it is now popularized.

Personally, I don't believe it. I believe we still can have dependent types (objects of the form ΠA_{x) without having to have Boolean logic.}

Comments

[nivanych.livejournal.com]

Мы можем даже иметь булевость, но не использовать её.

[ivan-gandhi.livejournal.com]

Да ей неоткуда на самом деле взяться. Надо разобраться, откуда же на самом деле у него это берётся. Тут что-то не так же.

[nivanych.livejournal.com]

Тут есть тонкость, связанная с "физическим смыслом".
Мы всегда можем сказать, что (например) все возможные лямбда-выражения есть множество, и например, рассуждать о выражениях, которые входят в конкретное подмножество или не входят. И когда-то, это бываает удобно и нужно.
В тех же топосах, мы вполне можем работать с такими вещами, "наблюдая со стороны", то есть, не имея никакой булевости.
Но вот, по моему скромному мнению, в базе логики булевость совершенно не нужна, раз её можно ввести потом. И уж если есть в распоряжении логика высокого порядка, то имхо, это совсем очевидно.