Формальные системы.Исчисление предикатов

Автор работы: Пользователь скрыл имя, 02 Декабря 2013 в 14:54, реферат

Краткое описание

Формальные системы — это системы операций над объектами, понимаемыми как последовательности символов (т. е. как слова в фиксированных алфавитах); сами операции также являются операциями над символами. Термин «формальный» подчеркивает, что объекты и операции над ними рассматриваются чисто формально, без каких бы то ни было содержательных интерпретаций символов.

Вложенные файлы: 1 файл

реферат по дискретной математике.docx

— 88.09 Кб (Скачать файл)

- логические символы (пропозициональные  связки):

- Ø – отрицание;

- Ù – логическое И (конъюнкция, логическое умножение);

- Ú – логическое ИЛИ (дизъюнкция, логическое сложение);

- ® (Þ) – импликация (если - то);

- « (º) – эквивалентность;

- кванторы переменных:

- $ – квантор существования;

- " – квантор всеобщности;

- вспомогательные символы:  круглые скобки, запятые, +, - и т.п.

 

5. Кванторы

 

5.1. Историческая справка

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

Хотя кванторно-логические конструкции широко используются как в научной, так и в обыденной речи, их формализация произошла только в 1879 г., в книге Фреге «Исчисление понятий». Обозначения Фреге имели вид громоздких графических конструкций и не были приняты. Впоследствии было предложено множество более удачных символов, но общепринятыми стали обозначения   для квантора существования (перевёрнутая первая буква англ. Exists — существует), предложенное Чарльзом Пирсом в 1885 г., и   для квантора общности, образованное Герхардом Генценом в 1935 г. по аналогии с символом квантора существования. Термины «квантор», «квантификация» также предложил Пирс.

Квантор — общее название для логических операций, ограничивающих область истинности какого-либо предиката и создающих высказывание. Чаще всего упоминают:

  • Квантор всеобщности (обозначение:  , читается: «для всех…», «для каждого…» или «каждый…», «любой…», «для любого…»).
  • Квантор существования (обозначение:  , читается: «существует…» или «найдётся…»).

В математической логике приписывание квантора к формуле называется связыванием или квантификацией.

 

5.2. Примеры использования кванторов.

Обозначим   предикат «x делится на 5». Используя квантор общности, можно формально записать следующие высказывания (конечно, ложные):

  1. любое натуральное число кратно 5;
  2. каждое натуральное число кратно 5;
  3. все натуральные числа кратны 5;

следующим образом:

.

Следующие (уже истинные) высказывания используют квантор существования:

    1. существуют натуральные числа, кратные 5;
    2. найдётся натуральное число, кратное 5;
    3. хотя бы одно натуральное число кратно 5.

Их формальная запись:

.

Кванторы в математической логике:

  • Высказывание   означает, что область значений переменной   включена в область истинности предиката  .

(«При всех значениях   утверждение верно»).

  • Высказывание   означает, что область истинности предиката   не пуста.

(«Существует   при котором утверждение верно»).

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

5.3. Операции над кванторами

Правило отрицания кванторов — применяется для построения отрицаний высказываний, содержащих кванторы, и имеет вид:

 

6. Семантика логики предикатов первого порядка.

 

Терм - переменная, константа или функция (т.е. объект или его свойство).

Предикат (атомарная формула, атомарное предложение, атом) - отношение, устанавливающее связь между термами (параметрами). Предикат (в математической логике «атом») - простейший случай формулы, т.е. формула, которую нельзя расчленить на подформулы. Например, друзья(отец(андрей), коля) – отец Андрея и Коля являются друзьями. В этом предикате: друзья - предикатный символ, отец(андрей) – функция, коля – константа. Если параметр отец(андрей) был бы не функцией, а предикатом, то предикат друзья был бы предикатом второго порядка.

Количество термов в предикате  называется арностью предиката.

Предикат с арностью, равной 0, обозначает событие, признак или  свойство, относящееся ко всей предметной области, например, end.

Предикат с арностью, равной 1, обозначает свойство сущности, например, дом(кирпичный).

