Решетка Медведева (Роджерс).

[george66]

Это очень известный результат, в теории множеств известный как лемма Кёнига (если дерево с конечным ветвлением бесконечно, то в нём есть бесконечный путь). Играет особую роль в интуиционизме Брауэра в виде так называемой теоремы о веере (она немного сложнее формулируется). Брауэр, отказавшись от закона исключённого третьего, не мог доказать многих результатов из анализа (например, что функция, непрерывная на отрезке, равномерно непрерывна на нём). Он добавил новую аксиому (так называемую бар-индукцию), которая доказуема классически (от противного) и позволяет доказать, что дерево с конечным ветвлением, у которого все ветви конечны, имеет конечную высоту (и потому конечное число узлов). Это позволило ему всё доказать в анализе, но вызвало большие споры. Сейчас это делают хитрее.

[пианист]

Не знал. Но все равно, достойно упоминания, потому что штучка изящная.
Очень интересно. А что это за хитрый способ?

[george66]

Когда дочитаете Роджерса и Барендрегта, попробуйте Драгалина "Математический интуиционизм".