10.7: Identidad
- 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}}\)
\( \newcommand{\vectorA}[1]{\vec{#1}} % arrow\)
\( \newcommand{\vectorAt}[1]{\vec{\text{#1}}} % arrow\)
\( \newcommand{\vectorB}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)
\( \newcommand{\vectorC}[1]{\textbf{#1}} \)
\( \newcommand{\vectorD}[1]{\overrightarrow{#1}} \)
\( \newcommand{\vectorDt}[1]{\overrightarrow{\text{#1}}} \)
\( \newcommand{\vectE}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash{\mathbf {#1}}}} \)
\( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)
\( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)
\(\newcommand{\avec}{\mathbf a}\) \(\newcommand{\bvec}{\mathbf b}\) \(\newcommand{\cvec}{\mathbf c}\) \(\newcommand{\dvec}{\mathbf d}\) \(\newcommand{\dtil}{\widetilde{\mathbf d}}\) \(\newcommand{\evec}{\mathbf e}\) \(\newcommand{\fvec}{\mathbf f}\) \(\newcommand{\nvec}{\mathbf n}\) \(\newcommand{\pvec}{\mathbf p}\) \(\newcommand{\qvec}{\mathbf q}\) \(\newcommand{\svec}{\mathbf s}\) \(\newcommand{\tvec}{\mathbf t}\) \(\newcommand{\uvec}{\mathbf u}\) \(\newcommand{\vvec}{\mathbf v}\) \(\newcommand{\wvec}{\mathbf w}\) \(\newcommand{\xvec}{\mathbf x}\) \(\newcommand{\yvec}{\mathbf y}\) \(\newcommand{\zvec}{\mathbf z}\) \(\newcommand{\rvec}{\mathbf r}\) \(\newcommand{\mvec}{\mathbf m}\) \(\newcommand{\zerovec}{\mathbf 0}\) \(\newcommand{\onevec}{\mathbf 1}\) \(\newcommand{\real}{\mathbb R}\) \(\newcommand{\twovec}[2]{\left[\begin{array}{r}#1 \\ #2 \end{array}\right]}\) \(\newcommand{\ctwovec}[2]{\left[\begin{array}{c}#1 \\ #2 \end{array}\right]}\) \(\newcommand{\threevec}[3]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \end{array}\right]}\) \(\newcommand{\cthreevec}[3]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \end{array}\right]}\) \(\newcommand{\fourvec}[4]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}\) \(\newcommand{\cfourvec}[4]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}\) \(\newcommand{\fivevec}[5]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}\) \(\newcommand{\cfivevec}[5]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}\) \(\newcommand{\mattwo}[4]{\left[\begin{array}{rr}#1 \amp #2 \\ #3 \amp #4 \\ \end{array}\right]}\) \(\newcommand{\laspan}[1]{\text{Span}\{#1\}}\) \(\newcommand{\bcal}{\cal B}\) \(\newcommand{\ccal}{\cal C}\) \(\newcommand{\scal}{\cal S}\) \(\newcommand{\wcal}{\cal W}\) \(\newcommand{\ecal}{\cal E}\) \(\newcommand{\coords}[2]{\left\{#1\right\}_{#2}}\) \(\newcommand{\gray}[1]{\color{gray}{#1}}\) \(\newcommand{\lgray}[1]{\color{lightgray}{#1}}\) \(\newcommand{\rank}{\operatorname{rank}}\) \(\newcommand{\row}{\text{Row}}\) \(\newcommand{\col}{\text{Col}}\) \(\renewcommand{\row}{\text{Row}}\) \(\newcommand{\nul}{\text{Nul}}\) \(\newcommand{\var}{\text{Var}}\) \(\newcommand{\corr}{\text{corr}}\) \(\newcommand{\len}[1]{\left|#1\right|}\) \(\newcommand{\bbar}{\overline{\bvec}}\) \(\newcommand{\bhat}{\widehat{\bvec}}\) \(\newcommand{\bperp}{\bvec^\perp}\) \(\newcommand{\xhat}{\widehat{\xvec}}\) \(\newcommand{\vhat}{\widehat{\vvec}}\) \(\newcommand{\uhat}{\widehat{\uvec}}\) \(\newcommand{\what}{\widehat{\wvec}}\) \(\newcommand{\Sighat}{\widehat{\Sigma}}\) \(\newcommand{\lt}{<}\) \(\newcommand{\gt}{>}\) \(\newcommand{\amp}{&}\) \(\definecolor{fillinmathshade}{gray}{0.9}\)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\]
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]}\).
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\). ◻
\(\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.