Формула (предложение, правило, правильно построенная  формула) - это либо предикат (атом), либо одна из следующих конструкций: ØА, AÙB, AÚB, A®B, A«B, ("X) A и ($X) А, где A и B - формулы, а X - переменная. Результатом вычисления формулы является либо истина либо ложь.

Примеры формул:

мать(маша, X) Ù мать(маша, Y) ® брат(X, Y) Ú сестра(X, Y) – если Маша мать X и Y, то X является братом или сестрой Y.

человек(X) ® смертен(Х) – если X – человек, то он смертен.

Приоритет операций и кванторов  при исчислении формул показан ниже

В скобках показаны операции (кванторы) с одинаковым приоритетом. Если в формуле используются операции (кванторы) с одинаковым приоритетом, то порядок исчисления слева-направо. Изменение порядка исчисления можно  добиться за счет использования круглых  скобок «( )».

Квантор существования $ указывает, что предложение истинно, по крайней мере, для одного значения переменной. Например, $X друзья(X, петя) – существует, по крайней мере, один субъект X, который является другом Пети.

Квантор всеобщности " указывает, что предложение истинно, для всех значений переменной. Например, "X человек(X) ® смертен(Х) – все люди смертны.

При комбинации кванторов  очень важен порядок их использования, например:

- "X$Y любит(Х, Y) – любой Х любит хотя бы одного Y;

- "Y$X любит(Х, Y) – каждого Y любит хотя бы один Х;

- $X"Y любит(Х, Y) – существует такой Х, который любит всех;

- $Y"X любит(Х, Y) – существует такой Y, которого любят все;

- "X"Y любит(Х, Y) и "Y"Х любит(Х, Y) – все любят всех;

- $X$Y любит(Х, Y) – существует такой X, который любит хотя бы одного из Y;

- $Y$Х любит(Х, Y) – существует такой Y, которого любит хотя бы один X. 

 

7. Исчисление предикатов

 

 

 Исчисление предикатов первого  порядка представляет собой исчисление высказываний, дополненное аксиомами , связанными с кванторами и дополнительными правилами вывода.

1. Алфавит исчисления предикатов состоит из предметных переменных х1 , х2, ..., предметных констант а1, а2, ..., предикатных букв P11, Р21, ..., Рjk... и функциональных букв f11, f21,..., fjk, ..., а также знаков логических связок Ú, Ù,¬,→, кванторов , и скобок (,).

Верхние индексы предикатных  и функциональных букв указывают  число аргументов, их нижние индексы  служат для обычной нумерации  букв. Переменные высказывания в исчисление предикатов вводятся либо непосредственно как пропозициональные буквы А1, А2, ..., либо как 0-местные предикаты P10, Р20, ..., т. е. как предикаты без предметных переменных.

2. Формулы. Понятие формулы определяется в два этапа.

  1. Термы:

а) предметные переменные и  константы являются термами;

б) если fn — функциональная буква, a t1,…, tn — термы, то fn(t1,…, tn) — терм.

 2)Формулы:

а) если Рп — предикатная буква, a t1,…, tn — термы, то Рп(t1,…, tn) — формула; все вхождения предметных переменных в формулу вида Рп(t1,…, tn)называются свободными;

б) если F1 ,F2 — формулы, то формулами являются ¬F, (F1→ F2),   

  (F1 Ú F2) ,(F1 Ù F2); все вхождения переменных, свободные в F1 ,F2, являются свободными и в указанных четырех видах формул;

в) если F(x) — формула, содержащая свободные вхождения переменной х, .то "xF(x) и $xF(x) — формулы; в этих формулах все вхождения переменной х называются связанными; свободные вхождения остальных переменных в F остаются свободными.

         3. Аксиомы исчисления предикатов делятся на две группы :

1) аксиомы исчисления высказываний (можно взять любую из систем I или II ).

Первая из них непосредственно использует все логические связки:

Система аксиом I:

I 1. A → (B → A);

I 2. (A → B) → ((A → (B → C)) → (A → C));

I 3. (A Ù B) → A;

