← Прорыв мыслитель 5 из 12

Курт Гёдель

1906–1978

Главный урок

Чтобы найти предел системы, опиши её полностью на её же языке. Гёдель заставил математику сказать о себе то, что она не хотела говорить.

Когда

1931 — 25 лет. Статья «Über formal unentscheidbare Sätze». Доказательство теорем о неполноте. Переворот в основаниях математики.

1940 — доказательство теоремы полноты для модальной логики.

Вся жизнь — Венский кружок, потом Принстон. Друг Эйнштейна, они вместе ходили на прогулки до конца жизни Эйнштейна.

Контекст

Венский кружок, 1920–30-е. Группа философов и учёных, верящих в программу Гильберта: можно ли обосновать всю математику на конечной, непротиворечивой системе аксиом?

Гёдель не пытался опровергнуть Гильберта. Он хотел понять пределы этой программы. И нашёл их.

Логическая цепочка

  1. Вопрос: можно ли доказать все истины математики в рамках одной формальной системы?
  2. Гёдель переформулировал: что значит «доказуемо в системе»? Можно ли это определить внутри самой системы?
  3. Изобрёл арифметизацию метаматематики: каждое утверждение о числах можно закодировать числом. Каждое доказательство — тоже числом.
  4. Теперь система может говорить о самой себе. Утверждение: «Я недоказуемо в этой системе».
  5. Два случая: если оно доказуемо — то утверждение ложно. Противоречие. Если недоказуемо — то утверждение истинно. И есть истина, которую нельзя доказать.
  6. Вывод: любая достаточно мощная формальная система неполна. Не «может быть неполна» — обязательно.

Как ему это удавалось

  • Формализация того, что обычно остаётся неформальным. «Доказуемость» — это мета-понятие. Гёдель сделал его частью системы.
  • Самоотсылка как инструмент. Использовал способность системы говорить о себе.
  • Строил на чужих результатах. Кантор (диагональный аргумент), Рассел (парадоксы), Гильберт (формализм).
  • Не пытался опровергать — пытался уточнить. Это не атака на Гильберта, а развитие его программы.

Что отсюда можно взять

  • Чтобы найти предел системы, опиши её полностью. Полуформальное описание — где прячутся скрытые допущения.
  • Самоотсылка — это не баг, а инструмент. Система, которая может говорить о себе, способна увидеть свои пределы.
  • Используй саму систему как инструмент анализа. Гёдель использовал формальные методы, чтобы доказать ограничения формальных методов.
  • Переформулируй мета-понятие как объект системы. Часто это открывает то, что раньше было невидимо.

Связанные