5.12: Призначення змінних

Last updated
Save as PDF

Page ID: 52978

$ \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } $ $ \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} $$\newcommand{\id}{\mathrm{id}}$ $ \newcommand{\Span}{\mathrm{span}}$ $ \newcommand{\kernel}{\mathrm{null}\,}$ $ \newcommand{\range}{\mathrm{range}\,}$ $ \newcommand{\RealPart}{\mathrm{Re}}$ $ \newcommand{\ImaginaryPart}{\mathrm{Im}}$ $ \newcommand{\Argument}{\mathrm{Arg}}$ $ \newcommand{\norm}[1]{\| #1 \|}$ $ \newcommand{\inner}[2]{\langle #1, #2 \rangle}$ $ \newcommand{\Span}{\mathrm{span}}$ $\newcommand{\id}{\mathrm{id}}$ $ \newcommand{\Span}{\mathrm{span}}$ $ \newcommand{\kernel}{\mathrm{null}\,}$ $ \newcommand{\range}{\mathrm{range}\,}$ $ \newcommand{\RealPart}{\mathrm{Re}}$ $ \newcommand{\ImaginaryPart}{\mathrm{Im}}$ $ \newcommand{\Argument}{\mathrm{Arg}}$ $ \newcommand{\norm}[1]{\| #1 \|}$ $ \newcommand{\inner}[2]{\langle #1, #2 \rangle}$ $ \newcommand{\Span}{\mathrm{span}}$

Template:MathJaxZach

Присвоєння змінних$s$ надає значення для кожної змінної - і їх нескінченно багато. Це, звичайно, не обов'язково. Ми вимагаємо призначення змінних, щоб призначити значення всім змінним просто тому, що це робить речі набагато простіше. Значення терміна$t$, і чи$A$ задовольняється формула в структурі стосовно$s$, залежить тільки від призначення$s$ робить змінні в$t$ і вільних змінних $A$. Це зміст наступних двох пропозицій. Щоб зробити ідею «залежить від» точною, ми показуємо, що будь-які дві змінні призначення, які узгоджуються з усіма змінними,$t$ дають однакове значення, і що$A$ задовольняється відносно одного, якщо воно задовольняється відносно іншого, якщо два призначення змінних узгоджуються з усіма вільні змінні$A$.

Пропозиція$\PageIndex{1}$

Якщо змінні в терміні$t$ є серед$x_1$,...,$x_n$, і$s_1(x_i) = s_2(x_i)$ for$i = 1$,...,$n$, то$\Value[s_1]{t}{M} = \Value[s_2]{t}{M}$.

Доказ. За індукцією за складністю$t$. Для базового випадку$t$ може бути постійним символом або однією зі змінних$x_1$,...,$x_n$. Якщо$t = c$, то$\Value[s_1]{t}{M} = \Assign{c}{M} = \Value[s_2]{t}{M}$. Якщо$t = x_i$,$s_1(x_i) = s_2(x_i)$ за гіпотезою судження, і так$\Value[s_1]{t}{M} = s_1(x_i) = s_2(x_i) = \Value[s_2]{t}{M}$.

Для індуктивного кроку припустимо, що$t = \Atom{f}{t_1, \dots, t_k}$ і що позов тримає$t_1$,...,$t_k$. Тоді

\ [\ begin {вирівняний}
\ Значення [s_1] {t} {M}
& =\ Значення [s_1] {\ Atom {f} {t_1,\ dots, t_k}} {M} =\\
& =\ Призначити {f} {M} (\ Значення [s_1] {t_1} {M},\ точки,\ Значення [s_1] {t_1} {M},\ точки,\ Значення [s_1] {t_1} {M} k} {M})
\ кінець {вирівняний}\]

Для$j = 1, \dots, k$, змінні$t_j$ знаходяться серед$x_1, \dots,x_n$. Отже, індукційна гіпотеза,$\Value[s_1]{t_j}{M} = \Value[s_2]{t_j}{M}$. Отже,

