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 consistentemente sus símbolos variables o de marcador de posición con otras expresiones.
La expresión resultante se denomina instancia de sustitución, o instancia para abreviar, de la expresión original.
Propositional logic
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) " (T → S)
es una instancia de sustitución de:
- P ' Q
y
- (A ↔ A)
es una instancia de sustitución de:
- (A ↔ A)
En algunos sistemas de deducción para lógica proposicional, una nueva expresión (una proposición) puede introducirse en una línea de una derivación si es una instancia de sustitución de una línea anterior de la derivación (Hunter 1971, p. 118). Así es como se introducen nuevas líneas en algunos sistemas axiomáticos. En 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.
Tautologies
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 Θ es nuevamente una tautología. Este hecho implica la solidez de la regla de deducción descrita en la sección anterior.
Primera lógica de orden
En lógica de primer orden, una sustitución es una aplicación total σ: V → T de variables a términos; muchos autores, pero no todos, requieren además σ(x) = x para todas las variables x, excepto un número finito. La notación { x1 ↦ t1, …, xk ↦ tk } se refiere a una sustitución que asigna cada variable xi al término correspondiente ti, para i=1,…,k, y cada otra variable a sí misma; las xi deben ser distintas por pares. La aplicación de esa sustitución a un término t se escribe en notación sufija como t { x1 ↦ t1,..., xk ↦ tk }; significa reemplazar (simultáneamente) cada ocurrencia de cada xi en t por ti. El resultado tσ de aplicar una sustitución σ a un término t se llama instancia de ese término t. Por ejemplo, aplicando la sustitución { x ↦ z, z ↦ h(a,y) } al término
f() z , a, g() x ), Sí.) rendimientos f() h()a,Sí.) , a, g() z ), Sí.) .
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 denomina sustitución fundamental si asigna todas las variables de su dominio a términos fundamentales, es decir, libres de variables. La instancia de sustitución tσ de una sustitución fundamental es un término fundamental si todas las variables de t'están en el dominio de σ', es decir, si vars(t) ⊆ dom(σ). Una sustitución σ se denomina sustitución lineal si tσ es un término lineal para algún término lineal (y por lo tanto para cada uno) t que contenga precisamente las variables del dominio de σ, es decir, con vars(t) = dom(σ). Una sustitución σ se denomina sustitución plana si xσ es una variable para cada variable x. Una sustitución σ se denomina sustitución de cambio de nombre si es una permutación en el conjunto de todas las variables. Como toda permutación, una sustitución de cambio de nombre σ siempre tiene una sustitución inversa σ−1, tal que tσσ−1 = t = tσ−1σ 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 fundamental, { x ↦ x1, y ↦ y2+4 } no es fundamental ni plana, sino lineal, { x ↦ y2, y ↦ y2+4 } no es lineal ni plana, { x ↦ y2, y ↦ y2 } es plana, pero no lineal, { x ↦ x1, y ↦ y2 } es a la vez lineal y plana, pero no un cambio de nombre, ya que asigna tanto y como y2 a y2; cada una de estas sustituciones tiene el conjunto {x,y} como su dominio. Un ejemplo de una sustitución de cambio de nombre es { x ↦ x1, x1 ↦ y, y ↦ y2, y2 ↦ x }, tiene la inversa { x ↦ y2, y2 ↦ y, y ↦ x1, x1 ↦ x }. La sustitución plana { x ↦ z, y ↦ z } no puede tener una inversa, ya que, por ejemplo, (x+y) { x ↦ z, y ↦ z } = z+z, y el último término no se puede transformar de nuevo en x+y, ya que se pierde la información sobre el origen del que proviene a z. La sustitución fundamental { x ↦ 2 } no puede tener una inversa debido a una pérdida similar de información de origen, por ejemplo. 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 cada variable a términos de resultado sintácticamente iguales, formalmente: σ = τ si xσ = xτ para cada variable x ∈ V. La composición de dos sustituciones σ = { x1 ↦ t1, …, xk ↦ tk } y τ = { y1 ↦ u1, …, yl ↦ ul } se obtiene quitando de la sustitución { x1 ↦ t1τ, …, xk ↦ tkτ, y1 ↦ u1, …, yl ↦ ul } aquellos pares yi ↦ ui para los cuales yi ∈ { x1, …, xk }. La composición de σ y τ se denota por στ. La composición es una operación asociativa y es compatible con la aplicación de la sustitución, es decir, (ρσ)τ = ρ(στ), y (tσ)τ = t(στ), respectivamente, para cada sustitución ρ, σ, τ y cada término t. La sustitución de identidad, que asigna cada variable a sí misma, es el elemento neutro de la composición de la sustitución. Una sustitución σ se llama idempotente si σσ = σ, y por lo tanto tσσ = tσ para cada término t. Cuando xi≠ti para todo i, la sustitución { x1 ↦ t1, …, xk ↦ tk } es idempotente si y solo si ninguna de las variables xi ocurre en ningún tj. La composición de la sustitución no es conmutativa, es decir, στ puede ser diferente de τσ, incluso si σ y τ son idempotentes.
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, p. ej. ((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, p. ej. ((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, hay 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, también llamada Ley de Leibniz.
Si consideramos las matemáticas como un lenguaje formal, una variable es un símbolo de un alfabeto, normalmente una letra como x, y y z, que denota un rango de valores posibles. Si una variable es libre en una expresión o fórmula dada, entonces puede ser reemplazada por cualquiera de los valores en su rango. También se pueden sustituir ciertos tipos de variables ligadas. 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 que se cuantifican universalmente se pueden reemplazar por cualquiera de los valores en su rango, y el resultado será una declaració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 ligadas. Por ejemplo, en , dependiendo del contexto, la variable puede ser libre y atado, o viceversa, pero ambos no pueden ser libres. Determinar qué valor se supone libre depende del contexto y la semántica.
El propiedad de la igualdado Ley de Leibniz (aunque este último término se reserva generalmente para contextos filosóficos), generalmente declara que, si dos cosas son iguales, entonces cualquier propiedad de uno, debe ser una propiedad de la otra. Puede ser declarado formalmente en la notación lógica como:Por todos y , y cualquier fórmula bien formada (con una variable x gratuita). Por ejemplo: Para todos los números reales a y b, si a = bEntonces a ≥ 0 implicación b ≥ 0 (aquí, es x ≥ 0). Esta es una propiedad que se utiliza más a menudo en el álgebra, especialmente en la solución de sistemas de ecuaciones, pero se une en casi cada área de matemáticas que utiliza la igualdad. Esto, unido a la propiedad reflexiva de la igualdad, forma los axiomas de la igualdad en la lógica de primer orden.
La sustitución está relacionada con la composición de funciones, pero no es idéntica a ella; está estrechamente relacionada con la β-reducción en el cálculo lambda. Sin embargo, en contraste con estas nociones, el énfasis en el álgebra está en la preservación de la estructura algebraica mediante la operación de sustitución, el hecho de que la sustitución da 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.
Un caso común de sustitución involucra polinomios, donde la sustitución de un valor numérico (u otra expresión) por el indeterminado de un polinomio univariado equivale a evaluar el polinomio en ese valor. De hecho, esta operación ocurre tan frecuentemente 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 para otros objetos matemáticos, se podría definir
de modo que la sustitución de X se puede designar mediante reemplazo dentro de "P(X)", digamos
o
La sustitución también se puede aplicar a otros tipos de objetos formales construidos a partir de símbolos, por ejemplo, elementos de grupos libres. Para que se defina la sustitución, se necesita una estructura algebraica con una propiedad universal apropiada, que afirme la existencia de homomorfismos únicos que envíen indeterminados a valores específicos; la sustitución entonces equivale a encontrar la imagen de un elemento bajo tal homomorfismo.
Véase también
- Integración por sustitución
- Lambda cálculo § Substitution
- Interpolación de cuerdas
- Bienes de sustitución de la igualdad
- Sustitución trigonométrica
- Instantiación universal
Notas
- ^ Algunos autores utilizan [ t1/x1, ... tk/xk Para denotar esa sustitución, por ejemplo. M. Wirsing (1990). Jan van Leeuwen (ed.). Especificación algebraica. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 675–788., aquí: p. 682.
- ^ Desde un término punto de vista álgebra, el conjunto T de términos es el álgebra de término libre sobre el conjunto V de variables, por lo tanto para cada asignación de sustitución σ: V → T hay un homomorfismo único σ: T → T que está de acuerdo con σ en V ⊆ T; la aplicación anteriormente definida σ a un plazo t es entonces visto como la aplicación de la función σ al argumento t.
Citaciones
- ^ a b David A. Duffy (1991). Principios del Teorema Automatizado Proving. Wiley.
- ^ a b Franz Baader, Wayne Snyder (2001). Alan Robinson y Andrei Voronkov (ed.). Teoría de unificación (PDF). Elsevier. pp. 439-526. Archivado desde el original (PDF) en 2015-06-08. Retrieved 2014-09-24.
- ^ N. Dershowitz; J.-P. Jouannaud (1990). "Reescribir sistemas". En Jan van Leeuwen (ed.). Modelos formales y semántica. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243-320.
- ^ Sobolev, S.K. (originador). "Axiomas de igualdad". Enciclopedia de Matemáticas. Springer. ISBN 1402006098.
- ^ Deutsch, Harry y Pawel Garbacz, "Identidad Relativa", The Stanford Encyclopedia of Philosophy (Fall 2024 Edition), Edward N. Zalta & Uri Nodelman (eds.), URL siguiente: https://plato.stanford.edu/entries/identity-relative/#StanAccoIden
- ^ Sobolev, S.K. (originador). "Individual variable". Enciclopedia de Matemáticas. Springer. ISBN 1402006098. Retrieved 2024-09-05.
- ^ Sobolev, S.K. (originador). Variable libre. Enciclopedia de Matemáticas. Springer. ISBN 1402006098.
- ^ Fitting, M., Teorema lógico y automatizado Proving (Berlin/Heidelberg: Springer, 1990), págs. 198 a 200.
- ^ Margret H. Hoft; Hartmut F.W. Hoft (6 de noviembre de 2002). Computando 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.
Referencias
- Crabbé, M. (2004). Sobre el concepto de sustitución. Diario Lógico del IGPL, 12, 111–124.
- Curry, H. B. (1952) Sobre la definición de sustitución, sustitución y nociones aliadas en un sistema formal abstracto. Revue philosophique de Louvain 50, 251–269.
- Hunter, G. (1971). Metalogic: Introducción a la metateoría de la lógica de primera orden estándar. University of California Press. ISBN 0-520-01822-2
- Kleene, S. C. (1967). Lógica Matemática. Reimpreso 2002, Dover. ISBN 0-486-42533-9
Enlaces externos
- Sustitución en el nLab