I 4. (A Ù B) → B;

I 5. A → (B → ( A Ù B));

I 6. A → (A Ú B));

I 7. B → (A Ú B));

I 8. (A → C) → ((B → C) → (( A Ú B) → C));

I 9. (A → B) → ((A → ¬B) → ¬A);

I 10. ¬ ¬A → A

    Другая система использует только две связки ¬ и →; при этом сокращается алфавит исчисления (выбрасываются знаки Ù , Ú) и , соответственно, определение формулы. Операции Ù , Ú рассматриваются не как связки исчисления высказываний, а как сокращения (употреблять которые удобно, но не обязательно) для некоторых его формул: A Ú B заменяет ¬А → В, A Ù B заменяет ¬(A → ¬B). В результате система аксиом становится намного компактнее.

Система аксиом II :

II 1. A → (B → A);

II 2. (A → (B → C)) → ((A → B) → (A → C));

II 3. (¬A → ¬B) → ((¬A → B) → A).

Приведенные системы аксиом равносильны в том смысле, что порождают одно и то же множество формул.

 

2) две предикатные аксиомы:

P1. "xF(x) → F(y);

Р2. F(y) → $xF(x).

В этих аксиомах F(x) — любая формула, содержащая свободные вхождения х, причем ни одно из них не находится в области действия квантора по у; формула F(y) получена из F(x) заменой всех свободных вхождений I на у.

Чтобы пояснить существенность требования к вхождениям х в F, рассмотрим в качестве F(x) формулу $уР(у,х), где это требование нарушено: свободное вхождение х находится в области действия $у. Подстановка этой формулы в аксиому Р1 дает формулу "х$уР(у, х) → $уР(у, у). Если ее проинтерпретировать на множестве N натуральных чисел с предикатом Р «быть больше», то получим высказывание: «если для всякого х найдется у, больший x то найдется у, больший самого себя». Посылка этой импликации истинна на N, а ее заключение ложно, и, следовательно, само высказывание ложно.

 

4. Правила вывода:

Правила вывода позволяют из данной системы аксиом получать другие истинные формулы исчисления высказываний. Назовем формулу исчисления высказываний ложной, если ее отрицание истинно. Будем обозначать истинные формулы буквой R, ложные - F.

К основным правилам вывода относятся два:

1) Правило заключения (Modus Ponens)

Если A  и (A → B) – выводимые формулы, то B также выводима. Это предложение можно записать в виде

A,A→B

B

             2) Правило подстановки

Пусть некоторая формула A  содержит переменное высказывание А. Тогда, заменив высказывание А всюду, где оно встречается, любой формулой B , получим истинную формулу. Это предложение записывается в виде

A (А)

A (B)

Формула называется выводимой  в исчислении высказываний, если ее можно получить, применяя правила  вывода к аксиомам исчисления высказываний. Утверждение, что формула B выводима, записывают так:

 

├ B

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

В исчислении предикатов первого  порядка (узком исчислении предикатов) два правила вывода (подстановки  и заключения) исчисления высказываний дополняют еще тремя правилами:

  1. правило для (если φ1 → φ2 выводима и в φ1 нет х в качестве свободной переменной, а в φ2 переменная х содержится в виде свободной переменной, то формула φ1 → (x)φ2 также выводима);
  2. правило для (если φ1 → φ2 выводима и х содержится в качестве свободной переменной в φ1 и не содержится в виде свободной переменной в φ2, то формула (x)φ1 → φ2 также выводима);
  3. правило переименования связанных переменных (если φ1 — выводимая формула и в φ1 имеется квантор всеобщности или квантор существования, то одна связанная переменная в φ1 может быть заменена другой связанной переменной одновременно во всех областях действия квантора и в самом кванторе. Полученная формула также выводима).

 

 

 

Заключение

 

Формальная система представляет собой совокупность чисто абстрактных объектов (не связанных с внешним миром), в которой представлены правила оперирования множеством символов в чисто синтаксической трактовке без учета смыслового содержания (или семантики).

Информация о работе Формальные системы.Исчисление предикатов