5.6: Subfórmulas
- Page ID
- 103684
\( \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}\)A menudo es útil hablar de las fórmulas que “conforman” una fórmula dada. A estos los llamamos sus subfórmulas. Cualquier fórmula cuenta como una subfórmula de sí misma; una subfórmula\(A\) distinta de\(A\) sí misma es una subfórmula apropiada.
Definición\(\PageIndex{1}\): Immediate Subformula
Si\(A\) es una fórmula, las subfórmulas inmediatas de\(A\) se definen inductivamente de la siguiente manera:
-
Las fórmulas atómicas no tienen subfórmulas inmediatas.
-
\(\indcase{A}{\lnot B}\)La única subfórmula inmediata de\(\indfrm\) es\(B\).
-
\(\indcase{A}{(B \ast C)}\)Las subfórmulas inmediatas de\(\indfrm\) son\(B\) y\(C\) (\(\ast\)es cualquiera de las conectivas de dos lugares).
-
\(\indcase{A}{\lforall{x}{B}}\)La única subfórmula inmediata de\(\indfrm\) es\(B\).
-
\(\indcase{A}{\lexists{x}{B}}\)La única subfórmula inmediata de\(\indfrm\) es\(B\).
Definición\(\PageIndex{2}\): Proper Subformula
Si\(A\) es una fórmula, las subfórmulas adecuadas de\(A\) son recursivamente como sigue:
-
Las fórmulas atómicas no tienen subfórmulas adecuadas.
-
\(\indcase{A}{\lnot B}\)Las subfórmulas adecuadas de\(\indfrm\) están\(B\) junto con todas las subfórmulas adecuadas de\(B\).
-
\(\indcase{A}{(B \ast C)}\)Las subfórmulas propias de\(\indfrm\) son\(B\)\(C\), junto con todas las subfórmulas propias de\(B\) y las de\(C\).
-
\(\indcase{A}{\lforall{x}{B}}\)Las subfórmulas adecuadas de\(\indfrm\) están\(B\) junto con todas las subfórmulas adecuadas de\(B\).
-
\(\indcase{A}{\lexists{x}{B}}\)Las subfórmulas adecuadas de\(\indfrm\) están\(B\) junto con todas las subfórmulas adecuadas de\(B\).
Definición\(\PageIndex{3}\): Subformula
Las subfórmulas de\(A\) son\(A\) en sí mismas junto con todas sus subfórmulas propias.
Observe la sutil diferencia en cómo hemos definido las subfórmulas inmediatas y las subfórmulas adecuadas. En el primer caso, hemos definido directamente las subfórmulas inmediatas de una fórmula\(A\) para cada forma posible de\(A\). Es una definición explícita por casos, y los casos reflejan la definición inductiva del conjunto de fórmulas. En el segundo caso, también hemos espejado la forma en que se define el conjunto de todas las fórmulas, pero en cada caso también hemos incluido las subfórmulas propias de las fórmulas más pequeñas\(B\),\(C\) además de estas fórmulas mismas. Esto hace que la definición sea recursiva. En general, una definición de una función sobre un conjunto definido inductivamente (en nuestro caso, fórmulas) es recursiva si los casos en la definición de la función hacen uso de la función misma. Para estar bien definidos, debemos asegurarnos, sin embargo, de que solo usamos los valores de la función para argumentos que vienen “antes” del que estamos definiendo, en nuestro caso, al definir “subfórmula apropiada” porque solo\((B \ast C)\) usamos las subfórmulas adecuadas de las fórmulas “anteriores” \(B\)y\(C\).