\ [\ begin {вирівняний}
\ Значення [s_1] {t} {M} & =\ Значення [s_2] {\ Atom {f} {t_1,\ dots, t_k}} {M} =\\ & =\ Призначити {f} {M} (\ Значення [s_1] {t_1} {M},\ точки,\ Значення [s_1] {t_1} {M},\ точки,\ Значення [s_1] {t_1} {M} k} {M}) =\\ & =\ Призначити {f} {M} (\ Значення [s_2] {t_1} {M},\ точки,\ Значення [s_2] {t_k} {M}) =\\ & =\ Значення [s_2] {\ Atom {f} {t_1,\ dots, t_k}} {M} =\ Значення [ s_2] {т} {М}. \ кінець {вирівняний}\] ◻

Пропозиція$\PageIndex{2}$

Якщо вільні$A$ змінні в є серед$x_1$,...$x_n$, і$s_1(x_i) = s_2(x_i)$ for$i = 1$,...$n$, то$\Sat[,s_1]{M}{A}$ iff$\Sat[,s_2]{M}{A}$.

Доказ. Використовуємо індукцію за складністю$A$. Для базового випадку, де$A$ атомний,$A$ може бути:$\lfalse$,$\Atom{R}{t_1, \dots, t_k}$ для$k$ присудка$R$ та термінів$t_1$,...$t_k$, або$\eq[t_1][t_2]$ для термінів$t_1$ і$t_2$.

$\indcase{A}{\lfalse}$$\SatN[,s_1]{M}{A}$і те й інше$\SatN[,s_2]{M}{A}$.
$\indcase{A}{\Atom{R}{t_1, \ldots, t_k}}$нехай$\Sat[,s_1]{M}{\indfrm}$. Тоді\[\langle \Value[s_1]{t_1}{M}, \ldots, \Value[s_1]{t_k}{M} \rangle \in \Assign{R}{M}.\nonumber\] для$i = 1$,...,,$k$,$\Value[s_1]{t_i}{M} = \Value[s_2]{t_i}{M}$ за пропозицією$\PageIndex{1}$. Так що у нас теж є$\langle \Value[s_2]{t_i}{M}, \ldots, \Value[s_2]{t_k}{M} \rangle \in \Assign{R}{M}$.
$\indcase{A}{\eq[t_1][t_2]}$припустимо$\Sat[,s_1]{M}{\indfrm}$. Потім$\Value[s_1]{t_1}{M} = \Value[s_1]{t_2}{M}$. Отже,\[\begin{aligned} \Value[s_2]{t_1}{M} & = \Value[s_1]{t_1}{M} & \text{(by Proposition $\PageIndex{1}$)} \\ & = \Value[s_1]{t_2}{M} & \text{(since $\Sat[,s_1]{M}{\eq[t_1][t_2]}$)}\\ &= \Value[s_2]{t_2}{M} & \text{(by Proposition $\PageIndex{1}$),} \end{aligned}\] так$\Sat[,s_2]{M}{\eq[t_1][t_2]}$.

Тепер припустимо, що$\Sat[,s_1]{M}{B}$ iff$\Sat[,s_2]{M}{B}$ для всіх формул$B$ менш складним, ніж$A$. Крок індукції протікає за випадками, визначеними головним оператором$A$. У кожному випадку ми демонструємо лише прямий напрямок біумовного; доказ зворотного напрямку симетричний. У всіх випадках, крім кількісних показників, ми застосовуємо індукційну гіпотезу до$B$ підформул$A$. Вільні змінні$B$ є одними з тих, з$A$. Таким чином, якщо$s_1$ і$s_2$ погоджуються на вільні змінні$A$, вони також погоджуються з тими$B$, і індукційна гіпотеза застосовується до$B$.

