Sustitución (lógica)

Una sustitución es una transformación sintáctica de expresiones formales . Aplicar una sustitución a una expresión significa reemplazar de forma consistente sus símbolos variables o marcadores de posición por otras expresiones.

La expresión resultante se denomina instancia de sustitución , o simplemente instancia , de la expresión original.

Lógica proposicional

Definición

Donde ψ y φ representan fórmulas de lógica proposicional , ψ es una instancia de sustitución de φ si y solo si ψ puede obtenerse a partir de φ sustituyendo fórmulas por variables proposicionales en φ , reemplazando cada ocurrencia de la misma variable por una ocurrencia de la misma fórmula. Por ejemplo:

ψ: (R → S) y (T → S)

es una instancia de sustitución de

φ: P y Q

Es decir, ψ se puede obtener reemplazando P y Q en φ con (R → S) y (T → S) respectivamente. De manera similar:

ψ: (A ↔ A) ↔ (A ↔ A)

es una instancia de sustitución de:

φ: (A ↔ A)

ya que ψ se puede obtener reemplazando cada A en φ con (A ↔ A).

En algunos sistemas de deducción para la lógica proposicional, se puede introducir una nueva expresión (una proposición ) en una línea de una derivación si se trata de una instancia de sustitución de una línea anterior de la misma. ^{[ 1 ]} Así es como se introducen nuevas líneas en algunos sistemas axiomáticos . En los sistemas que utilizan reglas de transformación , una regla puede incluir el uso de una instancia de sustitución con el fin de introducir ciertas variables en una derivación.

Tautologías

Una fórmula proposicional es una tautología si es verdadera bajo cualquier valoración (o interpretación ) de sus símbolos predicativos. Si Φ es una tautología y Θ es una instancia de sustitución de Φ, entonces Θ también es una tautología. Este hecho implica la validez de la regla de deducción descrita en la sección anterior.

Lógica de primer orden

En lógica de primer orden , una sustitución es una aplicación total $σ : V \to T$ de variables a términos ; muchos, ^{[ 2 ]}^{: 73}^{[ 3 ]}^{: 445} pero no todos ^{[ 4 ]}^{: 250} autores requieren además σ ( x ) = x para todas las variables x excepto un número finito de ellas . La notación { x ₁↦ t ₁, …, x _k ↦ t _k } ^[^{nota 1}^] se refiere a una sustitución que asigna a cada variable x _i el término correspondiente t _i , para i =1,…, k , y a cada otra variable consigo misma; los x _i deben ser distintos entre sí. La mayoría de los autores requieren además que cada término t _i sea sintácticamente diferente de x _i , para evitar infinitas notaciones distintas para la misma sustitución. Aplicar esa sustitución a un término t se escribe en notación posfija como t { x ₁↦ t ₁, ..., x _k ↦ t _k } ; significa reemplazar (simultáneamente) cada ocurrencia de cada x _i en t por t _i . ^[^{nota 2}^] El resultado tσ de aplicar una sustitución σ a un término t se llama una instancia de ese término t . Por ejemplo, aplicar la sustitución { x ↦ z , z ↦ h ( a , y ) } al término

El dominio dom ( σ ) de una sustitución σ se define comúnmente como el conjunto de variables realmente reemplazadas, es decir, dom ( σ ) = { x ∈ V | xσ ≠ x } . Una sustitución se llama sustitución base si asigna todas las variables de su dominio a términos base , es decir, libres de variables. La instancia de sustitución tσ de una sustitución base es un término base si todas las variables de t están en el dominio de σ, es decir, si vars ( t ) ⊆ dom ( σ ) . Una sustitución σ se llama sustitución lineal si tσ es un término lineal para algún (y por lo tanto todo) término lineal t que contiene precisamente las variables del dominio de σ , es decir, con vars ( t ) = dom ( σ ). Una sustitución σ se llama sustitución plana si xσ es una variable para cada variable x . Una sustitución σ se denomina sustitución de renombramiento si es una permutación del conjunto de todas las variables. Al igual que toda permutación, una sustitución de renombramiento σ siempre tiene una sustitución inversa σ ⁻¹ , tal que tσσ ⁻¹ = t = tσ ⁻¹σ para cada término t . Sin embargo, no es posible definir una inversa para una sustitución arbitraria.

