5.11: Задоволення формули в структурі

Template:MathJaxZach

Основне поняття, яке пов'язує такі вирази, як терміни та формули, з одного боку, та структури, з іншого, - це значення терміна та задоволення формули. Неофіційно значення терміна є елементом структури - якщо термін є просто константою, його значенням є об'єкт, присвоєний константі структурою, а якщо він побудований за допомогою функціональних символів, значення обчислюється зі значень констант і функцій, присвоєних функціям у терміні. Формула задовольняється в структурі, якщо інтерпретація, надана предикатам, робить формулу істинною в області структури. Це поняття задоволення задається індуктивно: специфікація структури безпосередньо визначає, коли атомні формули задовольняються, і ми визначаємо, коли складна формула задовольняється залежно від основного сполучного або кількісного показника та чи задовольняються безпосередні підформули чи ні. Випадок кванторів тут трохи складний, оскільки безпосередня підформула кількісної формули має вільну змінну, а структури не вказують значення змінних. Щоб вирішити цю складність, ми також вводимо присвоєння змінних та визначаємо задоволення не лише щодо структури, а щодо структури плюс присвоєння змінної.

Визначення\(\PageIndex{1}\): Variable Assignment

Присвоєння змінної\(s\) для структури\(\Struct{M}\) - це функція, яка відображає кожну змінну з елементом\(\Domain M\), тобто\(s\colon \Var \to \Domain M\).

Структура привласнює значення кожному символу константи, а змінну присвоює кожній змінній. Але ми хочемо використовувати терміни, побудовані з них, щоб також називати елементи домену. Для цього ми визначаємо значення термінів індуктивно. Для постійних символів та змінних значення є таким же, як його визначає структура або присвоєння змінних; для більш складних термінів воно обчислюється рекурсивно за допомогою функцій, які структура призначає символам функцій.

Визначення\(\PageIndex{2}\): Value of Terms

Якщо\(t\) є терміном мови\(\Lang L\),\(\Struct M\) є структурою for\(\Lang L\) і\(s\) є змінною присвоєння\(\Struct M\), значення\(\Value[s]{t}{M}\) визначається наступним чином:

1. \(\indcase{t}{c}\)\(\Value[s]{t}{M} = \Assign{c}{M}\).

2. \(\indcase{t}{x}\)\(\Value[s]{t}{M} = s(x)\).

3. \(\indcase{t}{\Atom{f}{t_1, \ldots, t_n}}\)\[\Value[s]{t}{M} = \Assign{f}{M}(\Value[s]{t_1}{M}, \ldots, \Value[s]{t_n}{M}).\nonumber\]

Визначення\(\PageIndex{3}\): \(x\)-Variant

Якщо\(s\) є присвоєнням змінної для структури\(\Struct M\), то будь-яке присвоєння змінної,\(s'\) для\(\Struct M\) якої відрізняється\(s\) максимум від того, чому вона присвоює,\(x\) називається \(x\)-варіант\(s\). Якщо\(s'\)\(x\) -варіант\(s\) ми пишемо\(\varAssign{s'}{s}{x}\).

Зауважте, що\(x\) -варіант присвоєння\(s\) не повинен призначати щось інше\(x\). Насправді кожне завдання вважається\(x\) -варіантом самого себе.

Визначення\(\PageIndex{4}\): Satisfaction

Задоволеність формули\(A\) в структурі\(\Struct M\) щодо присвоєння змінної\(s\), в символах:\(\Sat[,s]{M}{A}\), визначається рекурсивно наступним чином. (Ми пишемо\(\SatN[,s]{M}{A}\), щоб означати «ні»\(\Sat[,s]{M}{A}\).)

1. \(\indcase{A}{\lfalse}\)\(\SatN[,s]{M}{\indfrm}\).

2. \(\indcase{A}{\Atom{R}{t_1, \dots, t_n}}\)\(\Sat[,s]{M}{\indfrm}\)іфф\(\langle \Value[s]{t_1}{M}, \dots, \Value[s]{t_n}{M} \rangle \in \Assign{R}{M}\).

3. \(\indcase{A}{\eq[t_1][t_2]}\)\(\Sat[,s]{M}{\indfrm}\)іфф\(\Value[s]{t_1}{M} = \Value[s]{t_2}{M}\).

4. \(\indcase{A}{\lnot B}\)\(\Sat[,s]{M}{\indfrm}\)іфф\(\SatN[,s]{M}{B}\).

5. \(\indcase{A}{(B \land C)}\)\(\Sat[,s]{M}{\indfrm}\)іфф\(\Sat[,s]{M}{B}\) і\(\Sat[,s]{M}{C}\).

6. \(\indcase{A}{(B \lor C)}\)\(\Sat[,s]{M}{\indfrm}\)iff\(\Sat[,s]{M}{A}\) або\(\Sat[,s]{M}{B}\) (або обидва).

7. \(\indcase{A}{(B \lif C)}\)\(\Sat[,s]{M}{\indfrm}\)iff\(\SatN[,s]{M}{B}\) або\(\Sat[,s]{M}{C}\) (або обидва).

8. \(\indcase{A}{\lforall{x}{B}}\)\(\Sat[,s]{M}{\indfrm}\)iff для кожного\(x\) -варіанту\(s'\)\(s\),\(\Sat[,s']{M}{B}\).

9. \(\indcase{A}{\lexists{x}{B}}\)\(\Sat[,s]{M}{\indfrm}\)якщо є\(x\) -варіант\(s'\)\(s\) так, що\(\Sat[,s']{M}{B}\).

