10.7: Ідентичність

Last updated
Save as PDF

Page ID: 52811

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

Побудова термінової моделі, наведеної в попередньому розділі, достатньо для встановлення повноти логіки першого порядку для множин$\Gamma$, які не містять$\eq[][]$. Термін модель задовольняє кожен$A \in \Gamma^*$, який не містить$\eq[][]$ (а отже, і все$A \in \Gamma$). Він не працює, однак, якщо він$\eq[][]$ присутній. Причина полягає в тому, що$\Gamma^*$ тоді може містити речення$\eq[t][t']$, але в моделі терміна значення будь-якого терміна - це сам термін. Отже, якщо$t$ і$t'$ є різними термінами, їх значення в терміні модель - тобто,$t$ і$t'$, відповідно, - різні, і тому$\eq[t][t']$ є помилковими. Ми можемо виправити це, однак, використовуючи конструкцію, відому як «факторинг».

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

$\Gamma^*$Дозволяти бути послідовним і повним набором пропозицій в$\Lang L$. Визначаємо відношення$\approx$ на множині закритих термінів$\Lang L$ по\[t \approx t' \quad\text{ iff }\quad \eq[t][t'] \in \Gamma^*\nonumber\]

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

Співвідношення$\approx$ має такі властивості:

$\approx$є рефлексивним.
$\approx$симетрична.
$\approx$є перехідним.
Якщо$t \approx t'$,$f$ є символом функції, і,...$t_1$,,,,,$t_{i-1}$,,$t_{i+1}$,,,,$t_n$ є термінами, то\[\Atom{f}{t_1,\dots, t_{i-1}, t, t_{i+1}, \dots, t_n} \approx \Atom{f}{t_1,\dots, t_{i-1}, t', t_{i+1}, \dots, t_n}.\nonumber\]
Якщо$t \approx t'$,$R$ є присудком символ, і,...,$t_1$,,,,,$t_{i-1}$,$t_{i+1}$,,,,$t_n$ є термінами, то\[\begin{gathered} \Atom{R}{t_1,\dots, t_{i-1}, t, t_{i+1}, \dots, t_n} \in \Gamma^* \text{ iff } \\ \Atom{R}{t_1,\dots, t_{i-1}, t', t_{i+1}, \dots, t_n} \in \Gamma^*.\end{gathered}\]

Доказ. Оскільки$\Gamma^*$ є послідовним і повним,$\eq[t][t'] \in \Gamma^*$ iff$\Gamma^* \Proves \eq[t][t']$. При цьому досить показати наступне:

$\Gamma^* \Proves \eq[t][t]$на всі терміни$t$.
Якщо$\Gamma^* \Proves \eq[t][t']$ тоді$\Gamma^* \Proves \eq[t'][t]$.
Якщо$\Gamma^* \Proves \eq[t][t']$ і$\Gamma^* \Proves \eq[t'][t'']$, то$\Gamma^* \Proves \eq[t][t'']$.
Якщо$\Gamma^* \Proves \eq[t][t']$, то\[\Gamma^* \Proves \eq[\Atom{f}{t_1,\dots,t_{i-1},t,t_{i+1},,\dots,t_n}][\Atom{f}{t_1,\dots,t_{i-1},t',t_{i+1},\dots,t_n}]\nonumber\] для кожного$n$ -place функція символ$f$ і терміни$t_1$,...,$t_{i-1}$,$t_{i+1}$,...,$t_n$.
Якщо$\Gamma^* \Proves \eq[t][t']$ і$\Gamma^* \Proves \Atom{R}{t_1,\dots,t_{i-1},t,t_{i+1},\dots,t_n}$, то$\Gamma^* \Proves \Atom{R}{t_1,\dots,t_{i-1},t',t_{i+1},\dots,t_n}$ для кожного$n$ -місця присудок символ$R$ і терміни$t_1$,...,$t_{i-1}$,$t_{i+1}$,...,$t_n$.

◻

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

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

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

