10.7: Identidad

Última actualización
Guardar como PDF

Page ID: 103586

$ \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}}$$\newcommand{\AA}{\unicode[.8,0]{x212B}}$

Template:MathJaxZach

La construcción del término modelo dado en la sección anterior es suficiente para establecer la integridad de la lógica de primer orden para conjuntos$\Gamma$ que no contienen$\eq[][]$. El término modelo satisface todo$A \in \Gamma^*$ lo que no contiene$\eq[][]$ (y por lo tanto todos$A \in \Gamma$). No funciona, sin embargo, si$\eq[][]$ está presente. El motivo es que$\Gamma^*$ entonces puede contener una frase$\eq[t][t']$, pero en el término modelo el valor de cualquier término es ese término en sí mismo. De ahí que si$t$ y$t'$ son términos diferentes, sus valores en el modelo de términos —es decir,$t$ y$t'$, respectivamente— son diferentes, y por lo tanto$\eq[t][t']$ es falso. Podemos arreglar esto, sin embargo, usando una construcción conocida como “factoring”.

Definición$\PageIndex{1}$

$\Gamma^*$Sea un conjunto consistente y completo de oraciones en$\Lang L$. Definimos la relación$\approx$ en el conjunto de términos cerrados de$\Lang L$ por\[t \approx t' \quad\text{ iff }\quad \eq[t][t'] \in \Gamma^*\nonumber\]

Proposición$\PageIndex{1}$

La relación$\approx$ tiene las siguientes propiedades:

$\approx$es reflexivo.
$\approx$es simétrico.
$\approx$es transitivo.
Si$t \approx t'$,$f$ es un símbolo de función, y$t_1$,...,$t_{i-1}$,$t_{i+1}$,...,$t_n$ son términos, entonces\[\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\]
Si$t \approx t'$,$R$ es un símbolo predicado, y$t_1$,...,$t_{i-1}$,$t_{i+1}$,...,$t_n$ son términos, entonces\[\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}\]

Comprobante. Ya que$\Gamma^*$ es consistente y completo,$\eq[t][t'] \in \Gamma^*$ iff$\Gamma^* \Proves \eq[t][t']$. Por lo tanto, basta con mostrar lo siguiente:

