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



Скачать 85.99 Kb.
Дата15.01.2013
Размер85.99 Kb.
ТипДокументы
Исчисление предикатов с равенством

  1. Алфавит

    1. — предметные переменные,

    2. — предметные константы,

    3. — предикатные символы,

    4. — функциональные символы,

    5. — логические связки,

    6. — символы кванторов,

    7. — вспомогательные символы.

  2. Выражения

    1. Термами называются:

      1. любая предметная переменная или предметная константа,

      2. если — термы, и — некоторый функциональный символ, то — тоже терм.

      3. других нет.

    2. Формулами являются (элементарные (атомарные) — первая два вида):

      1. если — предикатная буква, а — термы, то — формула,

      2. если и — термы, то — формула,

      3. если и формулы, то — тоже формулы.


Совокупность I и II — язык ИПР.
Замечание. В формулах подформула называется областью действия квантора соответственно.
Определение.
Вхождение x в формулу A называется связным, если оно находится в области действия какого-либо квантора или . В противном случае — свободным вхождением.

Определение. Терм t называется свободным для x в формуле A, если никакое свободное вхождение x в формулу A не находится в области действия никакого квантора или , где y входит в терм t.
Пример (спорный пример, предлагаю не использовать)


Теорема 26. Верно:

  1. Терм, не содержащий переменных, свободен для любой переменной в любой формуле.

  2. Терм x свободен для x в любой формуле.

  3. Если формула A не содержит свободных вхождений x, то любой терм свободен для x в данной формуле1.


Определение. Обозначим и назовем «сигнатурой».
Пусть A — предметная область (то, откуда берутся значения для переменных?), тогда пара называется алгебраической системой.
Примеры


Пусть t — терм сигнатуры и . Пусть — алгебраическая система сигнатуры .
Определение. Значение терма при определим по индукции:

  1. если , то ,

  2. если и , то .


Пример

при


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

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

2) если — предикатный символ из , и термы , то ,

3) ,

4) ,

5) ,

6) ,

7) ,

8) .
Определение. Формула A сигнатуры называется выполнимой, если существует такая алгебраическая система , что A истинна при некоторых значениях свободных переменных.
Определение. Формула A тождественно истинна, если она в любой алгебраической системе той же сигнатуры истинна при любых значениях свободных переменных.
Определение. Говорят, что формула семантически следует из множества формул Г, если для любой алгебраической системы из истинности всех формул Г при некотором значении свободных переменных всех формул из Г следует истинность формулы A при тех же значениях свободных переменных из A (обозначение: ).
Определение. Если и , то говорят, что A равносильно B (обозначение: ).
Теорема 27. .
Теорема 28. Верно:

1) .

А также, если B не содержит свободных вхождений x, то верно:


Теорема 29. Верно:

1) ,

2) .
Теорема 30. Пусть y не входит в A(x). A(y) получается из A(x) заменой всех свободных вхождений x на y. Тогда:


Теорема 31. Верно:


Теорема 32 «О замене».

Пусть A — формула, B — подформула в ней, — результат замены некоторого вхождения B в формуле A на , тогда, если , то .
Определение. Формула вида , где , а кванторов не содержит, а , называется предваренной нормальной формой (ПНФ).
Теорема 33. Всякая формула ИПР равносильна некоторой ПНФ.
Формальное исчисление предикатов с равенством

  1. Алфавит

    1. — предметные переменные,

    2. — предметные константы,

    3. — функциональные символы,

    4. — предикатные символы,

    1. — логические символы,

    2. — вспомогательные символы.

  1. Выражения

    1. Термами являются:

      1. любая предметная переменная или константа,

      2. если — термы, то и — тоже термы,

      3. других нет.

    2. Формулами являются:

      1. , где — термы,

, где и — термы

(два вида из этого пункта — атомарные (атомные) формулы),

      1. если A и B — формулы, то — тоже формулы,

      2. других нет.

  1. Аксиомы2





























A — формула, содержащая x свободно.

t — терм, свободный для x в A.

— результат замены свободного вхождения x в формуле A на терм t.

  1. Правила вывода

    1. (modus ponens),

    2. (B не содержит x свободно),

    3. .


Определение. Подстановка терма t вместо свободного вхождения x в формулу A называется допустимой, если в результате ни одна переменная терма t не окажется связной. (Это определение эквивалентно определению терма t свободного для x в A.)
Определение. Выводом из множества гипотез Г называют упорядоченную последовательность формул, каждая из которых является либо аксиомой, либо гипотезой из Г, либо получена из предыдущих по одному из правил или (возможно, что ).
Определение. Формула A называется выводимой из множества гипотез Г, если существует вывод , где (обозначение: ). Если , то A называется просто выводимой (обозначение: ).
Определение. Правило называется допустимым в ИПР, если из того, что формулы выводимы (при любых подстановках?) в ИПР следует, что и B — выводимая в ИПР.
Теорема 34. Пусть B не имеет свободных вхождений x, терм t свободен для x в A. Тогда правила

  1. — правило обобщения,

  2. ,



являются допустимыми в ИПР.
Определение. Формула , полученная из тавтологии подстановкой произвольных формул ИПР вместо пропозициональных переменных соответственно, называется тавтологией ИПР.
Теорема 35. Любая тавтология ИПР выводима в ИПР. Другое определение3.
Определение. Рассмотрим совокупность формул Г, A и — вывод формулы B из этой совокупности. Говорят, что из (*) зависит от формулы A в этом выводе, если:

  1. ,

  2. получено из предыдущих формул, которые зависят от A.



Теорема 36 «О дедукции».