Por ejemplo, { x ↦ 2, y ↦ 3+4 } es una sustitución básica, { x ↦ x ₁, y ↦ y ₂+4 } no es básica ni plana, pero sí lineal, { x ↦ y ₂, y ↦ y ₂+4 } no es lineal ni plana, { x ↦ y ₂, y ↦ y ₂} es plana, pero no lineal, { x ↦ x ₁, y ↦ y ₂} es lineal y plana, pero no es un cambio de nombre, ya que asigna tanto y como y ₂ a y ₂ ; cada una de estas sustituciones tiene el conjunto { x , y } como su dominio. Un ejemplo de sustitución de renombramiento es { x ↦ x ₁, x ₁↦ y , y ↦ y ₂, y ₂↦ x } , tiene la inversa { x ↦ y ₂, y ₂↦ y , y ↦ x ₁, x ₁↦ x } . La sustitución plana { x ↦ z , y ↦ z } no puede tener una inversa, ya que eg ( x + y ) { x ↦ z , y ↦ z } = z + z , y el último término no se puede transformar de nuevo a x + y , ya que se pierde la información sobre el origen del que proviene a z . La sustitución básica { x ↦ 2 } no puede tener una inversa debido a una pérdida similar de información de origen eg en ( x +2) { x ↦ 2 } = 2+2, incluso si se permitiera reemplazar constantes por variables mediante algún tipo ficticio de "sustituciones generalizadas".

Dos sustituciones se consideran iguales si asignan a cada variable términos de resultado sintácticamente iguales , formalmente: σ = τ si xσ = xτ para cada variable x ∈ V. La composición de dos sustituciones σ = { x ₁↦ t ₁, …, x _k ↦ t _k } y τ = { y ₁↦ u ₁, …, y _l ↦ u _l } se obtiene eliminando de la sustitución { x ₁↦ t ₁τ , …, x _k ↦ t _k τ , y ₁↦ u ₁, …, y _l ↦ u _l } aquellos pares y _i ↦ u _i para los cuales y _i ∈ { x ₁, …, x _k } . La composición de σ y τ se denota por στ . La composición es una operación asociativa y es compatible con la aplicación de sustitución, es decir, ( ρσ ) τ = ρ ( στ ) y ( tσ ) τ = t ( στ ), respectivamente, para cada sustitución ρ , σ , τ y cada término t . La sustitución identidad , que asigna a cada variable su propia variable, es el elemento neutro de la composición de sustitución. Una sustitución σ se denomina idempotente si σσ = σ , y por lo tanto tσσ = tσ para cada término t . Cuando x _i ≠ t _i para todo i , la sustitución { x ₁↦ t ₁, …, x _k} ↦ t _k } es idempotente si y solo si ninguna de las variables x _i aparece en ningún t _j . La composición por sustitución no es conmutativa, es decir, στ puede ser diferente de τσ , incluso si σ y τ son idempotentes. ^[²^]^:^73–74^[³^]^:^445–446

Por ejemplo, { x ↦ 2, y ↦ 3+4 } es igual a { y ↦ 3+4, x ↦ 2 } , pero diferente de { x ↦ 2, y ↦ 7 } . La sustitución { x ↦ y + y } es idempotente, por ejemplo (( x + y ) { x ↦ y + y } ) { x ↦ y + y } = (( y + y )+ y ) { x ↦ y + y } = ( y + y )+ y , mientras que la sustitución { x ↦ x + y } no es idempotente, por ejemplo (( x + y ) { x ↦ x + y } ) { x ↦ x + y } = (( x + y )+ y ) { x ↦ x + y } = (( x + y )+ y )+ y . Un ejemplo de sustituciones no conmutativas es { x ↦ y } { y ↦ z } = { x ↦ z , y ↦ z } , pero { y ↦ z } { x ↦ y } = { x ↦ y , y ↦ z } .

