1.8. Símbolos ligados en la teoría de conjuntos
La sintaxis de los símbolos ligados
El último tipo de expresiones que forman los símbolos son los símbolos
ligados (símbolos de unión).
Tal símbolo une una (o más) variable(s) (digamos x), en una expresión F que
puede usar x como una variable libre en adición a las variables libres que
están disponibles (con un valor) fuera. Por lo tanto, se separa la
subexpresión «interior» F usando x como libre del «exterior», donde x es
una variable ligada. Aplicado a los datos del símbolo x y la expresión F, se
da un valor que depende de la estructura urinaria definida por F con el
argumento x (pero no puede en general dar una imagen completa y leal de
esta estructura unaria, que puede ser demasiado compleja para ser totalmente
grabada como un mero objeto).
La sintaxis de la teoría de conjuntos y las
teorías genéricas tienen mucha diferencia, que gestionan el rango de una
manera diferente. En las teorías genéricas, los rangos son tipos, los datos
implícitos de cuantificadores. Pero los símbolos ligados de la teoría de
conjuntos hacen su rango variable sobre un conjunto que es un objeto
designado por un argumento adicional (un espacio para un término que no
utiliza la variable ligada).
Una expresión es fundamental si todas sus variables son ligadas (sus
ocurrencias están contenidas por los símbolos ligados).
Vamos a repasar los símbolos ligados principales en la teoría de conjuntos.
Las definiciones de las funciones por términos
El definidor de la función (∋ ↦) conecta una variable al término, siguiendo
la sintaxis (E ∋ x ↦ t (x)), donde x es la variable, E es su rango, y t(x)
es el término (aquí abreviado como un predicado unario con los posibles
parámetros implícitos); puede expresarse de una forma más corta como
(x ↦ t(x)) cuando E es determinado por el contexto. Es definido si t(x) es
definido para todo x en E; se toma después el functor definido por t y
se restringe su clase de definitud a E, para darlo como una función con
dominio E.
Entonces esto convierte a los functores en las funciones, haciendo el reverso
de la acción del evaluador de una función que ha convertido las funciones
en su papel (significado) como functores, cuyos clases de definitud eran los
conjuntos. Esto pone los functores en una única forma (los que sólo eran accesibles
de una manera indirecta para ser usados como funciones por su termino definido
que podría tener la complejidad ilimitada) como un único tipo de objetos.
En 1.10 vamos a formalizar esa herramienta y ver verla como un caso particular
de un principio más general para teoría de conjuntos.
Las relaciones y el símbolo constructor de conjuntos
Una relación es un objeto parecido a una operación, pero con valores
booleanos: actúa como un predicado cuyos argumentos recorren sobre los
conjuntos. Pero esto no necesita ser introducido como otro tipo de objetos,
ya que los conjuntos serán suficientes para desempeñar estos papeles.
Para cualquier predicado unario A definido en un conjunto E, la subclase de
E definida por A es un conjunto (rango de una variable x que se introduce
para recorrer E, de modo que pueda ser ligada, desde donde y seleccionamos
los valores que satisfacen A(x)), por lo tanto un subconjunto de E, escrito
{x∈E | A (x)} (conjunto de todas x en E tal que A(x)): para todo y,
y ∈ {x∈E | A(x)}
⇔ (y ∈ E ∧ A(y))
El símbolo ligado {∈ | }, se llama el constructor de conjuntos:
{x∈E | A (x)} conecta x con el rango E en A. Se utilizará como un definidor
de las relaciones unarias en E, que figuran como subconjuntos F de E,
evaluados por ∈ como predicados (x ∈ F) con un argumento x. Pero estos
predicados no son solamente definidos en E, pero en todo el universo, dando
0 fuera de E cuyos datos se pierden. Esta falta de operador Dom
no importa, ya que el dominio E es generalmente determinado por el contexto.
Como el definidor de la función (respectivamente el constructor de conjuntos)
registra toda la estructura definida por la expresión dada en el conjunto
dado, es suficiente definir cualquier otro definidor en la misma expresión
con el mismo dominio, como está hecho de una estructura unaria aplicada a
su resultado (que es una función, respectivamente un conjunto).
Paradoja de Russell
Por supuesto, si la clase de todos los objetos fuera un conjunto, entonces el
el constructor de conjuntos podría utilizarla para también convertir todas
las clases en conjuntos. Pero esto no es posible: la clase de todos los
conjuntos no puede ser un conjunto (ningún conjunto E nunca puede contener
todos los conjuntos), como se puede demostrar utilizando el mismo constructor
de conjuntos:
Teorema. Para cada conjunto E existe un conjunto F tal que F ∉ E.
Demostración. F={x∈E | Set(x) ∧ x ∉ x}
⇒ (F ∈ F ⇔ (F ∈ E ∧ F ∉ F))
⇒ (F ∉ F ∴ F ∉ E). ∎
Eso nos va a obligar a guardar las distinciones entre los conjuntos y las
clases.
Other languages:
FR : 1.8. Symboles
liants en théorie des ensembles