$\indcase{A}{\lnot B}$якщо$\Sat[,s_1]{M}{\indfrm}$, то$\SatN[,s_1]{M}{B}$, так індукційної гіпотезою$\SatN[,s_2]{M}{B}$, отже$\Sat[,s_2]{M}{\indfrm}$.
$\indcase{A}{B \land C}$вправа.
$\indcase{A}{B \lor C}$якщо$\Sat[,s_1]{M}{\indfrm}$, то$\Sat[,s_1]{M}{B}$ або$\Sat[,s_1]{M}{C}$. За індукційною гіпотезою$\Sat[,s_2]{M}{C}$,$\Sat[,s_2]{M}{B}$ або, так$\Sat[,s_2]{M}{\indfrm}$.
$\indcase{A}{B \lif C}$вправа.
$\indcase{A}{\lexists{x}{B}}$якщо$\Sat[,s_1]{M}{\indfrm}$, є$x$ -варіант$s_1'$$s_1$ так, що$\Sat[,s_1']{M}{B}$. $s_2'$Дозволяти бути$x$ -варіант$s_2$, що призначає те ж саме$x$, що і робить$s_1'$. Вільні змінні$B$ є серед$x_1$,...,$x_n$, і$x$. $s_1'(x_i) = s_2'(x_i)$, Так як$s_1'$ і$s_2'$ є$x$ -варіанти$s_1$ і$s_2$, відповідно, і по гіпотезі$s_1(x_i) = s_2(x_i)$. $s_1'(x) = s_2'(x)$до того, як ми визначили$s_2'$. Тоді індукційна гіпотеза застосовується$B$ і$s_1'$$s_2'$, так$\Sat[,s_2']{M}{B}$. Отже, існує$x$ -варіант,$s_2$ який задовольняє$B$, і так$\Sat[,s_2]{M}{\indfrm}$.
$\indcase{A}{\lforall{x}{B}}$вправа.

За допомогою індукції ми отримуємо, що$\Sat[,s_1]{M}{A}$ iff$\Sat[,s_2]{M}{A}$ всякий раз, коли вільні змінні$A$ знаходяться серед$x_1$,...,$x_n$ і$s_1(x_i)=s_2(x_i)$ для$i = 1$,...,$n$. ◻

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

Заповніть доказ Пропозиції$\PageIndex{2}$.

Речення не мають вільних змінних, тому будь-які дві змінні присвоюють однакові речі всім (нульовим) вільним змінним будь-якого речення. Пропозиція щойно доведена тоді означає, що чи задовольняється речення у структурі відносно змінної присвоєння, повністю не залежить від присвоєння. Ми зафіксуємо цей факт. Обґрунтовано визначення задоволеності речення в структурі (без згадки змінної присвоєння), яка слідує за нею.

Слідство$\PageIndex{1}$

