Логика первого порядка и полнота

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

Definition

Логика первого порядка расширяет пропозициональную логику кванторами, охватывающими область объектов, наряду с символами отношений, функций и констант; теорема о полноте утверждает, что предложение выводимо в её системе доказательств именно тогда, когда оно является логическим следствием принятых аксиом.

Scope

Эта тема охватывает синтаксис языков первого порядка, термы, формулы и предложения, семантику структур и выполнимость, понятия общезначимости и логического следствия, дедуктивную систему для логики первого порядка, а также теоремы о корректности и полноте, связывающие доказуемость с истинностью.

Core questions

• Каковы точные синтаксис и семантика логики первого порядка?
• Что означает, что предложение является логическим следствием теории?
• Почему каждое общезначимое предложение формально доказуемо?
• Как полнота связывает систему доказательств с классом всех моделей?

Key theories

Теорема о корректности

Каждое предложение, выводимое в системе доказательств, истинно в каждой модели посылок, поэтому дедуктивная система никогда не доказывает ложных следствий.

Теорема Гёделя о полноте

Напротив, каждое предложение, которое выполняется во всех моделях теории, выводимо из неё, поэтому доказуемость и логическое следствие совпадают для логики первого порядка.

Конструкция Хенкина

Полнота доказывается путём построения модели непосредственно из максимально непротиворечивого множества предложений со свидетелями для экзистенциальных утверждений, что даёт синтаксический рецепт для построения моделей.

Clinical relevance

Логика первого порядка является стандартной основой для формализации математических теорий, а полнота гарантирует, что любая семантическая истина, общая для всех моделей, в принципе может быть доказана, что лежит в основе автоматического доказательства теорем и фундаментальной адекватности аксиоматических систем.

History

Логика первого порядка возникла из «Понятийного письма» Фреге и была выделена как отдельная система Гильбертом и Аккерманом. Гёдель доказал полноту в своей докторской диссертации 1929 года, а конструкция Хенкина 1949 года дала упрощённое доказательство с использованием максимально непротиворечивых множеств, которое является стандартным сегодня.

Key figures

• Gottlob Frege
• Kurt Goedel
• Leon Henkin
• Alfred Tarski

Seminal works

• enderton2001
• marker2002
• shoenfield1967

Frequently asked questions

Чем полнота отличается от теорем Гёделя о неполноте?

Полнота касается логического следствия: каждое предложение, истинное во всех моделях теории, доказуемо. Неполнота касается конкретной теории: достаточно сильная непротиворечивая теория имеет предложения, истинные в её предполагаемой модели, которые она не может доказать. Эти два понятия касаются разных аспектов и не противоречат друг другу.

Почему логика первого порядка является стандартным выбором?

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