Matemáticas

En matemáticas , existen dos usos comunes de la sustitución: la sustitución de variables por constantes (también llamada asignación para esa variable) y la propiedad de sustitución de la igualdad , ^{[ 5 ]} también llamada Ley de Leibniz . ^{[ 6 ]}

Considerando las matemáticas como un lenguaje formal , una variable es un símbolo de un alfabeto , generalmente una letra como $x$ , $y$ y $z$ , que denota un rango de valores posibles . ^{[ 7 ]} Si una variable es libre en una expresión o fórmula dada , entonces puede reemplazarse por cualquiera de los valores en su rango. ^{[ 8 ]} Ciertos tipos de variables ligadas también pueden sustituirse. Por ejemplo, los parámetros de una expresión (como los coeficientes de un polinomio ) o el argumento de una función . Además, las variables cuantificadas universalmente pueden reemplazarse por cualquiera de los valores en su rango, y el resultado será una afirmación verdadera . (Esto se llama instanciación universal ).

Para un lenguaje no formalizado, es decir, en la mayoría de los textos matemáticos fuera de la lógica matemática , para una expresión individual no siempre es posible identificar qué variables son libres y cuáles están ligadas. Por ejemplo, en ${\textstyle \sum _ {i<k}a_ {ik}}$ , dependiendo del contexto, la variable ${\textstyle i}$ puede ser gratis y ${\textstyle k}$ ligados, o viceversa, pero no pueden ser ambos libres. Determinar qué valor se supone libre depende del contexto y la semántica .

La propiedad de sustitución de la igualdad , o Ley de Leibniz (aunque este último término suele reservarse para contextos filosóficos ), establece generalmente que, si dos cosas son iguales, entonces cualquier propiedad de una debe ser propiedad de la otra. Se puede expresar formalmente en notación lógica como: $(a=b)\implies {\bigl [}\phi (a)\Rightarrow \phi (b){\bigr ]}$ Por cada ${\textstyle a}$ y ${\textstyle b}$ y cualquier fórmula bien formada ${\textstyle \phi (x)}$ (con una variable libre x). Por ejemplo: Para todos los números reales $a$ y $b$ , si $a = b$ , entonces $a \geq 0$ implica $b \geq 0$ (aquí, $\phi (x)$ es $x \geq 0$ ). Esta es una propiedad que se usa con mayor frecuencia en álgebra , especialmente en la resolución de sistemas de ecuaciones , pero se aplica en casi todas las áreas de las matemáticas que utilizan la igualdad. Esto, junto con la propiedad reflexiva de la igualdad, forma los axiomas de igualdad en la lógica de primer orden. ^{[ 9 ]}

La sustitución está relacionada con la composición de funciones , pero no es idéntica a ella ; guarda una estrecha relación con la β -reducción en el cálculo lambda . Sin embargo, a diferencia de estas nociones, en álgebra el énfasis recae en la preservación de la estructura algebraica mediante la operación de sustitución, es decir, en el hecho de que la sustitución proporciona un homomorfismo para la estructura en cuestión (en el caso de los polinomios, la estructura de anillo ).

Álgebra

La sustitución es una operación básica en álgebra , en particular en álgebra computacional . ^{[ 10 ]}^{[ 11 ]}

Un caso común de sustitución involucra polinomios , donde la sustitución de un valor numérico (u otra expresión) por la indeterminada de un polinomio univariado equivale a evaluar el polinomio en ese valor. De hecho, esta operación ocurre con tanta frecuencia que la notación para polinomios a menudo se adapta a ella; en lugar de designar un polinomio con un nombre como P , como se haría con otros objetos matemáticos, se podría definir

P(X)=X^{5}-3X^{2}+5X-17

de modo que la sustitución de X pueda designarse mediante el reemplazo dentro de " P ( X )", por ejemplo

P(2)=13

o

