5.13: Розширення

Last updated
Save as PDF

Page ID: 53021

$ \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

Розширеність, яку іноді називають релевантністю, може бути виражена неофіційно наступним чином: єдиними факторами, які впливають на задоволення формули$A$ в структурі$\Struct M$ щодо змінної присвоєння$s$, є розмір домену та призначення зроблені$\Struct M$ і$s$ до елементів мови, які насправді з'являються в$A$.

Одним з безпосередніх наслідків розширення є те, що там, де дві структури$\Struct M$ і$\Struct M'$ узгоджуються з усіма елементами мови, що з'являються в реченні$A$ і мають однаковий домен,$\Struct M$ а також$\Struct M'$ повинні погодитися на чи правда$A$ сама по собі.

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

$A$Дозволяти бути формулою,$\Struct M_1$ і$\Struct M_2$ бути структури з$\Domain{M_1} = \Domain{M_2}$, і$s$ змінної присвоєння на$\Domain{M_1} = \Domain{M_2}$. Якщо$\Assign{c}{M_1} = \Assign{c}{M_2}$$\Assign{R}{M_1}=\Assign{R}{M_2}$, і$\Assign{f}{M_1} = \Assign{f}{M_2}$ для кожного постійного символу$c$, символ відношення$R$, і символ функції,$f$ що відбуваються в$A$, то$\Sat[,s]{M_1}{A}$ iff $\Sat[,s]{M_2}{A}$.

Доказ. Спочатку довести (шляхом індукції$t$), що для кожного терміну,$\Value[s]{t}{M_1} = \Value[s]{t}{M_2}$. Потім довести пропозицію шляхом індукції на$A$, використовуючи твердження, щойно доведене для індукційної основи (де$A$ атомний) . ◻

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

Детально проведіть доказ Пропозиції$\PageIndex{1}$.

Слідство$\PageIndex{1}$: Extensionality for Sentences

$A$Дозволяти бути реченням і$\Struct{M_1}$,$\Struct{M_2}$ як в Пропозиції$\PageIndex{1}$. Потім$\Sat{M_1}{A}$ вимкніть$\Sat{M_2}{A}$.

Доказ. Випливає з пропозиції$\PageIndex{1}$ за наслідком 5.12.1. ◻

Причому значення терміна, а також задовольняє чи ні структура формулі, залежить тільки від значень його підтермінів.

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

$\Struct M$Дозволяти бути і структура,$t$ і$t'$ терміни, і$s$ змінна присвоєння. $\varAssign{s'}{s}{x}$Дозволяти бути$x$ -варіант$s$ заданого$s'(x) = \Value[s]{t'}{M}$. Потім$\Value[s]{\Subst{t}{t'}{x}}{M} = \Value[s']{t}{M}$.

Доказ. За допомогою індукції на$t$.

Якщо$t$ постійна, скажімо$t\ident c$, то$\Subst{t}{t'}{x} = c$, і$\Value[s]{c}{M} = \Assign{c}{M} = \Value[s']{c}{M}$.
Якщо$t$ змінна, відмінна$x$, скажімо$t \ident y$, то$\Subst{t}{t'}{x} = y$, і$\Value[s]{y}{M} = \Value[s']{y}{M}$ так як$\varAssign{s'}{s}{x}$.
Якщо$t \ident x$, то$\Subst{t}{t'}{x} = t'$. Але$\Value[s']{x}{M} = \Value[s]{t'}{M}$ за визначенням$s'$.
Якщо$t \ident \Atom{f}{t_1,\dots,t_n}$ тоді у нас є:\[\begin{gathered} \begin{aligned}[b] \Value[s]{\Subst{t}{t'}{x}}{M} & = \Value[s]{\Atom{f}{\Subst{t_1}{t'}{x}, \dots, \Subst{t_n}{t'}{x}}}{M}\\ & \qquad \text{ by definition of $\Subst{t}{t'}{x}$}\\ & = \Assign{f}{M}(\Value[s]{\Subst{t_1}{t'}{x}}{M}, \dots, \Value[s]{\Subst{t_n}{t'}{x}}{M})\\ & \qquad \text{ by definition of $\Value[s]{\Atom{f}{\dots}}{M}$}\\ & = \Assign{f}{M}(\Value[s']{t_1}{M}, \dots, \Value[s']{t_n}{M})\\ & \qquad \text{ by induction hypothesis}\\ & = \Value[s']{t}{M} \text{ by definition of $\Value[s']{\Atom{f}{\dots}}{M}$} \end{aligned}\end{gathered}\]

◻

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

$\Struct M$Дозволяти структура,$A$ формула,$t$ термін, і$s$ змінна присвоєння. $\varAssign{s'}{s}{x}$Дозволяти бути$x$ -варіант$s$ заданого$s'(x) = \Value[s]{t}{M}$. Потім$\Sat[,s]{M}{\Subst{A}{t}{x}}$ вимкніть$\Sat[,s']{M}{A}$.

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

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

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