Интуиционистская лемма Цорна

[akuklev]

Как известно, в интуиционистских теориях типов определимы только вычислимые тотальные `f : A -> B`. Теория типов не утверждает, что внутри типа функций `A -> B` не живёт ещё каких-нибудь (невычислимых) функций, но вот конкретно предьявить можно только тотально-вычислимые. А это означает, что у нас не может быть Тьюринг-полноты, т.е. как бы не была

Comments

[thread2]

мне кажется, это лучше спрашивать вот здесь : math.stackexchange.com

[66george]

Не знаю, но вот классика
https://core.ac.uk/download/pdf/81927529.pdf
Питер Фрейд доказал, что теорема Цермело в какой-то форме верна интуиционистски. Доказательство сложное, через топосы, но затем Тодд Вилсон дал доказательство на три странички с кванторами по высказываниям
https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/an-intuitionistic-version-of-zermelos-proof-that-every-choice-set-can-be-wellordered/C459B418A42FACF9F0D9ED4CC7B77A8F

[akuklev]

Спасибо!

[66george]

Это (статья Тодда Вилсона) одно из немногих интересных применений кванторов по высказываниям. Ещё формула Джибладзе, объект Хиггса и совсем простые применения в топосных "топологиях". Впечатление, что мы только поскребли поверхность.

[66george]

Внезапно нашёл Тодда Вилсона на линкедине. Он жив и даже на профессорской ставке (computer science, калифорнийский университет Фресно), но ничего не пишет с 2001-го года. Я его спросил, писал ли он что-то ещё после статьи о теореме Цермело. Он ответил "нет, по этой теме ничего не писал". Но и по другим темам тоже ничего не находится. Может, он в тюрьме сидел, но тогда как его взяли профессором?