P(X+1)=X^{5}+5X^{4}+10X^{3}+7X^{2}+4X-14.

La sustitución también puede aplicarse a otros tipos de objetos formales construidos a partir de símbolos, por ejemplo, elementos de grupos libres . Para que la sustitución esté definida, se necesita una estructura algebraica con una propiedad universal apropiada que asegure la existencia de homomorfismos únicos que transforman indeterminadas en valores específicos; la sustitución consiste entonces en hallar la imagen de un elemento bajo dicho homomorfismo.

Prueba de sustitución en ZFC

A continuación se presenta una demostración de la propiedad de sustitución de igualdad en ZFC (tal como se define en la lógica de primer orden sin igualdad), adaptada de Introduction to Axiomatic Set Theory (1982) de Gaisi Takeuti y Wilson M. Zaring. ^{[ 12 ]}

Teorema — si $a=b$ , entonces, para cualquier fórmula bien formada $\phi$ , $\phi (a)\Rightarrow \phi (b)$ .

Véase la teoría de conjuntos de Zermelo-Fraenkel § Lenguaje formal para la definición de fórmulas en ZFC. La definición es recursiva , por lo que se utiliza una demostración por inducción . En ZFC, en lógica de primer orden sin igualdad, la "igualdad de conjuntos" se define como que dos conjuntos tienen los mismos elementos, escrito simbólicamente como "para todo z, z está en x si y solo si z está en y". Entonces, el axioma de extensionalidad afirma que si dos conjuntos tienen los mismos elementos, entonces pertenecen a los mismos conjuntos:

Definición - $(x=y):=\forall z[z\in x\Leftrightarrow z\in y]$

Axioma — $(x=y)\Rightarrow \forall z(x\in z\Leftrightarrow y\in z)$

Fórmulas básicas

Dejar $X,Y,Z$ , sean metavariables para cualquier variable o conjunto, de tal manera que $X=Y$

Caso 1: $\phi (X):(Z\en X)$

Asumir $Z\in X$ , entonces, por definición de igualdad, $Z\in Y$ , de este modo $(X=Y)\implies {\bigl [}Z\in X\Rightarrow Z\in Y{\bigr ]}$

Caso 2: $\phi (X):(X\en Z)$

Asumir $X\in Z$ , entonces por el axioma de extensionalidad, $Y\in Z$ , de este modo $(X=Y)\implies {\bigl [}X\in Z\Rightarrow Y\in Z{\bigr ]}$

Fórmulas recursivas

Dejar $\psi,\varphi$ ser meta variables para cualquier fórmula con la propiedad que $(a=b)\implies {\bigl [}\phi (a)\Rightarrow \phi (b){\bigr ]}$ . Dejar $X,Y$ , sean metavariables para cualquier variable o conjunto, de tal manera que $X=Y$ y dejar $z$ ser una metavariable para cualquier variable.

Caso 1: $\neg (\psi )$

Desde $X=Y$ , entonces $Y=X$ por simetría de igualdad, por lo tanto ${\bigl [}\psi (Y)\Rightarrow \psi (X){\bigr ]}$ , por la hipótesis de inducción, por lo tanto ${\bigl [}\neg \psi (X)\Rightarrow \neg \psi (Y){\bigr ]}$ por contraposición , así $(X=Y)\implies {\bigl [}\neg \psi (X)\Rightarrow \neg \psi (Y){\bigr ]}$

Caso 2: $\psi \land \varphi$

Desde $X=Y$ , entonces ${\bigl [}\psi (X)\Rightarrow \psi (Y){\bigr ]}$ y ${\bigl [}\varphi (X)\Rightarrow \varphi (Y){\bigr ]}$ , lo cual implica ${\bigl [}{\bigl (}\psi (X)\land \varphi (X){\bigr )}\Rightarrow \psi (Y)\land \varphi (Y){\bigr )}{\bigr ]}$ , de este modo $(X=Y)\implica {\bigl [}{\bigl (}\psi (X)\land \varphi (X){\bigr )}\Rightarrow \psi (Y)\land \varphi (Y){\bigr )}{\bigr ]}$