Якщо$A$ є реченням і$s$ присвоєнням змінної, то$\Sat[,s]{M}{A}$ iff$\Sat[,s']{M}{A}$ для кожного присвоєння змінної$s'$.

Доказ. $s'$Дозволяти будь змінної присвоєння. Оскільки$A$ це речення, воно не має вільних змінних, і тому кожне присвоєння змінних$s'$ тривіально призначає ті ж речі всім вільним змінним,$A$ як це робить$s$. Таким чином, умова Пропозиції$\PageIndex{2}$ задовольняється, і ми маємо$\Sat[,s]{M}{A}$ iff$\Sat[,s']{M}{A}$. ◻

Визначення$\PageIndex{1}$

Якщо$A$ це речення, ми говоримо, що структура$\Struct M$ задовольняє$A$,$\Sat{M}{A}$, iff$\Sat[,s]{M}{A}$ для всіх змінних присвоєнь$s$.

Якщо$\Sat{M}{A}$, ми також просто говоримо, що$A$ це правда в$\Struct{M}$.

Пропозиція$\PageIndex{3}$

$\Struct{M}$Дозволяти бути структурою,$A$ бути реченням і$s$ змінною присвоєння. $\Sat{M}{A}$іфф$\Sat[,s]{M}{A}$.

Доказ. Вправа. ◻

Проблема$\PageIndex{2}$

Доведіть пропозицію$\PageIndex{3}$.

Пропозиція$\PageIndex{4}$

Припустимо, що містить$A(x)$ лише$x$ вільну, і$\Struct M$ є структурою. Потім:

$\Sat{M}{\lexists{x}{A(x)}}$iff$\Sat[,s]{M}{A(x)}$ для принаймні одного присвоєння змінної$s$.
$\Sat{M}{\lforall{x}{A(x)}}$iff$\Sat[,s]{M}{A(x)}$ для всіх присвоєнь змінних$s$.

Доказ. Вправа. ◻

Проблема$\PageIndex{3}$

Доведіть пропозицію$\PageIndex{4}$.

Проблема$\PageIndex{4}$

$\Lang L$Припустимо, мова без функціональних символів. Враховуючи структуру$\Struct M$,$c$ постійний символ і$a \in \Domain M$, визначити,$\Struct M[a/c]$ щоб бути структура, яка так само$\Struct M$, як, крім цього$\Assign{c}{M[a/c]} = a$. Визначте$\Struct M \mathrel{||}\joinrel\Relbar A$ для речень$A$ за допомогою:

$\indcase{A}{\lfalse}$ні$\Struct{M} \mathrel{||}\joinrel\Relbar\indfrm$.
$\indcase{A}{\Atom{R}{d_1, \dots, d_n}}$$\Struct M \mathrel{||}\joinrel\Relbar\indfrm$іфф$\langle \Assign{d_1}{M}, \dots, \Assign{d_n}{M} \rangle \in \Assign{R}{M}$.
$\indcase{A}{\eq[d_1][d_2]}$$\Struct M \mathrel{||}\joinrel\Relbar\indfrm$іфф$\Assign{d_1}{M} = \Assign{d_2}{M}$.
$\indcase{A}{\lnot B}$$\Struct{M} \mathrel{||}\joinrel\Relbar\indfrm$Якщо ні$\Struct{M} \mathrel{||}\joinrel\Relbar{B}$.
$\indcase{A}{(B \land C)}$$\Struct{M} \mathrel{||}\joinrel\Relbar \indfrm$іфф$\Struct{M} \mathrel{||}\joinrel\Relbar B$ і$\Struct{M} \mathrel{||}\joinrel\Relbar C$.
$\indcase{A}{(B \lor C)}$$\Struct{M} \mathrel{||}\joinrel\Relbar\indfrm$iff$\Struct{M} \mathrel{||}\joinrel\Relbar B$ або$\Struct{M} \mathrel{||}\joinrel\Relbar C$ (або обидва).
$\indcase{A}{(B \lif C)}$$\Struct{M} \mathrel{||}\joinrel\Relbar\indfrm$Якщо ні$\Struct {M} \mathrel{||}\joinrel\Relbar B$ або$\Struct M \mathrel{||}\joinrel\Relbar C$ (або обидва).
$\indcase{A}{\lforall{x}{B}}$$\Struct{M} \mathrel{||}\joinrel\Relbar{\indfrm}$якщо для всіх$a \in \Domain{M}$$\Struct{M[a/c]} \mathrel{||}\joinrel\Relbar\Subst{B}{c}{x}$, якщо$c$ не відбувається в$B$.
$\indcase{A}{\lexists{x}{B}}$$\Struct{M} \mathrel{||}\joinrel\Relbar {\indfrm}$якщо є$a \in \Domain M$ таке$\Struct{M[a/c]} \mathrel{||}\joinrel\Relbar\Subst{B}{c}{x}$, що, якщо$c$ не відбувається в$B$.

Нехай$x_1$,...,$x_n$ бути всі вільні змінні в$A$$c_1$,,...,$c_n$ постійні символи не в$A$,$a_1$,...,$a_n \in \Domain M$, і$s(x_i) = a_i$.

Покажіть, що$\Sat[,s]{M}{A}$ якщо$\Struct M[a_1/c_1,\dots,a_n/c_n] \mathrel{||}\joinrel\Relbar\Subst{\Subst{A}{c_1}{x_1}\dots}{c_n}{x_n}$.

(Ця проблема показує, що можна дати семантику для логіки першого порядку, яка дозволяє обійтися без присвоєння змінних.)

Проблема$\PageIndex{5}$

Припустимо, що$f$ це символ функції не в$A(x,y)$. Покажіть, що існує структура$\Struct{M}$ така,$\Sat{M}{\lforall{x}{\lexists{y}{A(x,y)}}}$ що якщо є$\Struct M'$ така, що$\Sat{M'}{\lforall{x}{A(x,f(x))}}$.

(Ця задача є окремим випадком того, що відоме як теорема Сколема;$\lforall{x}{A(x,f(x))}$ називається нормальною формою Сколема$\lforall{x}{\lexists{y}{A(x,y)}}$.)