5.13: Extensionalidad
- Page ID
- 103691
\( \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 extensionalidad, a veces llamada relevancia, puede expresarse de manera informal de la siguiente manera: los únicos factores que inciden\(A\) en la satisfacción de la fórmula en una estructura\(\Struct M\) relativa a una asignación variable\(s\), son el tamaño del dominio y las asignaciones hecho por\(\Struct M\) y\(s\) a los elementos del lenguaje que realmente aparecen en\(A\).
Una consecuencia inmediata de la extensionalidad es que donde dos estructuras\(\Struct M\) y\(\Struct M'\) coinciden en todos los elementos de la lengua que aparecen en una oración\(A\) y tienen el mismo dominio,\(\Struct M\) y también\(\Struct M'\) deben acordar sea o no\(A\) en sí mismo cierto.
Proposición\(\PageIndex{1}\): Extensionality
Dejar\(A\) ser una fórmula,\(\Struct M_1\) y\(\Struct M_2\) ser estructuras con\(\Domain{M_1} = \Domain{M_2}\), y\(s\) una asignación variable en\(\Domain{M_1} = \Domain{M_2}\). Si\(\Assign{c}{M_1} = \Assign{c}{M_2}\),\(\Assign{R}{M_1}=\Assign{R}{M_2}\), y\(\Assign{f}{M_1} = \Assign{f}{M_2}\) para cada símbolo constante\(c\), símbolo de relación y símbolo\(R\) de función\(f\) que ocurra en\(A\), entonces\(\Sat[,s]{M_1}{A}\) iff \(\Sat[,s]{M_2}{A}\).
Comprobante. Primero probar (por inducción sobre\(t\)) que para cada término,\(\Value[s]{t}{M_1} = \Value[s]{t}{M_2}\). Luego probar la proposición por inducción sobre\(A\), haciendo uso de la afirmación recién probada para la base de inducción (donde\(A\) es atómica) . ◻
Problema\(\PageIndex{1}\)
Llevar a cabo el comprobante de Proposición a\(\PageIndex{1}\) detalle.
Corolario\(\PageIndex{1}\): Extensionality for Sentences
Que\(A\) sea una oración y\(\Struct{M_1}\),\(\Struct{M_2}\) como en Proposición\(\PageIndex{1}\). Después\(\Sat{M_1}{A}\) iff\(\Sat{M_2}{A}\).
Comprobante. Se desprende de la Proposición\(\PageIndex{1}\) por Corolario 5.12.1. ◻
Además, el valor de un término, y si una estructura satisface o no una fórmula, sólo depende de los valores de sus subtérminos.
Dejar\(\Struct M\) ser una estructura,\(t\) y\(t'\) términos, y\(s\) una asignación variable. Dejar\(\varAssign{s'}{s}{x}\) ser la\(x\) -variante de\(s\) dada por\(s'(x) = \Value[s]{t'}{M}\). Entonces\(\Value[s]{\Subst{t}{t'}{x}}{M} = \Value[s']{t}{M}\).
Comprobante. Por inducción en\(t\).
-
Si\(t\) es una constante, digamos,\(t\ident c\), entonces\(\Subst{t}{t'}{x} = c\), y\(\Value[s]{c}{M} = \Assign{c}{M} = \Value[s']{c}{M}\).
-
Si\(t\) es una variable distinta a\(x\), digamos,\(t \ident y\), entonces\(\Subst{t}{t'}{x} = y\), y\(\Value[s]{y}{M} = \Value[s']{y}{M}\) desde entonces\(\varAssign{s'}{s}{x}\).
-
Si\(t \ident x\), entonces\(\Subst{t}{t'}{x} = t'\). Pero\(\Value[s']{x}{M} = \Value[s]{t'}{M}\) por definición de\(s'\).
-
Si\(t \ident \Atom{f}{t_1,\dots,t_n}\) entonces tenemos:\[\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}\]
◻
\(\Struct M\)Sea una estructura,\(A\) una fórmula,\(t\) un término y\(s\) una asignación de variables. Dejar\(\varAssign{s'}{s}{x}\) ser la\(x\) -variante de\(s\) dada por\(s'(x) = \Value[s]{t}{M}\). Después\(\Sat[,s]{M}{\Subst{A}{t}{x}}\) iff\(\Sat[,s']{M}{A}\).
Comprobante. Ejercicio. ◻
Problema\(\PageIndex{2}\)
Probar Proposición\(\PageIndex{3}\).