Caso 3: $\exists z(\psi )$

Desde $X=Y$ , $\psi (X,z)\Rightarrow \psi (Y,z)$ supongamos por contradicción que el resultado es falso, es decir $\exists z(\psi (X,z))$ es cierto pero $\exists z(\psi (Y,z))$ es falso. Por instanciación existencial , sea $z_{0}$ denotemos el valor tal que $\psi (X,z_{0})$ Es cierto. Entonces $\psi (Y,z_{0})$ es falso por suposición y por lo tanto $\psi (X,z_{0})\Rightarrow \psi (Y,z_{0})$ es falso, lo cual contradice nuestra hipótesis de inducción, y el resultado se deduce.

Véase también

Notas

↑ Algunos autores usan [ t ₁ / x ₁ , …, t _k / x _k ] para denotar esa sustitución, por ejemplo M. Wirsing (1990). Jan van Leeuwen (ed.). Especificación algebraica . Manual de informática teórica. Vol. B. Elsevier. págs. 675–788 . , aquí: pág. 682.
↑ Desde elpunto de vista del álgebra de términos , el conjunto T de términos es el álgebra de términos libre sobre el conjunto V de variables, por lo tanto, para cada aplicación de sustitución σ: V → T hay un homomorfismo único σ : T → T que coincide con σ en V ⊆ T ; la aplicación definida anteriormente de σ a un término t se considera entonces como la aplicación de la función σ al argumento t .

Citas

↑ Hunter, Geoffrey (1996) [1971]. Metalogic: An Introduction to the Metatheory of Standard First-Order Logic . University of California Press (publicado en 1973). p. 118. ISBN 9780520023567OCLC 36312727 ( Accesible para usuarios con discapacidades visuales )
1 2 David A. Duffy (1991). Principios de demostración automatizada de teoremas . Wiley.
1 2 Franz Baader , Wayne Snyder (2001). Alan Robinson y Andrei Voronkov (eds.). Teoría de la unificación (PDF) . Elsevier. págs. 439–526 . Archivado del original (PDF) el 8 de junio de 2015. Recuperado el 24 de septiembre de 2014 .
↑ N. Dershowitz; J.-P. Jouannaud (1990). "Sistemas de reescritura". En Jan van Leeuwen (ed.). Modelos formales y semántica . Manual de informática teórica. Vol. B. Elsevier. págs. 243–320 .
↑ Sobolev, SK (2001) [1994], "Axiomas de igualdad" , Enciclopedia de Matemáticas , EMS Press
↑ Deutsch, Harry y Pawel Garbacz, "Identidad relativa", The Stanford Encyclopedia of Philosophy (Edición de otoño de 2024), Edward N. Zalta y Uri Nodelman (eds.), próxima publicación. URL: https://plato.stanford.edu/entries/identity-relative/#StanAccoIden
↑ Sobolev, SK (2001) [1994], "Variable individual" , Enciclopedia de Matemáticas , EMS Press
↑ Sobolev, SK (2001) [1994], "Variable libre" , Enciclopedia de Matemáticas , EMS Press
↑ Fitting, M. , First-Order Logic and Automated Theorem Proving (Berlín/Heidelberg: Springer, 1990), pp. 198–200 .
^ Margret H. Hoft; Hartmut FW Hoft (6 de noviembre de 2002). Computación con Mathematica . Elsevier. ISBN 978-0-08-048855-4.
↑ Andre Heck (6 de diciembre de 2012). Introducción a Maple . Springer Science & Business Media. ISBN 978-1-4684-0484-5. sustitución.
↑ Takeuti, Gaisi; Zaring, Wilson M. (1982). «Introducción a la teoría axiomática de conjuntos» . Graduate Texts in Mathematics : 6–9 . doi : 10.1007/978-1-4613-8168-6 . ISSN 0072-5285 . Archivado del original el 6 de agosto de 2014.

Referencias

