Saltar al contenido principal

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

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:

1. $$\approx$$es reflexivo.

2. $$\approx$$es simétrico.

3. $$\approx$$es transitivo.

4. 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$

5. 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:

1. $$\Gamma^* \Proves \eq[t][t]$$para todos los términos$$t$$.

2. Si$$\Gamma^* \Proves \eq[t][t']$$ entonces$$\Gamma^* \Proves \eq[t'][t]$$.

3. Si$$\Gamma^* \Proves \eq[t][t']$$ y$$\Gamma^* \Proves \eq[t'][t'']$$, entonces$$\Gamma^* \Proves \eq[t][t'']$$.

4. 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$$.

5. 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:

1. $$\Domain{\equivclass{M}{\approx}} = \equivclass{\Trm[L]}{\approx}$$.

2. $$\Assign{c}{\equivclass{M}{\approx}} = \equivrep{c}{\approx}$$

3. $$\Assign{f}{\equivclass{M}{\approx}}(\equivrep{t_1}{\approx}, \dots, \equivrep{t_n}{\approx}) = \equivrep{\Atom{f}{t_1,\dots, t_n}}{\approx}$$

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

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

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

This page titled 10.7: Identidad is shared under a CC BY license and was authored, remixed, and/or curated by Richard Zach et al. (Open Logic Project) .