Призначення змінних є важливими в останніх двох реченнях. Ми не можемо визначити задоволення «для всіх\(a \in \Domain{M}\)»\(\Sat{M}{B(a)}\).\(\lforall{x}{B(x)}\) Ми не можемо визначити задоволення «принаймні для одного\(a \in \Domain{M}\)»\(\Sat{M}{B(a)}\).\(\lexists{x}{B(x)}\) Причина в тому, що не\(a\) є символом мови, а так не\(B(a)\) є формулою (\(\Subst{B}{a}{x}\)тобто невизначеною). Ми також не можемо припустити, що у нас є постійні символи або терміни, які називають кожен елемент\(\Struct{M}\), оскільки у визначенні структур немає нічого, що цього вимагає. Навіть у стандартній мові набір постійних символів незліченно нескінченний, тому, якщо\(\Domain{M}\) не перелічити, навіть не вистачає постійних символів, щоб назвати кожен об'єкт.

Приклад\(\PageIndex{1}\)

Нехай\(\Lang{L} = \{a, b, f, R\}\) де\(a\) і\(b\) є постійними символами,\(f\) є символом двомісної функції, і\(R\) є двомісним символом предиката. Розглянемо структуру,\(\Struct{M}\) визначену:

1. \(\Domain M = \{1, 2, 3, 4\}\)

2. \(\Assign{a}{M} = 1\)

3. \(\Assign{b}{M} = 2\)

4. \(\Assign{f}{M}(x, y) = x+y\)якщо\(x+y \le 3\) і в\(= 3\) іншому випадку.

5. \(\Assign{R}{M} = \{\tuple{1, 1}, \tuple{1, 2}, \tuple{2, 3}, \tuple{2, 4}\}\)

Функція\(s(x) = 1\), яка\(1 \in \Domain{M}\) призначає кожній змінній, є присвоєнням змінної для\(\Struct{M}\).

Тоді

\[\Value[s]{f(a,b)}{M} = \Assign{f}{M}(\Value[s]{a}{M}, \Value[s]{b}{M}).\nonumber\]

Так як\(a\) і\(b\) є постійними символами,\(\Value[s]{a}{M} = \Assign{a}{M} = 1\) і\(\Value[s]{b}{M} = \Assign{b}{M} = 2\). Так

\[\Value[s]{f(a,b)}{M} = \Assign{f}{M}(1, 2) = 1+2 = 3.\nonumber\]

Щоб обчислити значення,\(f(f(a,b),a)\) ми повинні розглянути

\[\Value[s]{f(f(a,b),a)}{M} = \Assign{f}{M}(\Value[s]{f(a, b)}{M}, \Value[s]{a}{M}) = \Assign{f}{M}(3, 1) = 3,\nonumber\]

так як\(3+1 > 3\). З тих пір\(s(x) = 1\) і\(\Value[s]{x}{M} = s(x)\), у нас також є

\[\Value[s]{f(f(a,b),x)}{M} = \Assign{f}{M}(\Value[s]{f(a, b)}{M}, \Value[s]{x}{M}) = \Assign{f}{M}(3, 1) = 3.\nonumber\]

