ЛМвИИ (1086253), страница 9
Текст из файла (страница 9)
Роль функции Vсостоит в том, чтобы интерпретировать функциональные и предикатные константы языка втерминах элементов S.Пусть {t} - список всех свободных переменных, входящих в терм t, a g - функция,приписывающая всякой индивидной переменной из t значение из S. Индуктивнымопределением введем понятие терма t в модели М при присваивании g, обозначив это понятиеU(t, g). Функция g соответствует функции Iv интерпретации I. Функция g не является частьюмодели М.Семантика формул языка логики предикатов первого порядка описывается с помощьюобозначенияM╞g A,которая означает "А истинна в модели М для назначения g".Тогда для любой формулы А имеем эквивалентные обозначения:M╞g AU(A, g)=1,I(A)=1U(A, g)=1.Теперь мы можем сделать следующие определения:• Если терм t есть константа ai , то U(t, g)=I(ai ), т.е.
индивидной константесопоставляется элемент множества S: I(ai )S.• Если терм t есть переменная xi , то в данной модели U(t, g)=g(x).• Если f - n-местная функциональная константа и t1, …, tn -термы, то U(f(t1, …, tn)) =V(f)(U(t1, g), …, U(tn , g) )).• Если P n-местная предикатная константа и t1, …, tn – термы, то U(f(t1, …, tn)) =• V(f)(U(t1, g), …, U(tn , g) )).В описанной семантике можно дать определение понятия выполнимости.M╞g P(t1, …, tn) тогда и только тогда, когда значение истинности V(P(t1, …, tn)) есть Ипри данной функции приписывания g.• M╞g ¬A тогда и только тогда, когда М |≠g А.• M╞g А^В тогда и только тогда, когда M╞g А и M╞g В.• Аналогично для формул AvB, А→В и А↔В.• М╞g ∀хА тогда и только тогда, когда М╞g А для всех присваиваний g, которыеотличаются от присваивания g только сопоставлением значения переменной х.Формула А общезначима тогда и только тогда, когда M╞g А для всех моделей М и всехприсваиваний g.Пример.
Рассмотрим формулу:∀x(P(x)→Q(f(x), a)).В этой формуле имеем: индивидную константу а, одноместную функциональнуюконстанту f, унарную предикатную константу Р (или просто предикат) и бинарный предикат Q.Задана следующая интерпретация I:S={1, 2};I(a): {1, 2}; примем а=1 для вcex x ∈S .Iv(a): {1, 2};I(f(х)) = Iс(f)(Iv(x)) = {2(1), 1(2)};I(P(х)) = Ic(Р)(Iv(х)) = {Л(1), И(2)};I(Q(f(x))) = Ic(Q)(Ic(f)(Iv(x)), I(a)) = {И(1(2), 1), И(1(2), 2), Л(2(1), 1), И(2(1), 2)}.При х=1P(x)→Q(f(x), a) = P(1)→Q(f(1), a) = P(1)→Q(2, 1) = Л→Л = И.При x=2P(x)→Q(f(x), a) = P(2)→Q(f(2), a) = P(2)→Q(1, 1) = И→И = И.Таким образом, для всех х из S формула P(x)→Q(f(x), a) истинна, следовательно, онаистинна в интерпретации I.Пример.
В интерпретации из предыдущего примера оценим выполнилось формулы:∃х(Р(f(х))^Q(х, f(a))).При x=1P(f(x))^Q(x, f(a)) = P(f(1))^Q(1, f(a)) = P(2)^Q(1, f(1)) = P(2)^Q(1, 2) = И^И = И.При х=2P(f(x))^Q(х, f(а)) = P(f(2))^Q(2, f(a)) = P(1)^Q(2, f(1)) = Р(1)^Q(2, 2) = Л^И = Л.Поскольку для x ∈S , т.е. х=1, формула P(f(x))^Q(x, f(a)) истинна, то формула∃х(Р(f(х))^Q(х, f(a))) истинна в интерпретации I.Правило вывода в логике предикатов определяется как правило логическогоследования.
Формула В логически следует из формул A1, A2, …, An (A1, A2, …, An├B) тогда итолько тогда, когда всякая интерпретация, удовлетворяющая A1^A2^…^An, удовлетворяет такжеи В, т.е. из истинности посылок A1, A2, …, An следует истинность заключения В. В соответствиис определением формальной дедуктивной системы, множество выводимых формул образованоформулами, которые логически следуют из аксиом или аксиом и ранее введенных формул.Следующие две теоремы позволяют определить справедливость логическогоследования A1, A2, …, An├B из общезначимости формулы A1^A2^…^An →B илипротиворечивости формулы A1^A2^…^An ^¬B.Теорема дедукции.
Формула В является логическим следствием A1, A2, …, An тогда итолько тогда, когда формула A1^A2^…^An →B общезначима.Доказательство. Необходимость. Пусть A1, A2, …, An├B, тогда A1^A2^…^An →Bобщезначима.Обозначим через I{i1, i2, …, iK , ...} множество интерпретаций упорядоченных такимобразом, что первые k позиций занимают интерпретации, в которых формула A1^A2^…^Anистинна, а затем перечислены интерпретации, в которых формула A1^A2^…^An ложна. Изопределения логического следования вытекает, что возможны два случая, представленных втабл.2.1 и 2.2.Таблица 2.1.Таблица 2.2.I A1^A2^…^An B A1^A2^…^An →BI A1^A2^…^An В A1^A2^…^An →Bi1ИИИi1И…Иi2ИИИi2И...И…...............……IKИИИIKИ…И...JIЛИ…И…И…ЛЛИ…И…И………………………ЛЛИ…Л…ИДостаточность.
Пусть A1^A2^…^An →B общезначима, тогда справедливо A1, A2, …,An├B.Таблица 2.3АBА→ВИИИИЛЛЛИИЛЛИИз таблицы истинности формулы А→В (табл.2.3) следует, что общезначимостьформулы A1^A2^…^An →B исключает существование интерпретаций, в которых A1^A2^…^Anистинна, а В - ложна. Следовательно, из истинности формулы A1^…^An следует истинность В,т.е.
A1, A2, …, An├B.Теорема противоречивости. Формула В является логическим следствием A1, A2, …, Anтогда и только тогда, когда формула A1^A2^…^An ^¬B противоречива.Из теоремы следует, что для доказательства выводимости формулы В из формул A1, A2,…, An достаточно доказать противоречивость формулы A1^A2^…^An ^¬B. Это утверждениележит в основе метода резолюции (опровержения). Для применения этого метода необходимопредставить формулы в стандартизованном виде, который представляет собой конъюнкциюдизъюнкций. Приведение формул к стандартной форме рассмотрены в последующих разделах.Пример. Пусть заданы формулы:F1: ∀x(P(x)→Q(x));F2: P(a).Показать, что Q(a) является логическим следствием F1 и F2.Пусть задана некоторая интерпретация I, в которой формула ∀x(P(x)→Q(x)) истинна.Будем считать, что в формуле F2 Р(а) истинна. Положим, что Q(a) ложна в принятойинтерпретации I, тогда импликация P(a)→Q(a)≡¬P(a)vQ(a) ложна.
Следовательно, ложна в I иформула ∀x(P(x)→Q(x)), а это невозможно в силу исходного предположения. Тогда следует,что Q(a) истинна в любой интерпретации, в которой формула ∀x(P(x)→Q(x))^Р(а) истинна.Следовательно, Q(a) является следствием F1 и F21.2.3.Приведем еще несколько примеров, иллюстрирующих рассмотренный материал.Общезначимые формулы:∀xP(x)→∀yP(y) - тавтология;∀xP(х)→∃уР(у) - при любой непустой области интерпретации из справедливости длявсех элементов следует справедливость для отдельных;P(a)v¬P(a) - тавтология;Невыполнимые формулы:∀хР(х)→¬∀уР(у) - противоречие;∀xP(x)→¬P(a) - из справедливости для всех следует несправедливость дня отдельногоэлемента, что также является противоречием.Выполнимые формулы:P(a)→¬∃xP(x) - формула истинна в интерпретациях, в которых Р(а) ложна.
Например,если Р(х) интерпретируется как " х - отличник" и в рассматриваемом множестве Dстудентов группы Иванов не является отличником, тогда формула Р(Иванов)→¬∃хР(х)- истинна;∀x(P(x)v¬Q(x)) - формула, истинная в интерпретациях, в которых для каждогоэлемента истинно Р или ложно Q;∃хР(х) - формула истинная в интерпретациях, в которых хотя бы для одного элементаистинно Р.Напомним, интерпретация называется моделью для данного множества формул, есливсе формулы рассматриваемого множества истинны (выполнимы) в даннойинтерпретации.4.a)Моделью для формул∀x^¬P(x, x),∀x, y, z(P(x, y)^Р(у, z)→P(x, z)), ∀x∃yP(x, y)является множество действительных чисел с заданным на нем отношением меньше,т.е.
Р(х, у) - «х меньше j».b) Моделью для формул∀х(O(х)^Р(х)→П(х)),∀x(¬O(x)v¬P(x)→¬П(x)),∃х¬П(x),где O(х) - "x учится отлично", Р(х) - « х занимается общественной работой » и П(х)- "x получает повышенную стипендию", могут служить реально существующиепринципы, используемые при назначении стипендии.c) в) Моделью для формулы∀ ∃ ∀ x R ∧P x ,Q f x , , является следующая интерпретация:S- множество действительных чисел;Р(х, α, δ): |x-α|<δ;Q(f(x), β, ε): |f(x)-β|<ε;R(ε): ε>0;f(х) - произвольная, фиксированная функция, заданная на отрезке [а, β]; х, δ, ε индивидные переменные из S; α, β - константы из S, ∈[ a , b ] . В такойинтерпретации приведенная формула соответствует утверждению о том, что числоβ является пределом функции f(х) при x→α.2.3.
Правила вывода в логике предикатов первогопорядка.В процессе решения задачи мы используем различные способы рассуждений, которыеприводят к поставленной цели. Мы можем декомпозировать задачу на подзадачи, каждая изкоторых имеет свое частичное решение, или вывод, и при этом этот частичный выводстановится основой для решения следующей подзадачи и т.д. В любом.случае началомрассуждений является гипотеза или совокупность гипотез, из которых на базе некоторых правил(законов) делается заключение. В самом начале мы уже отмечали, что заключения типа "потомучто" или "если...
то" являются примерами рассуждений. Интуитивно можно определить процессрешения задачи как вывод из гипотез и аксиом. И эта идея получила отражение в техрассуждениях, которые приведены в предыдущем параграфе и. в частности, в теореме дедукции.Теперь дадим более строгое определение вывода.Выводом из множества гипотез (посылок, допущений) назовется непустая конечнаяпоследовательность формул, в которой каждая формула есть одна из гипотез, или формула,полученная из предшествующих формул последовательности по одному из правил вывода, илитеорема; вывод последней формулы >той последовательности называется заключением изисходного множества гипотез.Доказательством выводимости называется непустая конечная последовательностьвыводимостей, в которой каждая выводимость или является непосредственно обоснованной,или же получена из предшествующих выводимостей по одному из правил:• правило дедукции (Г, А├В) ├ (Г├А→В);• правило доказательства от противного (Г, ¬A├B^¬B)├(Г├A);• правило сведения к абсурду (Г, ¬А├В^¬В)├(Г├¬А).Эти правила называются правшами второго рода, в отличие от правил В1 - В12.(гл1,§1.5), которые называются правилами первого рода.
В приведенных правилах Г - множествогипотез (формул), возможно непустое, А, В - формулы.Выводимость, для которой есть доказательство, называется обоснованной.В приведенном определении вывода осталось нераскрытым понятие теоремы.Существует несколько равнозначных определений понягия теоремы. Приведем два из них:Если В есть логическое следствие формул A1, …, An, то формула ((A1, …, An)→В)называется теоремой, а В - заключение теоремы.Формула А называется теоремой, если и только если существует обоснованнаявыводимость Г├А, для которой Г пусто.Например, пусть требуется обосновать выводимость формулы ├(c→d)→(¬d→¬c), т.е.установить, что приведенная формула является теоремой.
Естественно, что доказательстводолжно опираться на посылки (гипотезы). Правомочен вопрос, как определить в поставленнойзадаче гипотезы. Возможны два способа выделения гипотез:• если главный знак (логическая связка) формулы не является конъюнкцией илиэквивалентностью, то можно взять в качестве единственной гипотезы отрицание этойформулы. Для приведенного примера¬((c→d)→(¬d→¬c));• если главным знаком формулы является импликация, то в качестве гипотезы взятьантецедент (посылку) этой формулы (в примере c→d);• если консеквент (следствие) формулы имеет главным знаком импликацию, то вкачестве второй гипотезы взять антецедент консеквента и т.д. Из полученных гипотезследует вывести консеквент последнего консеквента.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
