Правила для кванторов всеобщности
|
| ||||||||||||||||
где v не является свободной | где t является | ||||||||||||||||
переменной для любой формулы в G | подстановочным для v в F(v) | ||||||||||||||||
В каждой из следующих задач выведите данную формулу из пустого множества посылок.
3.19(P(a) & " x (P(x) Й Q(x))) Й Q(a).
3.20" xy P(x, y) Й " x P (x, x).
Правила для кванторов существования
|
| ||||||||||||||||
где t – подстановочный | где для C и любой формулы из G | ||||||||||||||||
для v в F(v) | v не является свободной переменной | ||||||||||||||||
В каждой из следующих задач выведите данную формулу из пустого множества посылок.
3.21(P(a) Ъ P(b)) Й $ x P(x).
3.22$ x P(x) є " x P(x).
Корректность и полнота логики предикатов
Множество правил вывода для логики предикатов обладает свойством корректности и полноты подобно свойствам пропозициональных выводов.
Теорема корректности.Если существует вывод замкнутой формулы F из множества формул G, тогда G влечёт F.
Теорема полноты.Для любой замкнутой формулы F и любого множества предложений G, если G влечёт F, то существует вывод F из некоторого подмножества G.
Полнота логики предикатов для случая счётного G и для другого множества правил вывода была доказана Куртом Гёделем в 1930 году.
|
|
Функциональные символы и равенство: синтаксис
Логика предикатов, определённая выше немного более ограничена, чем что обыкновенно называется ``логикой первого порядка'', и наша следующая цель – удалить эти ограничения. Во-первых, мы обобщим понятие терма. В дополнение к объектным константам и объектным переменным, мы разрешим построение термов с использованием символов для функций, ``функциональных констант''. Во-вторых, мы добавим к языку знак равенства, и уравнения будут включены как новый тип атомарных формул.
Наше наиболее общее понятие сигнатуры определяется следующим образом.
Определение 28 (Сигнатура,константы).Сигнатура – это множество символов двух типов – функциональных констант и предикатных констант – с неотрицательным целым числом, называемым арностью, связанным с каждым символом. Объектная константа – это функциональная константа арности 0. Функциональная константа унарна, если её арность равна 1, и бинарна, если её арность равна 2. Пропозициональная константы, так же как унарные и бинарные предикатные константы, определены как выше.
Определение 29 (Терм).Возьмём сигнатуру s, не включающую ни дополнительных символов, указанных в начале данной части, ни знака равенства. Множество X строк замкнуто относительно правил построения термов, если
|
|
- каждая объектная константа принадлежит X,
- каждая объектная переменная принадлежит X,
- для каждой функциональной константы h арности n (n > 0) и любой строки t1, ... , tn, если t1, ... , tn принадлежит X, тогда также принадлежит h(t1, ... , tn).
Строка является термом, если она принадлежит все множествам, которые замкнуты относительно правил построения.*
3.23Каждый терм содержит объектную константу или объектную переменную. Верно или нет ?
В логике первого порядка существуют три типа атомарных формул:
- пропозициональные константы,
- строки вида R(t1, ... , tn) где R – предикатная константа арности n (n > 0) и t1, ..., tn – термы,
- строки вида (t1 = t2), где t1, t2 – термы.
Взяв в качестве множества атомарных формул данное множество, мы получаем, что определение формул (первого порядка) совпадает с определением предикатных формул в начале этой части.
Для любых термов t1 и t2, t1 № t2 обозначает формулу (t1 = t2).
Функциональные символы и равенство: семантика
Выводы в логике первого порядка
Определение вывода в логике предикатов с функциональными константами и равенством включает новый тип аксиом и два новых правила вывода. Правила, как и раньше, содержат метапеременные, служащие для обозначения формул и термов.
|
|
Новые аксиомы выражают рефлексивность равенства и имеют вид Ж |– t = t , где t – произвольный терм. Новые правила вывода – правила замены:
|
|
где t1 и t2 свободные для v в F(v).*
Для каждой из следующих формул найдите вывод из пустого множества посылок.
3.27x = y Й f(x, y) = f(y, x).
см. Решение
3.28" x $ y (y = f(x)).
3.29$ y (x = y & y = z) Й x = z.
3.30$ x (x = a & P (x)) є P (a).
Теории первого порядка
Теория первого порядка сигнатуры s определяется с помощью аксиом. Интерпретация, при которой истинны все аксиомы теории первого порядка G, называется моделью G. Если теория первого порядка G выполнима, мы также говорим что она непротиворечива. Логические следствия теории первого порядка называется её теоремами. Доказательство предложения F в теории первого порядка G есть вывод F из подмножества аксиом из G.
Теоремы корректности и полноты выполняются для логик предикатов с функциональными символами и равенством и могут быть сформулированы в рамках теорий первого порядка следующим образом. В соответствие с теоремой корректности, если существует доказательство предложения F в теории первого порядка G, тогда F является теоремой G. В соответствие с теоремой полноты Гёделя, обратное также верно: для любой теоремы F теории первого порядка G, существует доказательство F в G.
|
|
Однако, добавление правил вывода для кванторов второго порядка ведёт к формальной системе которая корректна, но не полна.
Дата добавления: 2018-02-28; просмотров: 508; Мы поможем в написании вашей работы! |
Мы поможем в написании ваших работ!