Пусть из и существует такой вывод формулы B, в котором ни при каком применении правила связывания квантором () к формулам, зависящим в этом выводе от A, не связывается квантором никакая переменная, входящая в A, тогда .
Определение. Формулы ИПР A и B называются эквивалентными, если и (обозначение: ).
Теорема 37. Верно:

  1. ,

  2. .


Замечание (как лемма). .
Теорема 38. Пусть формула B не содержит свободных вхождений x. Тогда:

(y нет в )

(y нет в )


Теорема 39. Бинарное отношение на множестве всех формул ИПР есть конгруэнция, то есть:

  1. для любого A (рефлексивность),

  2. (транзитивность),

  3. (симметричность),

  4. , где .

  5. и , где .


Теорема 40 «О замене». Пусть , и — формула, содержащая подформулу A, — результат замены A на B. Тогда .
Теорема 41. Для любой формулы ИПР существует эквивалентная ей предваренная нормальная форма (ПНФ).
Определение. Множество формул X называется противоречивым, если в этом множестве найдутся формулы такие, что из них выводится: для некоторой формулы A. В противном случае X называют непротиворечивым множеством формул.
Теорема 42. Если , то , где — любая.
Замечание (к теореме 42) (переформулировка и обозначение). .
Определение4. Множество X формул ИПР называется несовместным (противоречивым), если такие, что для некоторой формулы A. В противном случае X называется непротиворечивым (совместным).
Теорема 43. Свойства непротиворечивых множеств формул

  1. Верно:

    1. — непротиворечивое,

    2. ИПР — тоже непротиворечивое множество.

  2. Если X — непротиворечивое, , и , тогда — непротиворечивое (другими словами: если X — непротиворечивое, то оно замкнуто по выводимости).

  3. Если — непротиворечивое, и , то есть y не принадлежит к множеству всех свободных переменных множества формул , то — непротиворечивое.

  4. Если — возрастающая последовательность непротиворечивых множеств формул, то — тоже непротиворечивое.

  5. Если — произвольная формула ИПР, и X — непротиворечивое множество формул, то либо , либо непротиворечивое.


Определение5. Множество формул X называется непротиворечивым, если в этом множестве найдутся такие, что для любой формулы A.
Теорема 44 «О существовании модели». Любое непротиворечивое множество формул X имеет модель (). Если бесконечное множество формул X непротиворечиво, то X имеет модель мощности не более, чем мощность множества X ().
Определение. Формулы, не имеющие свободных переменных, называются предложениями.
Теорема 45 (Гёделя). Любая тождественно истинная формула ИПР доказуема.
Теорема Мальцева. Множество предложений S имеет модель тогда и только тогда, когда каждое конечное подмножество имеет модель.
Теорема Танненбаума. Существует нестандартная модель арифметики.
Теорема. Существует нестандартная модель анализа.

1 Здесь было «в любой формуле». Мне кажется, что должно быть «в данной формуле».

2 Именно эти аксиомы можно не учить.

3 для тавтологий ИПР.

4 Обратите внимание, что я выписывал определения из лекций так, как они шли. На самом деле это определение уже давалось, причем на предыдущей лекции, здесь оно находится выше на этой же странице.

5 И третий раз это же определение, но идет как «обратное».




Похожие:

Исчисление предикатов с равенством iconЛекция Какие семантики бывают. Исчисление предикатов как прототипический пример формального языка Владимир Борщев, винити ран
Лекция Какие семантики бывают. Исчисление предикатов как прототипический пример формального языка
Исчисление предикатов с равенством iconНормальные формы формул логики предикатов
При этом, используя равносильности алгебры высказываний и логики предикатов, каждую формулу логики предикатов можно привести к нормальной...
Исчисление предикатов с равенством iconИсчисление предикатов. Пропозициональная функция
Р(Х­1,Х2,…,Хn) есть атомарная (элементарная) формула. Эта формула трактуется как высказывание, гласящее, что объекты Х1,Х2,,…,Хn...
Исчисление предикатов с равенством iconС. 38. Модель согласования выводов из теорий, используемых для объяснения особых состояний сознания (осс)
Предлагается использовать алгебраические модели конструктивной логики (амкл), отображающие интуиционистское исчисление предикатов...
Исчисление предикатов с равенством iconЛабораторная работа №1 по дисциплине "Системы искусственного интелекта"
Исчисление предикатов первого порядка является теоретической основной множества формализмов методов искусственного интеллекта. Задачи...
Исчисление предикатов с равенством iconЯзык Пролог Пролог (Prolog)
Пролог декларативный язык, который основывается на исчисление предикатов и при работе с которым необходимо описать ситуацию (правила...
Исчисление предикатов с равенством iconЛекция 3 Логика предикатов Понятие предиката
Такой логической системой является логика предикатов, содержащая всю логику высказываний в качестве своей части
Исчисление предикатов с равенством iconИспользование реляторов для описания движений в рукопашном бое
А значит являются предложениями, которые состоят из термов, предикатов и аргументов предикатов. Каждый из членов предложения выступает...
Исчисление предикатов с равенством iconЛабораторная работа №1 По предмету: «Искусственный интеллект.» "Знакомство с Prolog".
Пролог (англ. Prolog) — язык и система логического программирования, основанные на языке предикатов математической логики дизъюнктов...
Исчисление предикатов с равенством iconЛогические операции над предикатами
Рассмотрим применение операций логики высказываний к предикатам на примерах одноместных предикатов. Эти операции в логике предикатов...
Разместите кнопку на своём сайте:
ru.convdocs.org


База данных защищена авторским правом ©ru.convdocs.org 2016
обратиться к администрации
ru.convdocs.org