Корректность и полнота логики высказываний
Теорема корректности.Если существует вывод F из G, тогда G логически влечёт F.
Теорема полноты.Для любой формулы F и любого множества формул G, если G влечёт F, тогда существует вывод F из подмножества G.
Полнота логики высказываний (для другого множества правил вывода) была установлена Емилем Постом в 1921 году.
Логика предикатов
Понятие ``предикат'' обобщает понятие ``высказывание''. Неформально говоря, предикат – это высказывание, в которое можно подставлять аргументы. Если аргумент один – то предикат выражает свойство аргумента, если больше – то отношение между аргументами.
Пример предикатов. Возьмём высказывания: ``Сократ - человек'', ``Платон - человек''. Оба эти высказывания выражают свойство ``быть человеком''. Таким образом, мы можем рассматривать предикат ``быть человеком'' и говорить, что он выполняется для Сократа и Платона.
Возьмём высказывание: ``расстояние от Иркутска до Москвы 5 тысяч километров''. Вместо него мы можем записать предикат ``расстояние'' (означающий, что первый и второй аргумент этого предиката находятся на расстоянии, равном третьему аргументу) для аргументов ``Иркутск'', ``Москва'' и ``5 тысяч километров''.
Язык логики высказываний не вполне подходит для выражения логических рассуждений, проводимых людьми, более удобен для этого язык логики предикатов.
Пример рассуждения, не выразимого в логике высказываний. Все люди смертны. Сократ - человек. Следовательно, Сократ смертен.
|
|
Это рассуждение на языке логики высказываний можно записать тремя отдельными высказываниями. Однако никакой связи между ними установить не удастся. На языке логики предикатов эти предложения можно выразить с помощью двух предикатов: ``быть человеком'' и ``быть смертным''. Первое предложение устанавливает связь между этими предикатами.
Перейдём теперь к формальному изложению логики предикатов.
Язык логики предикатов
``Предикатные формулы'' обобщают понятие пропозициональной формулы, определённое в части 2.
Предикатная сигнатура – это множество символов двух типов – объектные константы и предикатные константы – с неотрицательным целым числом, называемым арностью, назначенным каждой предикатной константе. Предикатную константу мы будем называть пропозициональной, если её арность равна 0. Пропозициональные константы являются аналогом атомов в логике высказываний. Предикатная константа унарна, если её арность равна 1, и бинарна, если её арность равна 2. Например, мы можем определить предикатную сигнатуру
{ a, P, Q } | (4) |
объявляя a объектной константой, P – унарной предикатной константой, и Q – бинарной предикатной константой.
|
|
Возьмём предикатную сигнатуру s, которая включает по крайней мере одну предикатную константу и не включает ни одного из следующих символов:
- объектные переменные x, y, z, x1, y1, z1, x2, y2, z2, ...,
- пропозициональные связки,
- квантор всеобщности " и квантор существования $,
- скобки и запятая.
Алфавит логики предикатов состоит из элементов из s и четырёх групп дополнительных символов, указанных выше. Строка – это конечная последовательность символов из этого алфавита.
Терм – это объектная константа или объектная переменная. Строка называется атомарной формулой, если она является пропозициональной константой или имеет вид R(t1, ..., tn), где R – предикатная константа арности n (n > 0) и t1, ... , tn – термы. Например, если мы рассматриваем сигнатуру (4), то P(a) и Q(a, x) – атомарные формулы.
Множество X строк замкнуто относительно правил построения (для логики предикатов), если
- каждая атомарная формула принадлежит X,
- для любой строки F если F принадлежит X, то F тоже принадлежит,
- для любых строк F, G и любой бинарной связки Д, если F и G принадлежат X, то также принадлежит (F Д G),
- для любого квантора K, любой переменной v и любой строки F если F принадлежит X, то также принадлежит Kv F.
Строка F является (предикатной) формулой, если F принадлежит всем множествам, которые замкнуты относительно правил построения.
|
|
Например, если рассматриваемая сигнатура есть (4), тогда
(P (a) Ъ $ x(P (x) & Q(x, y)))
– формула.
3.1Является ли " x формулой?
Как и в логике высказываний можно доказать, что множество формул замкнуто относительно правил построения. Теоремы возможности и единственности разбора подобны соответствующим теоремам для пропозициональных формул.
В случае предикатных формул доказательство по структурной индукции имеет следующий вид. Для данного свойства формул мы проверяем, что
- каждая атомарная формула обладает этим свойством,
- для любой формулы F, обладающей этим свойством, F также обладает этим свойством,
- для любых формул F, G, обладающих этим свойством, и любой бинарной связки Д, (F Д G) также обладает этим свойством,
- для любого квантора K, любой переменной v и любой формулы F, обладающей этим свойством, Kv F также обладает этим свойством.
Тогда это свойство выполняется для всех формул.
3.2Если формула содержит квантор, тогда она содержит переменную. Верно или нет ?
3.3Если формула содержит квантор, тогда она содержит скобки. Верно или нет ?
При записи предикатных формул мы будем опускать некоторые скобки и применять другие сокращения, введённые в части 2. Строку вида
|
|
" v1 ··· " vn (n і 0)
будем писать как " v1 ··· vn, и подобным образом для квантора существования.
Дата добавления: 2018-02-28; просмотров: 820; Мы поможем в написании вашей работы! |
Мы поможем в написании ваших работ!