Формальные системы, объяснённые честно
Более понятная интерактивная страница о формальных системах, аксиомах, выводах, непротиворечивости и о том, почему возникает неполнота.
Это учебный симулятор формальной системы. Он не доказывает теоремы Гёделя напрямую. Он помогает увидеть, что делают аксиомы, как растут выводы и почему «добавление новых аксиом» не устраняет неполноту магическим образом.
Каждый шаг ниже — это либо исходная аксиома, либо выведенное утверждение, полученное учебным движком.
Это утверждения, которые симулятор может вывести следующими из текущих аксиом и уже известных утверждений.
Формальная система начинается с аксиом и использует правила вывода для получения теорем. Главный вопрос состоит не только в том, что можно вывести, но и в том, что нельзя вывести, не разрушив непротиворечивость.
Гёдель закодировал формулы и доказательства числами, а затем построил предложение, которое по сути говорит: «Я недоказуем в этой системе». Если система непротиворечива, это предложение нельзя доказать внутри системы, хотя в предполагаемой интерпретации оно истинно.
Эта страница моделирует небольшой движок правил, чтобы показать, как аксиомы расширяют теорию. Она не реализует полную арифметику первого порядка, нумерацию Гёделя или настоящую проверку доказательств. Это концептуальный мост, а не помощник по доказательствам.