Припустимо,$\Gamma^*$ є послідовним і повним набором в мові$\Lang L$,$t$ є терміном, і$\approx$ як в попередньому визначенні. Потім:\[\equivrep{t}{\approx} = \Setabs{t'}{t'\in \Trm[L], t \approx t'}\nonumber\] і$\equivclass{\Trm[L]}{\approx} = \Setabs{\equivrep{t}{\approx}}{t \in \Trm[L]}$.

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

Дозвольте$\Struct M = \Struct M(\Gamma^*)$ бути терміном модель для$\Gamma^*$. Далі$\Struct{\equivclass{M}{\approx}}$ йде наступна структура:

$\Domain{\equivclass{M}{\approx}} = \equivclass{\Trm[L]}{\approx}$.
$\Assign{c}{\equivclass{M}{\approx}} = \equivrep{c}{\approx}$
$\Assign{f}{\equivclass{M}{\approx}}(\equivrep{t_1}{\approx}, \dots, \equivrep{t_n}{\approx}) = \equivrep{\Atom{f}{t_1,\dots, t_n}}{\approx}$
$\tuple{\equivrep{t_1}{\approx}, \dots, \equivrep{t_n}{\approx}} \in \Assign{R}{\equivclass{M}{\approx}}$іфф$\Sat{M}{\Atom{R}{t_1,\dots, t_n}}$.

Зверніть увагу, що ми визначили$\Assign{f}{\equivclass{M}{\approx}}$ і$\Assign{R}{\equivclass{M}{\approx}}$ для елементів,$\equivclass{\Trm[L]}{\approx}$ посилаючись на них як$\equivrep{t}{\approx}$, тобто через представників$t \in \equivrep{t}{\approx}$. Ми повинні переконатися, що ці визначення не залежать від вибору цих представників, тобто, що для деяких інших варіантів,$t'$ які визначають ті ж класи еквівалентності ($\equivrep{t}{\approx} = \equivrep{t'}{\approx}$), визначення дають той самий результат. Наприклад, якщо$R$ є одномісним присудком символ, останнє речення визначення говорить, що$\equivrep{t}{\approx} \in \Assign{R}{\equivclass{M}{\approx}}$ iff$\Sat{M}{\Atom{R}{t}}$. Якщо для якогось іншого терміну$t'$ з$t \approx t'$$\SatN{M}{\Atom{R}{t}}$, то визначення вимагатиме$\equivrep{t'}{\approx} \notin \Assign{R}{\equivclass{M}{\approx}}$. Якщо$t \approx t'$, то$\equivrep{t}{\approx} = \equivrep{t'}{\approx}$, але ми не можемо мати обох$\equivrep{t}{\approx} \in \Assign{R}{\equivclass{M}{\approx}}$ і$\equivrep{t}{\approx} \notin \Assign{R}{\equivclass{M}{\approx}}$. Однак Пропозиція$\PageIndex{1}$ гарантує, що цього не може статися.

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

$\Struct{\equivclass{M}{\approx}}$чітко визначені, тобто якщо,...,$t_1$,,,,$t_n$,,$t_1'$,,,,$t_n'$ є термінами, а$t_i \approx t_i'$ потім

$\equivrep{\Atom{f}{t_1,\dots, t_n}}{\approx} = \equivrep{\Atom{f}{t_1',\dots, t_n'}}{\approx}$, т. Е\[\Atom{f}{t_1,\dots, t_n} \approx \Atom{f}{t_1',\dots, t_n'}\nonumber\].
$\Sat{M}{\Atom{R}{t_1,\dots, t_n}}$якщо$\Sat{M}{\Atom{R}{t_1',\dots, t_n'}}$, т. Е.\[\Atom{R}{t_1,\dots, t_n} \in \Gamma^* \text{ iff } \Atom{R}{t_1',\dots, t_n'} \in \Gamma^*.\nonumber\]

Доказ. Випливає з Пропозиції$\PageIndex{1}$ шляхом індукції на$n$. ◻

Лемма$\PageIndex{1}$

$\Sat{\equivclass{M}{\approx}}{A}$iff$A \in \Gamma^*$ для всіх речень$A$.

Доказ. За індукцією$A$, так само, як на доказі Лемми$\PageIndex{1}$. Єдиний випадок, який потребує додаткової уваги - це коли$A \ident \eq[t][t']$. \[\begin{aligned} \Sat{\equivclass{M}{\approx}}{\eq[t][t']} & \text{ iff } \equivrep{t}{\approx} = \equivrep{t'}{\approx} \text{ (by definition of $\Struct{\equivclass{M}{\approx}}$)}\\ & \text{ iff } t \approx t' \text{ (by definition of $\equivrep{t}{\approx}$)}\\ & \text{ iff } \eq[t][t'] \in \Gamma^* \text{ (by definition of $\approx$).}\end{aligned}\]◻

Зверніть увагу, що$\Struct{M(\Gamma^*)}$ while завжди перелічуваний і нескінченний,$\Struct{\equivclass{M}{\approx}}$ може бути кінцевим, так як може виявитися, що класів тільки скінченно багато$\equivrep{t}{\approx}$. Цього слід очікувати, оскільки$\Gamma$ може містити речення, які вимагають будь-якої структури, в якій вони істинні, щоб бути кінцевими. Наприклад,$\lforall{x}{\lforall{y}{x = y}}$ є послідовним реченням, але задовольняється лише структурами з доменом, який містить рівно один елемент.