Crabbé, M. (2004). Sobre la noción de sustitución . Logic Journal of the IGPL, 12, 111–124.
Curry, HB (1952) Sobre la definición de sustitución, reemplazo y nociones afines en un sistema formal abstracto . Revue philosophique de Louvain 50, 251–269.
Kleene, SC (1967). Lógica matemática . Reimpreso en 2002, Dover. ISBN 0-486-42533-9
Robinson, Alan JA; Voronkov, Andrei (22 de junio de 2001). Manual de razonamiento automatizado . Elsevier. ISBN 978-0-08-053279-0

Enlaces externos

Sustitución en el laboratorio n

[5] Algunos autores usan [ t ₁ / x ₁ , …, t _k / x _k ] para denotar esa sustitución, por ejemplo M. Wirsing (1990). Jan van Leeuwen (ed.). Especificación algebraica . Manual de informática teórica. Vol. B. Elsevier. págs. 675–788 . , aquí: pág. 682.

[6] Desde elpunto de vista del álgebra de términos , el conjunto T de términos es el álgebra de términos libre sobre el conjunto V de variables, por lo tanto, para cada aplicación de sustitución σ: V → T hay un homomorfismo único σ : T → T que coincide con σ en V ⊆ T ; la aplicación definida anteriormente de σ a un término t se considera entonces como la aplicación de la función σ al argumento t .

[1] Hunter, Geoffrey (1996) [1971]. Metalogic: An Introduction to the Metatheory of Standard First-Order Logic . University of California Press (publicado en 1973). p. 118. ISBN 9780520023567OCLC 36312727 ( Accesible para usuarios con discapacidades visuales )

[Duffy.1991-2] 1 2 David A. Duffy (1991). Principios de demostración automatizada de teoremas . Wiley.

[Baader.Snyder.2001-3] 1 2 Franz Baader , Wayne Snyder (2001). Alan Robinson y Andrei Voronkov (eds.). Teoría de la unificación (PDF) . Elsevier. págs. 439–526 . Archivado del original (PDF) el 8 de junio de 2015. Recuperado el 24 de septiembre de 2014 .

[Dershowitz.Jouannaud.1990-4] N. Dershowitz; J.-P. Jouannaud (1990). "Sistemas de reescritura". En Jan van Leeuwen (ed.). Modelos formales y semántica . Manual de informática teórica. Vol. B. Elsevier. págs. 243–320 .

[7] Sobolev, SK (2001) [1994], "Axiomas de igualdad" , Enciclopedia de Matemáticas , EMS Press

[8] Deutsch, Harry y Pawel Garbacz, "Identidad relativa", The Stanford Encyclopedia of Philosophy (Edición de otoño de 2024), Edward N. Zalta y Uri Nodelman (eds.), próxima publicación. URL: https://plato.stanford.edu/entries/identity-relative/#StanAccoIden

[:0-9] Sobolev, SK (2001) [1994], "Variable individual" , Enciclopedia de Matemáticas , EMS Press

[10] Sobolev, SK (2001) [1994], "Variable libre" , Enciclopedia de Matemáticas , EMS Press

[11] Fitting, M. , First-Order Logic and Automated Theorem Proving (Berlín/Heidelberg: Springer, 1990), pp. 198–200 .

[HoftHoft2002-12] Margret H. Hoft; Hartmut FW Hoft (6 de noviembre de 2002). Computación con Mathematica . Elsevier. ISBN 978-0-08-048855-4.

[HECK2012-13] Andre Heck (6 de diciembre de 2012). Introducción a Maple . Springer Science & Business Media. ISBN 978-1-4684-0484-5. sustitución.

[14] Takeuti, Gaisi; Zaring, Wilson M. (1982). «Introducción a la teoría axiomática de conjuntos» . Graduate Texts in Mathematics : 6–9 . doi : 10.1007/978-1-4613-8168-6 . ISSN 0072-5285 . Archivado del original el 6 de agosto de 2014.

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[

[

[ 5 ]

[ 6 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]

[ 12 ]