Корректность и полнота логики предикатов
Множество правил вывода для логики предикатов обладает свойством корректности и полноты подобно свойствам пропозициональных выводов.
Теорема корректности. Если существует вывод замкнутой формулы F из множества формул G, тогда G влечёт F.
Теорема полноты. Для любой замкнутой формулы F и любого множества предложений G, если G влечёт F, то существует вывод F из некоторого подмножества G.
Полнота логики предикатов для случая счётного G и для другого множества правил вывода была доказана Куртом Гёделем в 1930 году.
Функциональные символы и равенство: синтаксис
Логика предикатов, определённая выше немного более ограничена, чем что обыкновенно называется ``логикой первого порядка'', и наша следующая цель – удалить эти ограничения. Во-первых, мы обобщим понятие терма. В дополнение к объектным константам и объектным переменным, мы разрешим построение термов с использованием символов для функций, ``функциональных констант''. Во-вторых, мы добавим к языку знак равенства, и уравнения будут включены как новый тип атомарных формул.
Наше наиболее общее понятие сигнатуры определяется следующим образом.
Определение (Сигнатура,константы). Сигнатура – это множество символов двух типов – функциональных констант и предикатных констант – с неотрицательным целым числом, называемым арностью, связанным с каждым символом. Объектная константа – это функциональная константа арности 0. Функциональная константа унарна, если её арность равна 1, и бинарна, если её арность равна 2. Пропозициональная константы, так же как унарные и бинарные предикатные константы, определены как выше.
Определение (Терм). Возьмём сигнатуру s, не включающую ни дополнительных символов, указанных в начале данной части, ни знака равенства. Множество X строк замкнуто относительно правил построения термов, если
- каждая объектная константа принадлежит X,- каждая объектная переменная принадлежит X,
- для каждой функциональной константы h арности n (n > 0) и любой строки t1, ... , tn,
если t1, ... , tn принадлежит X, тогда также принадлежит h(t1, ... , tn).
Строка является термом, если она принадлежит все множествам, которые замкнуты относительно правил построения.
Каждый терм содержит объектную константу или объектную переменную. Верно или нет ?
В логике первого порядка существуют три типа атомарных формул:
- пропозициональные константы,- строки вида R(t1, ... , tn) где R – предикатная константа арности n (n > 0) и t1, ..., tn – термы,
- строки вида (t1 = t2), где t1, t2 – термы.
Взяв в качестве множества атомарных формул данное множество, мы получаем, что определение формул (первого порядка) совпадает с определением предикатных формул в начале этой части.
Для любых термов t1 и t2, t1 № t2 обозначает формулу ¬(t1 = t2).