Атомна формула\(R(t_1, t_2)\) задовольняється, якщо кортеж значень її аргументів\(\tuple{\Value[s]{t_1}{M}, \Value[s]{t_2}{M}}\), тобто є елементом\(\Assign{R}{M}\). Так, наприклад, ми маємо\(\Sat[,s]{M}{R(b,f(a,b))}\) з тих пір\(\tuple{\Value{b}{M}, \Value{f(a,b)}{M}} = \tuple{2, 3} \in \Assign{R}{M}\), але\(\SatN[,s]{M}{R(x, f(a,b))}\) з тих пір\(\tuple{1, 3} \notin \Assign{R}{M}[s]\).

Щоб визначити, чи\(A\) задовольняється неатомна формула, ви застосовуєте пункти індуктивного визначення, яке стосується основного сполучного. Наприклад, основною сполучною в\(R(a, a) \lif (R(b, x) \lor R(x, b))\) є\(\lif\), і

\ [\ почати {вирівняний}
&\ Сб [, с] {М} {R (a, a)\ lif (R (b, x)\ lor R (x, b))}\ текст {iff}\
&\ qquad\ SatN [, s] {M} {R (a, a)}\ текст {або}\ сб [, s] {M} {R (a, a)}\ текст {або}\ Сб [, s] {M} {R (a, a))\ або R (x, b)}
\ кінець {вирівняний}\]

Оскільки\(\Sat[,s]{M}{R(a,a)}\) (тому що\(\tuple{1,1} \in \Assign{R}{M}\)) ми ще не можемо визначити відповідь і повинні спочатку з'ясувати, якщо\(\Sat[,s]{M}{R(b, x) \lor R(x, b)}\):

\ [\ почати {вирівняний}
&\ Сб [, с] {М} {R (b, x)\ lor R (x, b)}\ текст {iff}\\
&\ qquad\ Сб [, s] {M} {R (b, x)}\ текст {або}\ Сб [, s] {M} {R (x, b)}
\ кінець {вирівняний}\]

І це так, оскільки\(\Sat[,s]{M}{R(x, b)}\) (тому що\(\tuple{1,2} \in \Assign{R}{M}\)).

Нагадаємо, що a\(x\) -variant of\(s\) - це\(s\) змінна присвоєння, яка відрізняється від максимум тим, що йому присвоюється\(x\). Для кожного елемента\(\Domain{M}\) існує\(x\) -варіант\(s\):\(s_1(x) = 1\),,\(s_2(x) = 2\)\(s_3(x) = 3\)\(s_4(x) = 4\), і with\(s_i(y) = s(y) = 1\) для всіх змінних\(y\) крім\(x\). Це все\(x\) -варіанти\(s\) для будови\(\Struct{M}\), так як\(\Domain{M} = \{1, 2, 3, 4\}\). Відзначимо, зокрема, що\(s_1 = s\) це теж\(x\) -варіант\(s\),\(s\) тобто завжди\(x\) -варіант самого себе.

