Дополнительные законы
1)
1’)
2)
x
P(x) =
2’)
x
P(x) =
3) x A(x) Λ x B(x) = x (A(x) Λ B(x))
4) C Λ x B(x) = x (C Λ B(x))
5) C v x B(x) = x (C v B(x))
6) C -> x B(x) = x(C -> B(x))
7) x (B(x) -> C) = x B(x) -> C
8) x A(x) v x B(x) = x (A(x) v B(x))
9) x (C v B(x)) = C v x B(x)
10) x (C Λ B(x)) = C Λ x B(x)
11) x A(x) Λ y B(y) = x y (A(x) Λ B(y))
12) x (C -> B(x)) = C -> x B(x)
13) x (B(x) -> C) = x B(x) -> C
14) x y B(x, y) = y x B(x, y)
15) x y B(x, y) = y x B(x, y)
Формула ЛП имеет нормальную форму, если она содержит только операции Λ, V и кванторные операции, а ˥ отнесена к элементарным формулам.
В предваренной нормальной форме кванторные операции либо полностью отсутствуют, либо используется после всех операций АЛ.
Теорема.
Всякая формула ЛП может быть приведена к ПНФ.
Формула A ЛП называется выполнимой в области M, если существуют значения переменных, входящих в эту формулу и отнесенных к множеству M, при которых A принимает истинные значения.
Формула A называется выполнимой, если существует область, на которой эта формула выполнима. Если она выполнима, то это не означает, что она выполнима на любой области.
Формула A называется ТИ в области M, если она пинимает истинные значения для всех переменнх, входящих в эту формулу и отнесенных к этой области.
Формула A называется общезначимой, если она ТИ на всякой области.
Формула A называется ТЛ в области M, если она принимает ложные значения для всех значений переменных, входящих в эту формулу и отнесенных к этой области.
Из приведенных опеределений следует:
1) Если формула А общезначима, то она и выполнима на всякой области;
2) Если формула А ТИ в области М, то она и выполнима в этой области;
3) Если формула А ТЛ в области М, то она не выполнима в этой области;
4) Если формула А не выполнима, тоо она ТЛ на всякой области.
Общезначимую формулу называют логический законом.
Теорема 1.
Для того, чтобы формула А была общезначима, необходимо и достаточно, чтобы ее отрицание было невыполнимо.
Теорема 2.
Для того, чтобы формула А была выполнима, необходимо и достаточно, чтобы формула ˥A была необщезначима.
Проблема разрешимости для общезначимости и выполнимости. Неразешимость ее в общем случае.
В 1936 году американский математик Черч доказал, что проблема разрешимости ЛП в общем виде неразрешима, т. е. не сущестует алгоритма, который позволил бы установить, к какому классу формул относится любая формула ЛП. Для конечной области проблема разрешима.
Аксиоматическая теория – это совокпность всех теорем, доказываемых исходя из данной системы аксиом. Аксиоматические теории делятся на формальные и неформальные.
Неформальные АТ – теории, наполненне теоретико-множественным содержанием, понятие выводимости в них довольно расплывчато и в значительной степени опирается на здравый смысл.
Формальная АТ считается определенной, если выполняются следующие условия:
1) задан язык теории с некоторым не более чем счетным числом символов, называемое алфавитом теории; конечная последовательность символов алфавита называется выражениями;
2) определено понятие формулы в этой теории – это подмножество множества выражений;
3) определено некоторое число формул, называемые аксиомами;
4) определены правила вывода в этой теории, т. е. некоторое множество отношений между формулами.
Теории 1-ого порядка (Т) отлиаются от теории высших порядков тем, что не допускают в своем изложениии предикаты, которые имеют в качестве возможных значений своих аргументов другие предикаты и функции. Кроме того, они не допускают квантовые операции по предикатам и фунциям. Теории 1-ого порядка достаточно для выражения большого количества известных математических теорий. Такие математические теории иногда называют элементарными теориями. Аксиомы теории 1-ого порядка забиваются на два класса: логические аксиомы и специальные.
Логические аксиомы
1) A -> (B -> A)
2) (A -> (B -> C)) =>( (A -> B) -> (A -> C))
3) (˥B -> ˥A) => ((˥B -> A) -> B)
4) xi A(xi) -> A(t), где A(xi), где A(xi)- формула теории Т, t – предметная переменная или предметная константа, t может совпадать с x.
5) xi (A -> B) -> (A -> xi B), если xi не входит свободно в формулу А.
Правила вывода:
1) правило заключения или Модус Понес
| = A, |= A -> B (посылки)
--------------------
|= B (заключение)
2) правило связывания квантором всеобщности или правило обобщения.
|= A
-----------------------
|= xi A
Доказательством или выводом называют конечную последовательность S1, S2, …, Sn высказываний рассматриваемой теории, каждая из которых является либо аксиомой, либо выводится из одного или более предыдущих высказываний по логическим правилам теории.
Теоремой или докзанным высказыванием называется высказывание, являющееся последним высказыванием некоторого доказательства.
Формула А называется следствием множества формул ɣ т. и т. т., когда существует такая последовательность формул A1, A2, …, An, что An совпадает с А и все Ai есть либо аксиомы теории Т, либо формула из множества ɣ(ГА), либо непосредств. следствие из некоторой предыдущей формулы. Эта последовательность называется выводом формулы А из множества гипотез ɣ(ГА) и Г |= A