$\Gamma^* \Proves \eq[t][t]$para todos los términos$t$.
Si$\Gamma^* \Proves \eq[t][t']$ entonces$\Gamma^* \Proves \eq[t'][t]$.
Si$\Gamma^* \Proves \eq[t][t']$ y$\Gamma^* \Proves \eq[t'][t'']$, entonces$\Gamma^* \Proves \eq[t][t'']$.
Si$\Gamma^* \Proves \eq[t][t']$, entonces\[\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\] para cada$n$ -lugar función símbolo$f$ y términos$t_1$,...,$t_{i-1}$,$t_{i+1}$,...,$t_n$.
Si$\Gamma^* \Proves \eq[t][t']$ y$\Gamma^* \Proves \Atom{R}{t_1,\dots,t_{i-1},t,t_{i+1},\dots,t_n}$, entonces$\Gamma^* \Proves \Atom{R}{t_1,\dots,t_{i-1},t',t_{i+1},\dots,t_n}$ para cada$n$ -lugar símbolo predicado$R$ y términos$t_1$,...,$t_{i-1}$,$t_{i+1}$,...,$t_n$.

◻

Problema$\PageIndex{1}$

Completar el comprobante de Proposición$\PageIndex{1}$.

Definición$\PageIndex{2}$

Supongamos que$\Gamma^*$ es un conjunto consistente y completo en un idioma$\Lang L$,$t$ es un término, y$\approx$ como en la definición anterior. Entonces:\[\equivrep{t}{\approx} = \Setabs{t'}{t'\in \Trm[L], t \approx t'}\nonumber\] y$\equivclass{\Trm[L]}{\approx} = \Setabs{\equivrep{t}{\approx}}{t \in \Trm[L]}$.

Definición$\PageIndex{3}$

Deje$\Struct M = \Struct M(\Gamma^*)$ ser el término modelo para$\Gamma^*$. Entonces$\Struct{\equivclass{M}{\approx}}$ está la siguiente estructura:

$\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}}$iff$\Sat{M}{\Atom{R}{t_1,\dots, t_n}}$.

Obsérvese que hemos definido$\Assign{f}{\equivclass{M}{\approx}}$ y$\Assign{R}{\equivclass{M}{\approx}}$ para elementos de$\equivclass{\Trm[L]}{\approx}$ al referirse a ellos como$\equivrep{t}{\approx}$, es decir, vía representantes$t \in \equivrep{t}{\approx}$. Tenemos que asegurarnos de que estas definiciones no dependan de la elección de estos representantes, es decir, que para algunas otras elecciones$t'$ que determinan las mismas clases de equivalencia ($\equivrep{t}{\approx} = \equivrep{t'}{\approx}$), las definiciones arrojan el mismo resultado. Por ejemplo, si$R$ es un símbolo de predicado de un solo lugar, la última cláusula de la definición dice que$\equivrep{t}{\approx} \in \Assign{R}{\equivclass{M}{\approx}}$ iff$\Sat{M}{\Atom{R}{t}}$. Si por algún otro término$t'$ con$t \approx t'$,$\SatN{M}{\Atom{R}{t}}$, entonces la definición requeriría$\equivrep{t'}{\approx} \notin \Assign{R}{\equivclass{M}{\approx}}$. Si$t \approx t'$, entonces$\equivrep{t}{\approx} = \equivrep{t'}{\approx}$, pero no podemos tener ambos$\equivrep{t}{\approx} \in \Assign{R}{\equivclass{M}{\approx}}$ y$\equivrep{t}{\approx} \notin \Assign{R}{\equivclass{M}{\approx}}$. No obstante, la Proposición$\PageIndex{1}$ garantiza que esto no puede suceder.

Proposición$\PageIndex{2}$

$\Struct{\equivclass{M}{\approx}}$está bien definido, es decir, si$t_1$,...,$t_n$,$t_1'$,...,$t_n'$ son términos, y$t_i \approx t_i'$ entonces

$\equivrep{\Atom{f}{t_1,\dots, t_n}}{\approx} = \equivrep{\Atom{f}{t_1',\dots, t_n'}}{\approx}$, es decir,\[\Atom{f}{t_1,\dots, t_n} \approx \Atom{f}{t_1',\dots, t_n'}\nonumber\] y
$\Sat{M}{\Atom{R}{t_1,\dots, t_n}}$iff$\Sat{M}{\Atom{R}{t_1',\dots, t_n'}}$, es decir,\[\Atom{R}{t_1,\dots, t_n} \in \Gamma^* \text{ iff } \Atom{R}{t_1',\dots, t_n'} \in \Gamma^*.\nonumber\]

Comprobante. Se desprende de la Proposición$\PageIndex{1}$ por inducción en$n$. ◻

Lema$\PageIndex{1}$

$\Sat{\equivclass{M}{\approx}}{A}$iff$A \in \Gamma^*$ para todas las oraciones$A$.

Comprobante. Por inducción en$A$, al igual que en la prueba de Lemma$\PageIndex{1}$. El único caso que necesita atención adicional es cuándo$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}\]◻

Obsérvese que si bien$\Struct{M(\Gamma^*)}$ es siempre enumerable e infinito,$\Struct{\equivclass{M}{\approx}}$ puede ser finito, ya que puede resultar que sólo hay finitamente muchas clases$\equivrep{t}{\approx}$. Esto es de esperarse, ya que$\Gamma$ pueden contener frases que requieran que cualquier estructura en la que sean verdaderas sea finita. Por ejemplo,$\lforall{x}{\lforall{y}{x = y}}$ es una oración consistente, pero se satisface sólo en estructuras con un dominio que contiene exactamente un elemento.