Щоб визначити, чи\(\lexists{x}{A(x)}\) задовольняється екзистенціально кількісна формула, ми повинні визначити, чи\(\Sat[,s']{M}{A(x)}\) є принаймні один\(x\) -варіант\(s'\)\(s\). Отже,\[\Sat[,s]{M}{\lexists{x}{(R(b,x) \lor R(x,b))}},\nonumber\] оскільки\(\Sat[,s_1]{M}{R(b,x) \lor R(x, b)}\) (також підходив\(s_3\) би рахунок). Але,\[\SatN[,s]{M}{\lexists{x}{(R(b,x) \land R(x,b))}}\nonumber\] так як ні для кого з\(s_i\),\(\Sat[,s_i]{M}{R(b,x) \land R(x,b)}\).

Щоб визначити, чи\(\lforall{x}{A(x)}\) задовольняється універсально кількісна формула, ми повинні визначити, чи\(\Sat[,s']{M}{A(x)}\) для всіх\(x\)\(s'\) -варіантів\(s\). Отже,\[\Sat[,s]{M}{\lforall{x}{(R(x,a) \lif R(a,x))}},\nonumber\] так як\(\Sat[,s_i]{M}{R(x,a) \lif R(a,x)}\) для всіх\(s_i\) (\(\Sat[,s_1]{M}{R(a,x)}\)і\(\SatN[,s_j]{M}{R(x,a)}\) для\(j = 2\)\(3\), і\(4\)). Але,\[\SatN[,s]{M}{\lforall{x}{(R(a,x) \lif R(x,a))}}\nonumber\] так як\(\SatN[,s_2]{M}{R(a,x) \lif R(x,a)}\) (тому що\(\Sat[,s_2]{M}{R(a, x)}\) і\(\SatN[,s_2]{M}{R(x, a)}\)).

Для більш складного випадку розглянемо\[\lforall{x}{(R(a,x) \lif \lexists{y}{R(x,y)})}.\nonumber\] Оскільки\(\SatN[,s_3]{M}{R(a,x)}\) і цікаві випадки\(\SatN[,s_4]{M}{R(a,x)}\), коли нам доводиться турбуватися про наслідок умовного, є лише\(s_1\) і\(s_2\). Чи\(\Sat[,s_1]{M}{\lexists{y}{R(x,y)}}\) тримає? Він робить, якщо є хоча б один\(y\) -варіант\(s_1'\)\(s_1\) так, що\(\Sat[,s_1']{M}{R(x,y)}\). По суті,\(s_1\) є такий\(y\) -варіант (\(s_1(x) = 1\)\(s_1(y) = 1\),, і\(\tuple{1,1} \in \Assign{R}{M}\)), тому відповідь так. Щоб визначити, чи\(\Sat[,s_2]{M}{\lexists{y}{R(x,y)}}\) треба дивитися на\(y\) -варіанти\(s_2\). Тут,\(s_2\) себе не задовольняє\(R(x,y)\) (\(s_2(x) = 2\),\(s_2(y) = 1\), і\(\tuple{2,1}\notin \Assign{R}{M}\)). Однак розглянемо\(\varAssign{s_2'}{s_2}{y}\) с\(s_2'(y) = 3\). \(\Sat[,s_2']{M}{R(x,y)}\)з тих пір\(\tuple{2,3} \in \Assign{R}{M}\), і так\(\Sat[,s_2]{M}{\lexists{y}{R(x,y)}}\). У сумі, для кожного\(x\) -варіанту\(s_i\)\(s\), або\(\SatN[,s_i]{M}{R(a,x)}\) (\(i = 3\),\(4\)) або\(\Sat[,s_i]{M}{\lexists{y}{R(x,y)}}\) (\(i = 1\),\(2\)), і так\[\Sat[,s]{M}{\lforall{x}{(R(a,x) \lif \lexists{y}{R(x,y)})}}.\nonumber\] З іншого боку,\[\SatN[,s]{M}{\lexists{x}{(R(a,x) \land \lforall{y}{R(x,y)})}}.\nonumber\] єдиними\(x\)\(s_i\) -варіантами\(s\) з\(\Sat[,s_i]{M}{R(a,x)}\) є\(s_1\) і\(s_2\). Але для кожного, є по черзі свій\(y\) -варіант\(\varAssign{s_i'}{s_i}{y}\) з\(s_i'(y) = 4\) так що\(\SatN[,s_i']{M}{R(x,y)}\) і так\(\SatN[,s_i]{M}{\lforall{y}{R(x,y)}}\) для\(i = 1\),\(2\). Підсумовуючи, жоден з\(x\) -варіантів не\(\varAssign{s_i}{s}{x}\) є таким, що\(\Sat[,s_i]{M}{R(a,x) \land \lforall{y}{R(x,y)}}\).

Проблема\(\PageIndex{1}\)

Нехай\(\Lang L = \{c, f, A\}\) з одним постійним символом, одним символом функції одного місця і одним двомісним символом присудка, і нехай структура\(\Struct{M}\) буде задана

1. \(\Domain M = \{1, 2, 3\}\)

2. \(\Assign{c}{M} = 3\)

3. \(\Assign{f}{M}(1) = 2, \Assign{f}{M}(2) = 3, \Assign{f}{M}(3) = 2\)

4. \(\Assign{A}{M} = \{\tuple{1, 2}, \tuple{2, 3}, \tuple{3, 3}\}\)

(а) Нехай\(s(v) = 1\) для всіх змінних\(v\). Дізнайтеся, чи\[\Sat[,s]{M}{\lexists{x}{(A(f(z), c) \lif \lforall{y}{(A(y, x) \lor A(f(y), x))})}}\nonumber\] поясніть, чому чи ні.

(b) Дайте іншу структуру та присвоєння змінних, в яких формула не задовольняється.