17 июля 2011 · Комментарий

Без заголовка

Имя не сохранено · Оригинал в ЖЖ ↗ · Ссылка на запись

Но для Ваших инженеров-программистов такая математика ИМХО глубоко избыточна. Если уж их грузить, тогда FOL и HOL логиками и изложением математики на них, например конструктивным. На мой скромный взгляд, актуальная математика будущего будет основана на вычислимых HOL системах. Ну что-то конечно на FOL. Бумажные доказательства естественно останутся, но это удел суровых логиков (например доказательства мета-теорий) и математиков, а инженерам-программистам - компьютер. С другой стороны для мета-теорий тоже делают формальные компьютерные системы.